- -

Library mathcomp.character.classfun

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This file contains the basic theory of class functions: - 'CF(G) == the type of class functions on G : {group gT}, i.e., - which map gT to the type algC of complex algebraics, - have support in G, and are constant on each conjugacy - class of G. 'CF(G) implements the FalgType interface of - finite-dimensional F-algebras. - The identity 1 : 'CF(G) is the indicator function of G, - and (later) the principal character. -> The %CF scope (cfun_scope) is bound to the 'CF(_) types. - 'CF(G)%VS == the (total) vector space of 'CF(G). - 'CF(G, A) == the subspace of functions in 'CF(G) with support in A. - phi x == the image of x : gT under phi : 'CF(G). - # [phi]%CF == the multiplicative order of phi : 'CF(G). - cfker phi == the kernel of phi : 'CF(G); note that cfker phi <| G. - cfaithful phi <=> phi : 'CF(G) is faithful (has a trivial kernel). - '1_A == the indicator function of A as a function of 'CF(G). - (Provided A <| G; G is determined by the context.) - phi^*%CF == the function conjugate to phi : 'CF(G). - cfAut u phi == the function conjugate to phi by an algC-automorphism u - phi^u The notation "_ ^u" is only reserved; it is up to - clients to set Notation "phi ^u" := (cfAut u phi). - ' [phi, psi] == the convolution of phi, psi : 'CF(G) over G, normalised - ' [phi, psi]_G by #|G| so that ' [1, 1]_G = 1 (G is usually inferred). - cfdotr psi phi == ' [phi, psi] (self-expanding). - ' [phi], ' [phi]_G == the squared norm ' [phi, phi] of phi : 'CF(G). - orthogonal R S <=> each phi in R : seq 'CF(G) is orthogonal to each psi in - S, i.e., ' [phi, psi] = 0. As 'CF(G) coerces to seq, one - can write orthogonal phi S and orthogonal phi psi. - pairwise_orthogonal S <=> the class functions in S are pairwise orthogonal - AND non-zero. - orthonormal S <=> S is pairwise orthogonal and all class functions in S - have norm 1. - isometry tau <-> tau : 'CF(D) -> 'CF(R) is an isometry, mapping - ' [, _ ]_D to ' [, _ ]_R. - {in CD, isometry tau, to CR} <-> in the domain CD, tau is an isometry - whose range is contained in CR. - cfReal phi <=> phi is real, i.e., phi^* == phi. - cfAut_closed u S <-> S : seq 'CF(G) is closed under conjugation by u. - cfConjC_closed S <-> S : seq 'CF(G) is closed under complex conjugation. - conjC_subset S1 S2 <-> S1 : seq 'CF(G) represents a subset of S2 closed - under complex conjugation. - := [/\ uniq S1, {subset S1 <= S2} & cfConjC_closed S1]. - 'Res[H] phi == the restriction of phi : 'CF(G) to a function of 'CF(H) - 'Res[H, G] phi 'Res[H] phi x = phi x if x \in H (when H \subset G), - 'Res phi 'Res[H] phi x = 0 if x \notin H. The syntax variants - allow H and G to be inferred; the default is to specify - H explicitly, and infer G from the type of phi. - 'Ind[G] phi == the class function of 'CF(G) induced by phi : 'CF(H), - 'Ind[G, H] phi when H \subset G. As with 'Res phi, both G and H can - 'Ind phi be inferred, though usually G isn't. - cfMorph phi == the class function in 'CF(G) that maps x to phi (f x), - where phi : 'CF(f @* G), provided G \subset 'dom f. - cfIsom isoGR phi == the class function in 'CF(R) that maps f x to phi x, - given isoGR : isom G R f, f : {morphism G >-> rT} and - phi : 'CF(G). - (phi %% H)%CF == special case of cfMorph phi, when phi : 'CF(G / H). - (phi / H)%CF == the class function in 'CF(G / H) that coincides with - phi : 'CF(G) on cosets of H \subset cfker phi. - For a group G that is a semidirect product (defG : K ><| H = G), we have - cfSdprod KxH phi == for phi : 'CF(H), the class function of 'CF(G) that - maps k * h to psi h when k \in K and h \in H. - For a group G that is a direct product (with KxH : K \x H = G), we have - cfDprodl KxH phi == for phi : 'CF(K), the class function of 'CF(G) that - maps k * h to phi k when k \in K and h \in H. - cfDprodr KxH psi == for psi : 'CF(H), the class function of 'CF(G) that - maps k * h to psi h when k \in K and h \in H. - cfDprod KxH phi psi == for phi : 'CF(K), psi : 'CF(H), the class function - of 'CF(G) that maps k * h to phi k * psi h (this is - the product of the two functions above). - Finally, given defG : \big[dprod/1](i | P i) A i = G, with G and A i - groups and i ranges over a finType, we have - cfBigdprodi defG phi == for phi : 'CF(A i) s.t. P i, the class function - of 'CF(G) that maps x to phi x_i, where x_i is the - (A i)-component of x : G. - cfBigdprod defG phi == for phi : forall i, 'CF(A i), the class function - of 'CF(G) that maps x to \prod(i | P i) phi i x_i, - where x_i is the (A i)-component of x : G. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
-Delimit Scope cfun_scope with CF.
- -
-Reserved Notation "''CF' ( G , A )" (at level 8, format "''CF' ( G , A )").
-Reserved Notation "''CF' ( G )" (at level 8, format "''CF' ( G )").
-Reserved Notation "''1_' G" (at level 8, G at level 2, format "''1_' G").
-Reserved Notation "''Res[' H , G ]" (at level 8, only parsing).
-Reserved Notation "''Res[' H ]" (at level 8, format "''Res[' H ]").
-Reserved Notation "''Res'" (at level 8, only parsing).
-Reserved Notation "''Ind[' G , H ]" (at level 8, only parsing).
-Reserved Notation "''Ind[' G ]" (at level 8, format "''Ind[' G ]").
-Reserved Notation "''Ind'" (at level 8, only parsing).
-Reserved Notation "'[ phi , psi ]_ G" (at level 2, only parsing).
-Reserved Notation "'[ phi , psi ]"
- (at level 2, format "'[hv' ''[' phi , '/ ' psi ] ']'").
-Reserved Notation "'[ phi ]_ G" (at level 2, only parsing).
-Reserved Notation "'[ phi ]" (at level 2, format "''[' phi ]").
-Reserved Notation "phi ^u" (at level 3, format "phi ^u").
- -
-Section AlgC.
-

- -

- Arithmetic properties of group orders in the characteristic 0 field algC. -

- -
-Variable (gT : finGroupType).
-Implicit Types (G : {group gT }) (B : {set gT }).
- -
-Lemma neq0CG G : (#|G |)%:R != 0 :> algC.
-Lemma neq0CiG G B : (#|G : B |)%:R != 0 :> algC.
- Lemma gt0CG G : 0 < #|G |%:R :> algC.
-Lemma gt0CiG G B : 0 < #|G : B |%:R :> algC.
- -
-Lemma algC'G G : [char algC ]^'.-group G.
- -
-End AlgC.
- -
-Section Defs.
- -
-Variable gT : finGroupType.
- -
-Definition is_class_fun (B : {set gT }) (f : {ffun gT → algC }) :=
-  [∀ x, ∀ y in B , f (x ^ y) == f x ] && (support f \subset B ).
- -
-Lemma intro_class_fun (G : {group gT }) f :
-    {in G &, ∀ x y, f (x ^ y) = f x } →
-    (∀ x, x \notin G → f x = 0) →
-  is_class_fun G (finfun f).
- -
-Variable B : {set gT }.
- -
-Record classfun : predArgType :=
-  Classfun {cfun_val; _ : is_class_fun G cfun_val}.
-Implicit Types phi psi xi : classfun.
-

- -

- The default expansion lemma cfunE requires key = 0. -

-Fact classfun_key : unit.
-Definition Cfun := locked_with classfun_key (fun flag : nat ⇒ Classfun).
- -
-Canonical cfun_subType := Eval hnf in [subType for cfun_val ].
-Definition cfun_eqMixin := Eval hnf in [eqMixin of classfun by <:].
-Canonical cfun_eqType := Eval hnf in EqType classfun cfun_eqMixin.
-Definition cfun_choiceMixin := Eval hnf in [choiceMixin of classfun by <:].
-Canonical cfun_choiceType := Eval hnf in ChoiceType classfun cfun_choiceMixin.
- -
-Definition fun_of_cfun phi := cfun_val phi : gT → algC.
-Coercion fun_of_cfun : classfun >-> Funclass.
- -
-Lemma cfunElock k f fP : @Cfun k (finfun f) fP =1 f.
- -
-Lemma cfunE f fP : @Cfun 0 (finfun f) fP =1 f.
- -
-Lemma cfunP phi psi : phi =1 psi ↔ phi = psi.
- -
-Lemma cfun0gen phi x : x \notin G → phi x = 0.
- -
-Lemma cfun_in_genP phi psi : {in G , phi =1 psi } → phi = psi.
- -
-Lemma cfunJgen phi x y : y \in G → phi (x ^ y) = phi x.
- -
-Fact cfun_zero_subproof : is_class_fun G (0 : {ffun _}).
- Definition cfun_zero := Cfun 0 cfun_zero_subproof.
- -
-Fact cfun_comp_subproof f phi :
-  f 0 = 0 → is_class_fun G [ffun x ⇒ f (phi x)].
-Definition cfun_comp f f0 phi := Cfun 0 (@cfun_comp_subproof f phi f0).
-Definition cfun_opp := cfun_comp (oppr0 _).
- -
-Fact cfun_add_subproof phi psi : is_class_fun G [ffun x ⇒ phi x + psi x ].
-Definition cfun_add phi psi := Cfun 0 (cfun_add_subproof phi psi).
- -
-Fact cfun_indicator_subproof (A : {set gT }) :
-  is_class_fun G [ffun x ⇒ ((x \in G ) && (x ^: G \subset A ))%:R ].
-Definition cfun_indicator A := Cfun 1 (cfun_indicator_subproof A).
- -
-Lemma cfun1Egen x : '1 _G x = (x \in G )%:R.
- -
-Fact cfun_mul_subproof phi psi : is_class_fun G [ffun x ⇒ phi x × psi x ].
-Definition cfun_mul phi psi := Cfun 0 (cfun_mul_subproof phi psi).
- -
-Definition cfun_unit := [pred phi : classfun | [∀ x in G , phi x != 0]].
-Definition cfun_inv phi :=
-  if phi \in cfun_unit then cfun_comp (invr0 _) phi else phi.
- -
-Definition cfun_scale a := cfun_comp (mulr0 a).
- -
-Fact cfun_addA : associative cfun_add.
- Fact cfun_addC : commutative cfun_add.
- Fact cfun_add0 : left_id cfun_zero cfun_add.
- Fact cfun_addN : left_inverse cfun_zero cfun_opp cfun_add.
- -
-Definition cfun_zmodMixin := ZmodMixin cfun_addA cfun_addC cfun_add0 cfun_addN.
-Canonical cfun_zmodType := ZmodType classfun cfun_zmodMixin.
- -
-Lemma muln_cfunE phi n x : (phi *+ n) x = phi x *+ n.
- -
-Lemma sum_cfunE I r (P : pred I) (phi : I → classfun) x :
-  (\sum_(i <- r | P i ) phi i) x = \sum_(i <- r | P i ) (phi i) x.
- -
-Fact cfun_mulA : associative cfun_mul.
- Fact cfun_mulC : commutative cfun_mul.
- Fact cfun_mul1 : left_id '1 _G cfun_mul.
-Fact cfun_mulD : left_distributive cfun_mul cfun_add.
- Fact cfun_nz1 : '1 _G != 0.
- -
-Definition cfun_ringMixin :=
-  ComRingMixin cfun_mulA cfun_mulC cfun_mul1 cfun_mulD cfun_nz1.
-Canonical cfun_ringType := RingType classfun cfun_ringMixin.
-Canonical cfun_comRingType := ComRingType classfun cfun_mulC.
- -
-Lemma expS_cfunE phi n x : (phi ^+ n .+1) x = phi x ^+ n .+1.
- -
-Fact cfun_mulV : {in cfun_unit , left_inverse 1 cfun_inv *%R }.
-Fact cfun_unitP phi psi : psi × phi = 1 → phi \in cfun_unit.
-Fact cfun_inv0id : {in [predC cfun_unit ], cfun_inv =1 id }.
- -
-Definition cfun_unitMixin := ComUnitRingMixin cfun_mulV cfun_unitP cfun_inv0id.
-Canonical cfun_unitRingType := UnitRingType classfun cfun_unitMixin.
-Canonical cfun_comUnitRingType := [comUnitRingType of classfun ].
- -
-Fact cfun_scaleA a b phi :
-  cfun_scale a (cfun_scale b phi) = cfun_scale (a × b) phi.
- Fact cfun_scale1 : left_id 1 cfun_scale.
- Fact cfun_scaleDr : right_distributive cfun_scale +%R.
- Fact cfun_scaleDl phi : {morph cfun_scale ^~ phi : a b / a + b }.
- -
-Definition cfun_lmodMixin :=
-  LmodMixin cfun_scaleA cfun_scale1 cfun_scaleDr cfun_scaleDl.
-Canonical cfun_lmodType := LmodType algC classfun cfun_lmodMixin.
- -
-Fact cfun_scaleAl a phi psi : a *: (phi × psi ) = (a *: phi ) × psi.
- Fact cfun_scaleAr a phi psi : a *: (phi × psi ) = phi × (a *: psi ).
- -
-Canonical cfun_lalgType := LalgType algC classfun cfun_scaleAl.
-Canonical cfun_algType := AlgType algC classfun cfun_scaleAr.
-Canonical cfun_unitAlgType := [unitAlgType algC of classfun ].
- -
-Section Automorphism.
- -
-Variable u : {rmorphism algC → algC }.
- -
-Definition cfAut := cfun_comp (rmorph0 u).
- -
-Lemma cfAut_cfun1i A : cfAut '1 _A = '1 _A.
- -
-Lemma cfAutZ a phi : cfAut (a *: phi) = u a *: cfAut phi.
- -
-Lemma cfAut_is_rmorphism : rmorphism cfAut.
-Canonical cfAut_additive := Additive cfAut_is_rmorphism.
-Canonical cfAut_rmorphism := RMorphism cfAut_is_rmorphism.
- -
-Lemma cfAut_cfun1 : cfAut 1 = 1.
- -
-Lemma cfAut_scalable : scalable_for (u \; *:%R) cfAut.
- Canonical cfAut_linear := AddLinear cfAut_scalable.
-Canonical cfAut_lrmorphism := [lrmorphism of cfAut ].
- -
-Definition cfAut_closed (S : seq classfun) :=
-  {in S , ∀ phi, cfAut phi \in S }.
- -
-End Automorphism.
- -
-Definition cfReal phi := cfAut conjC phi == phi.
- -
-Definition cfConjC_subset (S1 S2 : seq classfun) :=
-  [/\ uniq S1 , {subset S1 ≤ S2 } & cfAut_closed conjC S1 ].
- -
-Fact cfun_vect_iso : Vector.axiom #|classes G | classfun.
-Definition cfun_vectMixin := VectMixin cfun_vect_iso.
-Canonical cfun_vectType := VectType algC classfun cfun_vectMixin.
-Canonical cfun_FalgType := [FalgType algC of classfun ].
- -
-Definition cfun_base A : #|classes B ::&: A |.-tuple classfun :=
-  [tuple of [seq '1 _xB | xB in classes B ::&: A ]].
-Definition classfun_on A := <<cfun_base A >>%VS.
- -
-Definition cfdot phi psi := #|B |%:R ^-1 × \sum_(x in B ) phi x × (psi x )^*.
-Definition cfdotr_head k psi phi := let: tt := k in cfdot phi psi.
-Definition cfnorm_head k phi := let: tt := k in cfdot phi phi.
- -
-Coercion seq_of_cfun phi := [:: phi ].
- -
-Definition cforder phi := \big [lcmn /1%N]_(x in <<B >>) #[phi x ]%C.
- -
-End Defs.
- -
- -
- -
-Notation "''CF' ( G )" := (classfun G) : type_scope.
-Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope.
-Notation "''1_' A" := (cfun_indicator _ A) : ring_scope.
-Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
-Notation "1" := (@GRing.one (cfun_ringType _)) (only parsing) : cfun_scope.
- -
-Notation "phi ^*" := (cfAut conjC phi) : cfun_scope.
-Notation cfConjC_closed := (cfAut_closed conjC).
-

- -

- Workaround for overeager projection reduction. -

-Notation eqcfP := (@eqP (cfun_eqType _) _ _) (only parsing).
- -
-Notation "#[ phi ]" := (cforder phi) : cfun_scope.
-Notation "''[' u , v ]_ G":= (@cfdot _ G u v) (only parsing) : ring_scope.
-Notation "''[' u , v ]" := (cfdot u v) : ring_scope.
-Notation "''[' u ]_ G" := '[u, u]_G (only parsing) : ring_scope.
-Notation "''[' u ]" := '[u, u] : ring_scope.
-Notation cfdotr := (cfdotr_head tt).
-Notation cfnorm := (cfnorm_head tt).
- -
-Section Predicates.
- -
-Variables (gT rT : finGroupType) (D : {set gT }) (R : {set rT }).
-Implicit Types (phi psi : 'CF (D )) (S : seq 'CF (D )) (tau : 'CF (D ) → 'CF (R )).
- -
-Definition cfker phi := [set x in D | [∀ y, phi (x × y)%g == phi y ]].
- -
-Definition cfaithful phi := cfker phi \subset [1].
- -
-Definition ortho_rec S1 S2 :=
- all [pred phi | all [pred psi | '[phi , psi ] == 0] S2 ] S1.
- -
-Fixpoint pair_ortho_rec S :=
- if S is psi :: S' then ortho_rec psi S' && pair_ortho_rec S' else true.
- -
-

- -

- We exclude 0 from pairwise orthogonal sets. -

-Definition pairwise_orthogonal S := (0 \notin S ) && pair_ortho_rec S.
- -
-Definition orthonormal S := all [pred psi | '[psi ] == 1] S && pair_ortho_rec S.
- -
-Definition isometry tau := ∀ phi psi, '[tau phi , tau psi ] = '[phi , psi ].
- -
-Definition isometry_from_to mCFD tau mCFR :=
- prop_in2 mCFD (inPhantom (isometry tau))
- ∧ prop_in1 mCFD (inPhantom (∀ phi, in_mem (tau phi) mCFR)).
- -
-End Predicates.
- -
-

- -

- Outside section so the nosimpl does not get "cooked" out. -

-Definition orthogonal gT D S1 S2 := nosimpl (@ortho_rec gT D S1 S2).
- -
- -
-Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
-    (isometry_from_to (mem CFD) tau (mem CFR))
-  (at level 0, format "{ 'in' CFD , 'isometry' tau , 'to' CFR }")
-     : type_scope.
- -
-Section ClassFun.
- -
-Variables (gT : finGroupType) (G : {group gT }).
-Implicit Types (A B : {set gT }) (H K : {group gT }) (phi psi xi : 'CF (G )).
- -
- -
-Lemma cfun0 phi x : x \notin G → phi x = 0.
- -
-Lemma support_cfun phi : support phi \subset G.
- -
-Lemma cfunJ phi x y : y \in G → phi (x ^ y) = phi x.
- -
-Lemma cfun_repr phi x : phi (repr (x ^: G)) = phi x.
- -
-Lemma cfun_inP phi psi : {in G , phi =1 psi } → phi = psi.
- -
-Lemma cfuniE A x : A <| G → '1 _A x = (x \in A )%:R.
- -
-Lemma support_cfuni A : A <| G → support '1 _A =i A.
- -
-Lemma eq_mul_cfuni A phi : A <| G → {in A , phi × '1 _A =1 phi }.
- -
-Lemma eq_cfuni A : A <| G → {in A , '1 _A =1 (1 : 'CF (G ))}.
- -
-Lemma cfuniG : '1 _G = 1.
- -
-Lemma cfun1E g : (1 : 'CF (G )) g = (g \in G )%:R.
- -
-Lemma cfun11 : (1 : 'CF (G )) 1%g = 1.
- -
-Lemma prod_cfunE I r (P : pred I) (phi : I → 'CF (G )) x :
-  x \in G → (\prod_(i <- r | P i ) phi i) x = \prod_(i <- r | P i ) (phi i) x.
- -
-Lemma exp_cfunE phi n x : x \in G → (phi ^+ n) x = phi x ^+ n.
- -
-Lemma mul_cfuni A B : '1 _A × '1 _B = '1 _(A :&: B ) :> 'CF (G ).
- -
-Lemma cfun_classE x y : '1 _(x ^: G ) y = ((x \in G ) && (y \in x ^: G ))%:R.
- -
-Lemma cfun_on_sum A :
-  'CF (G , A ) = (\sum_(xG in classes G | xG \subset A ) <['1 _xG ]>)%VS.
- -
-Lemma cfun_onP A phi :
-  reflect (∀ x, x \notin A → phi x = 0) (phi \in 'CF (G , A )).
- -
-Lemma cfun_on0 A phi x : phi \in 'CF (G , A ) → x \notin A → phi x = 0.
- -
-Lemma sum_by_classes (R : ringType) (F : gT → R) :
-    {in G &, ∀ g h, F (g ^ h) = F g } →
-  \sum_(g in G ) F g = \sum_(xG in classes G ) #|xG |%:R × F (repr xG).
- -
-Lemma cfun_base_free A : free (cfun_base G A).
- -
-Lemma dim_cfun : \dim 'CF (G ) = #|classes G |.
- -
-Lemma dim_cfun_on A : \dim 'CF (G , A ) = #|classes G ::&: A |.
- -
-Lemma dim_cfun_on_abelian A : abelian G → A \subset G → \dim 'CF (G , A ) = #|A |.
- -
-Lemma cfuni_on A : '1 _A \in 'CF (G , A ).
- -
-Lemma mul_cfuni_on A phi : phi × '1 _A \in 'CF (G , A ).
- -
-Lemma cfun_onE phi A : (phi \in 'CF (G , A )) = (support phi \subset A ).
- -
-Lemma cfun_onT phi : phi \in 'CF (G , [set : gT ]).
- -
-Lemma cfun_onD1 phi A :
-  (phi \in 'CF (G , A ^#)) = (phi \in 'CF (G , A )) && (phi 1%g == 0).
- -
-Lemma cfun_onG phi : phi \in 'CF (G , G ).
- -
-Lemma cfunD1E phi : (phi \in 'CF (G , G ^#)) = (phi 1%g == 0).
- -
-Lemma cfunGid : 'CF (G , G ) = 'CF (G )%VS.
- -
-Lemma cfun_onS A B phi : B \subset A → phi \in 'CF (G , B ) → phi \in 'CF (G , A ).
- -
-Lemma cfun_complement A :
-  A <| G → ('CF (G , A ) + 'CF (G , G :\: A )%SET = 'CF (G ))%VS.
- -
-Lemma cfConjCE phi x : (phi ^*)%CF x = (phi x )^*.
- -
-Lemma cfConjCK : involutive (fun phi ⇒ phi ^*)%CF.
- -
-Lemma cfConjC_cfun1 : (1^*)%CF = 1 :> 'CF (G ).
- -
-

- -

- Class function kernel and faithful class functions -

- -

- Note: other isometry lemmas, and the dot product lemmas for orthogonal - and orthonormal sequences are in vcharacter, because we need the 'Z[S] - notation for the isometry domains. Alternatively, this could be moved to - cfun. -

- -
-End DotProduct.
- -
- -
-Section CfunOrder.
- -
-Variables (gT : finGroupType) (G : {group gT }) (phi : 'CF (G )).
- -
-Lemma dvdn_cforderP n :
-  reflect {in G , ∀ x, phi x ^+ n = 1} (#[phi ]%CF %| n)%N.
- -
-Lemma dvdn_cforder n : (#[phi ]%CF %| n ) = (phi ^+ n == 1).
- -
-Lemma exp_cforder : phi ^+ #[phi ]%CF = 1.
- -
-End CfunOrder.
- -
- -
-Section MorphOrder.
- -
-Variables (aT rT : finGroupType) (G : {group aT }) (R : {group rT }).
-Variable f : {rmorphism 'CF (G ) → 'CF (R )}.
- -
-Lemma cforder_rmorph phi : #[f phi ]%CF %| #[phi ]%CF.
- -
-Lemma cforder_inj_rmorph phi : injective f → #[f phi ]%CF = #[phi ]%CF.
- -
-End MorphOrder.
- -
-Section BuildIsometries.
- -
-Variable (gT : finGroupType) (L G : {group gT }).
-Implicit Types (phi psi xi : 'CF (L )) (R S : seq 'CF (L )).
-Implicit Types (U : {pred 'CF (L )}) (W : {pred 'CF (G )}).
- -
-Lemma sub_iso_to U1 U2 W1 W2 tau :
-    {subset U2 ≤ U1 } → {subset W1 ≤ W2 } →
-  {in U1 , isometry tau , to W1 } → {in U2 , isometry tau , to W2 }.
- -
-Lemma isometry_of_free S f :
-    free S → {in S &, isometry f } →
-  {tau : {linear 'CF (L ) → 'CF (G )} |
-    {in S , tau =1 f } & {in <<S >>%VS &, isometry tau }}.
- -
-Lemma isometry_of_cfnorm S tauS :
-    pairwise_orthogonal S → pairwise_orthogonal tauS →
-    map cfnorm tauS = map cfnorm S →
-  {tau : {linear 'CF (L ) → 'CF (G )} | map tau S = tauS
-                                   & {in <<S >>%VS &, isometry tau }}.
- -
-Lemma isometry_raddf_inj U (tau : {additive 'CF (L ) → 'CF (G )}) :
-    {in U &, isometry tau } → {in U &, ∀ u v, u - v \in U } →
-  {in U &, injective tau }.
- -
-Lemma opp_isometry : @isometry _ _ G G -%R.
- -
-End BuildIsometries.
- -
-Section Restrict.
- -
-Variables (gT : finGroupType) (A B : {set gT }).
- -
-Fact cfRes_subproof (phi : 'CF (B )) :
-  is_class_fun H [ffun x ⇒ phi (if H \subset G then x else 1%g) *+ (x \in H )].
-Definition cfRes phi := Cfun 1 (cfRes_subproof phi).
- -
-Lemma cfResE phi : A \subset B → {in A , cfRes phi =1 phi }.
- -
-Lemma cfRes1 phi : cfRes phi 1%g = phi 1%g.
- -
-Lemma cfRes_is_linear : linear cfRes.
-Canonical cfRes_additive := Additive cfRes_is_linear.
-Canonical cfRes_linear := Linear cfRes_is_linear.
- -
-Lemma cfRes_cfun1 : cfRes 1 = 1.
- -
-Lemma cfRes_is_multiplicative : multiplicative cfRes.
-Canonical cfRes_rmorphism := AddRMorphism cfRes_is_multiplicative.
-Canonical cfRes_lrmorphism := [lrmorphism of cfRes ].
- -
-End Restrict.
- -
-Notation "''Res[' H , G ]" := (@cfRes _ H G) (only parsing) : ring_scope.
-Notation "''Res[' H ]" := 'Res [H, _] : ring_scope.
-Notation "''Res'" := 'Res [_] (only parsing) : ring_scope.
- -
-Section MoreRestrict.
- -
-Variables (gT : finGroupType) (G H : {group gT }).
-Implicit Types (A : {set gT }) (phi : 'CF (G )).
- -
-Lemma cfResEout phi : ~~ (H \subset G ) → 'Res [H ] phi = (phi 1%g)%:A.
- -
-Lemma cfResRes A phi :
-  A \subset H → H \subset G → 'Res [A ] ('Res [H ] phi) = 'Res [A ] phi.
- -
-Lemma cfRes_id A psi : 'Res [A ] psi = psi.
- -
-Lemma sub_cfker_Res A phi :
-  A \subset H → A \subset cfker phi → A \subset cfker ('Res [H , G ] phi).
- -
-Lemma eq_cfker_Res phi : H \subset cfker phi → cfker ('Res [H , G ] phi) = H.
- -
-Lemma cfRes_sub_ker phi : H \subset cfker phi → 'Res [H , G ] phi = (phi 1%g)%:A.
- -
-Lemma cforder_Res phi : #['Res [H ] phi ]%CF %| #[phi ]%CF.
- -
-End MoreRestrict.
- -
-Section Morphim.
- -
-Variables (aT rT : finGroupType) (D : {group aT }) (f : {morphism D >-> rT }).
- -
-Section Main.
- -
-Variable G : {group aT }.
-Implicit Type phi : 'CF (f @* G ).
- -
-Fact cfMorph_subproof phi :
-  is_class_fun <<G >>
-    [ffun x ⇒ phi (if G \subset D then f x else 1%g) *+ (x \in G )].
-Definition cfMorph phi := Cfun 1 (cfMorph_subproof phi).
- -
-Lemma cfMorphE phi x : G \subset D → x \in G → cfMorph phi x = phi (f x).
- -
-Lemma cfMorph1 phi : cfMorph phi 1%g = phi 1%g.
- -
-Lemma cfMorphEout phi : ~~ (G \subset D ) → cfMorph phi = (phi 1%g)%:A.
- -
-Lemma cfMorph_cfun1 : cfMorph 1 = 1.
- -
-Fact cfMorph_is_linear : linear cfMorph.
-Canonical cfMorph_additive := Additive cfMorph_is_linear.
-Canonical cfMorph_linear := Linear cfMorph_is_linear.
- -
-Fact cfMorph_is_multiplicative : multiplicative cfMorph.
-Canonical cfMorph_rmorphism := AddRMorphism cfMorph_is_multiplicative.
-Canonical cfMorph_lrmorphism := [lrmorphism of cfMorph ].
- -
-Hypothesis sGD : G \subset D.
- -
-Lemma cfMorph_inj : injective cfMorph.
- -
-Lemma cfMorph_eq1 phi : (cfMorph phi == 1) = (phi == 1).
- -
-Lemma cfker_morph phi : cfker (cfMorph phi) = G :&: f @*^-1 (cfker phi ).
- -
-Lemma cfker_morph_im phi : f @* cfker (cfMorph phi) = cfker phi.
- -
-Lemma sub_cfker_morph phi (A : {set aT }) :
-  (A \subset cfker (cfMorph phi)) = (A \subset G ) && (f @* A \subset cfker phi ).
- -
-Lemma sub_morphim_cfker phi (A : {set aT }) :
-  A \subset G → (f @* A \subset cfker phi ) = (A \subset cfker (cfMorph phi)).
- -
-Lemma cforder_morph phi : #[cfMorph phi ]%CF = #[phi ]%CF.
- -
-End Main.
- -
-Lemma cfResMorph (G H : {group aT }) (phi : 'CF (f @* G )) :
-  H \subset G → G \subset D → 'Res (cfMorph phi ) = cfMorph ('Res [f @* H ] phi).
- -
-End Morphim.
- -
- -
-Section Isomorphism.
- -
-Variables (aT rT : finGroupType) (G : {group aT }) (f : {morphism G >-> rT }).
-Variable R : {group rT }.
- -
-Hypothesis isoGR : isom G R f.
- -
-Let defR := isom_im isoGR.
-Let defG : G1 = G := isom_im (isom_sym isoGR).
- -
-Fact cfIsom_key : unit.
-Definition cfIsom :=
-  locked_with cfIsom_key (cfMorph \o 'Res [G1 ] : 'CF (G ) → 'CF (R )).
-Canonical cfIsom_unlockable := [unlockable of cfIsom ].
- -
-Lemma cfIsomE phi x : x \in G → cfIsom phi (f x) = phi x.
- -
-Lemma cfIsom1 phi : cfIsom phi 1%g = phi 1%g.
- -
-Canonical cfIsom_additive := [additive of cfIsom ].
-Canonical cfIsom_linear := [linear of cfIsom ].
-Canonical cfIsom_rmorphism := [rmorphism of cfIsom ].
-Canonical cfIsom_lrmorphism := [lrmorphism of cfIsom ].
-Lemma cfIsom_cfun1 : cfIsom 1 = 1.
- -
-Lemma cfker_isom phi : cfker (cfIsom phi) = f @* cfker phi.
- -
-End Isomorphism.
- -
- -
-Section InvMorphism.
- -
-Variables (aT rT : finGroupType) (G : {group aT }) (f : {morphism G >-> rT }).
-Variable R : {group rT }.
- -
-Hypothesis isoGR : isom G R f.
- -
-Lemma cfIsomK : cancel (cfIsom isoGR) (cfIsom (isom_sym isoGR)).
- -
-Lemma cfIsomKV : cancel (cfIsom (isom_sym isoGR)) (cfIsom isoGR).
- -
-Lemma cfIsom_inj : injective (cfIsom isoGR).
- -
-Lemma cfIsom_eq1 phi : (cfIsom isoGR phi == 1) = (phi == 1).
- -
-Lemma cforder_isom phi : #[cfIsom isoGR phi ]%CF = #[phi ]%CF.
- -
-End InvMorphism.
- -
- -
-Section Coset.
- -
-Variables (gT : finGroupType) (G : {group gT }) (B : {set gT }).
-Implicit Type rT : finGroupType.
- -
-Definition cfMod : 'CF (G / B ) → 'CF (G ) := cfMorph.
- -
-Definition ffun_Quo (phi : 'CF (G )) :=
-  [ffun Hx : coset_of B ⇒
-    phi (if B \subset cfker phi then repr Hx else 1%g) *+ (Hx \in G / B)%g].
-Fact cfQuo_subproof phi : is_class_fun <<G / B >> (ffun_Quo phi).
-Definition cfQuo phi := Cfun 1 (cfQuo_subproof phi).
- -
- -
-

- -

- We specialize the cfMorph lemmas to cfMod by strengthening the domain - condition G \subset 'N(H) to H <| G; the cfMorph lemmas can be used if the - stronger results are needed. -

- -
-Lemma cfModE phi x : B <| G → x \in G → (phi %% B)%CF x = phi (coset B x).
- -
-Lemma cfMod1 phi : (phi %% B)%CF 1%g = phi 1%g.
- -
-Canonical cfMod_additive := [additive of cfMod ].
-Canonical cfMod_rmorphism := [rmorphism of cfMod ].
-Canonical cfMod_linear := [linear of cfMod ].
-Canonical cfMod_lrmorphism := [lrmorphism of cfMod ].
- -
-Lemma cfMod_cfun1 : (1 %% B)%CF = 1.
- -
-Lemma cfker_mod phi : B <| G → B \subset cfker (phi %% B).
- -
-

- -

- Note that cfQuo is nondegenerate even when G does not normalize B. -

- -
-Lemma cfQuoEnorm (phi : 'CF (G )) x :
-  B \subset cfker phi → x \in 'N_G (B ) → (phi / B)%CF (coset B x) = phi x.
- -
-Lemma cfQuoE (phi : 'CF (G )) x :
-  B <| G → B \subset cfker phi → x \in G → (phi / B)%CF (coset B x) = phi x.
- -
-Lemma cfQuo1 (phi : 'CF (G )) : (phi / B)%CF 1%g = phi 1%g.
- -
-Lemma cfQuoEout (phi : 'CF (G )) :
-  ~~ (B \subset cfker phi ) → (phi / B)%CF = (phi 1%g)%:A.
- -
-

- -

- cfQuo is only linear on the class functions that have H in their kernel. -

- -
-Lemma cfQuo_cfun1 : (1 / B)%CF = 1.
- -
-

- -

- Cancellation properties -

- -
-Lemma cfModK : B <| G → cancel cfMod cfQuo.
- -
-Lemma cfQuoK :
-  B <| G → ∀ phi, B \subset cfker phi → (phi / B %% B)%CF = phi.
- -
-Lemma cfMod_eq1 psi : B <| G → (psi %% B == 1)%CF = (psi == 1).
- -
-Lemma cfQuo_eq1 phi :
-  B <| G → B \subset cfker phi → (phi / B == 1)%CF = (phi == 1).
- -
-End Coset.
- -
-Notation "phi / H" := (cfQuo H phi) : cfun_scope.
-Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope.
- -
-Section MoreCoset.
- -
-Variables (gT : finGroupType) (G : {group gT }).
-Implicit Types (H K : {group gT }) (phi : 'CF (G )).
- -
-Lemma cfResMod H K (psi : 'CF (G / K )) :
-  H \subset G → K <| G → ('Res (psi %% K ) = 'Res [H / K ] psi %% K)%CF.
- -
-Lemma quotient_cfker_mod (A : {set gT }) K (psi : 'CF (G / K )) :
-  K <| G → (cfker (psi %% K) / K)%g = cfker psi.
- -
-Lemma sub_cfker_mod (A : {set gT }) K (psi : 'CF (G / K )) :
-    K <| G → A \subset 'N (K ) →
-  (A \subset cfker (psi %% K)) = (A / K \subset cfker psi)%g.
- -
-Lemma cfker_quo H phi :
-  H <| G → H \subset cfker (phi) → cfker (phi / H) = (cfker phi / H)%g.
- -
-Lemma cfQuoEker phi x :
-  x \in G → (phi / cfker phi)%CF (coset (cfker phi) x) = phi x.
- -
-Lemma cfaithful_quo phi : cfaithful (phi / cfker phi).
- -
-

- -

- Note that there is no requirement that K be normal in H or G. -

-Lemma cfResQuo H K phi :
-     K \subset cfker phi → K \subset H → H \subset G →
-  ('Res [H / K ] (phi / K) = 'Res [H ] phi / K)%CF.
- -
-Lemma cfQuoInorm K phi :
-  K \subset cfker phi → (phi / K)%CF = 'Res ('Res ['N_G (K )] phi / K )%CF.
- -
-Lemma cforder_mod H (psi : 'CF (G / H )) : H <| G → #[psi %% H ]%CF = #[psi ]%CF.
- -
-Lemma cforder_quo H phi :
-  H <| G → H \subset cfker phi → #[phi / H ]%CF = #[phi ]%CF.
- -
-End MoreCoset.
- -
-Section Product.
- -
-Variable (gT : finGroupType) (G : {group gT }).
- -
-Lemma cfunM_onI A B phi psi :
-  phi \in 'CF (G , A ) → psi \in 'CF (G , B ) → phi × psi \in 'CF (G , A :&: B ).
- -
-Lemma cfunM_on A phi psi :
-  phi \in 'CF (G , A ) → psi \in 'CF (G , A ) → phi × psi \in 'CF (G , A ).
- -
-End Product.
- -
-Section SDproduct.
- -
-Variables (gT : finGroupType) (G K H : {group gT }).
-Hypothesis defG : K ><| H = G.
- -
-Fact cfSdprodKey : unit.
- -
-Definition cfSdprod :=
-  locked_with cfSdprodKey
-   (cfMorph \o cfIsom (tagged (sdprod_isom defG)) : 'CF (H ) → 'CF (G )).
-Canonical cfSdprod_unlockable := [unlockable of cfSdprod ].
- -
-Canonical cfSdprod_additive := [additive of cfSdprod ].
-Canonical cfSdprod_linear := [linear of cfSdprod ].
-Canonical cfSdprod_rmorphism := [rmorphism of cfSdprod ].
-Canonical cfSdprod_lrmorphism := [lrmorphism of cfSdprod ].
- -
-Lemma cfSdprod1 phi : cfSdprod phi 1%g = phi 1%g.
- -
-Let nsKG : K <| G.
-Let sHG : H \subset G.
-Let sKG : K \subset G.
- -
-Lemma cfker_sdprod phi : K \subset cfker (cfSdprod phi).
- -
-Lemma cfSdprodEr phi : {in H , cfSdprod phi =1 phi }.
- -
-Lemma cfSdprodE phi : {in K & H , ∀ x y, cfSdprod phi (x × y)%g = phi y }.
- -
-Lemma cfSdprodK : cancel cfSdprod 'Res [H ].
- -
-Lemma cfSdprod_inj : injective cfSdprod.
- -
-Lemma cfSdprod_eq1 phi : (cfSdprod phi == 1) = (phi == 1).
- -
-Lemma cfRes_sdprodK phi : K \subset cfker phi → cfSdprod ('Res [H ] phi) = phi.
- -
-Lemma sdprod_cfker phi : K ><| cfker phi = cfker (cfSdprod phi).
- -
-Lemma cforder_sdprod phi : #[cfSdprod phi ]%CF = #[phi ]%CF.
- -
-End SDproduct.
- -
-Section DProduct.
- -
-Variables (gT : finGroupType) (G K H : {group gT }).
-Hypothesis KxH : K \x H = G.
- -
-Lemma reindex_dprod R idx (op : Monoid.com_law idx) (F : gT → R) :
-   \big [op /idx ]_(g in G ) F g =
-      \big [op /idx ]_(k in K ) \big [op /idx ]_(h in H ) F (k × h)%g.
- -
-Definition cfDprodr := cfSdprod (dprodWsd KxH).
-Definition cfDprodl := cfSdprod (dprodWsdC KxH).
-Definition cfDprod phi psi := cfDprodl phi × cfDprodr psi.
- -
-Canonical cfDprodl_additive := [additive of cfDprodl ].
-Canonical cfDprodl_linear := [linear of cfDprodl ].
-Canonical cfDprodl_rmorphism := [rmorphism of cfDprodl ].
-Canonical cfDprodl_lrmorphism := [lrmorphism of cfDprodl ].
-Canonical cfDprodr_additive := [additive of cfDprodr ].
-Canonical cfDprodr_linear := [linear of cfDprodr ].
-Canonical cfDprodr_rmorphism := [rmorphism of cfDprodr ].
-Canonical cfDprodr_lrmorphism := [lrmorphism of cfDprodr ].
- -
-Lemma cfDprodl1 phi : cfDprodl phi 1%g = phi 1%g.
-Lemma cfDprodr1 psi : cfDprodr psi 1%g = psi 1%g.
-Lemma cfDprod1 phi psi : cfDprod phi psi 1%g = phi 1%g × psi 1%g.
- -
-Lemma cfDprodl_eq1 phi : (cfDprodl phi == 1) = (phi == 1).
- Lemma cfDprodr_eq1 psi : (cfDprodr psi == 1) = (psi == 1).
- -
-Lemma cfDprod_cfun1r phi : cfDprod phi 1 = cfDprodl phi.
- Lemma cfDprod_cfun1l psi : cfDprod 1 psi = cfDprodr psi.
- Lemma cfDprod_cfun1 : cfDprod 1 1 = 1.
- Lemma cfDprod_split phi psi : cfDprod phi psi = cfDprod phi 1 × cfDprod 1 psi.
- -
-Let nsKG : K <| G.
-Let nsHG : H <| G.
-Let cKH : H \subset 'C (K ).
-Let sKG := normal_sub nsKG.
-Let sHG := normal_sub nsHG.
- -
-Lemma cfDprodlK : cancel cfDprodl 'Res [K ].
-Lemma cfDprodrK : cancel cfDprodr 'Res [H ].
- -
-Lemma cfker_dprodl phi : cfker phi \x H = cfker (cfDprodl phi).
- -
-Lemma cfker_dprodr psi : K \x cfker psi = cfker (cfDprodr psi).
- -
-Lemma cfDprodEl phi : {in K & H , ∀ k h, cfDprodl phi (k × h)%g = phi k }.
- -
-Lemma cfDprodEr psi : {in K & H , ∀ k h, cfDprodr psi (k × h)%g = psi h }.
- -
-Lemma cfDprodE phi psi :
-  {in K & H , ∀ h k, cfDprod phi psi (h × k)%g = phi h × psi k }.
- -
-Lemma cfDprod_Resl phi psi : 'Res [K ] (cfDprod phi psi) = psi 1%g *: phi.
- -
-Lemma cfDprod_Resr phi psi : 'Res [H ] (cfDprod phi psi) = phi 1%g *: psi.
- -
-Lemma cfDprodKl (psi : 'CF (H )) : psi 1%g = 1 → cancel (cfDprod ^~ psi) 'Res.
- -
-Lemma cfDprodKr (phi : 'CF (K )) : phi 1%g = 1 → cancel (cfDprod phi) 'Res.
- -
-

- -

- Note that equality holds here iff either cfker phi = K and cfker psi = H, - or else phi != 0, psi != 0 and coprime #|K : cfker phi| #|H : cfker phi|. -

-Lemma cfker_dprod phi psi :
-  cfker phi <*> cfker psi \subset cfker (cfDprod phi psi).
- -
-Lemma cfdot_dprod phi1 phi2 psi1 psi2 :
-  '[cfDprod phi1 psi1 , cfDprod phi2 psi2 ] = '[phi1 , phi2 ] × '[psi1 , psi2 ].
- -
-Lemma cfDprodl_iso : isometry cfDprodl.
- -
-Lemma cfDprodr_iso : isometry cfDprodr.
- -
-Lemma cforder_dprodl phi : #[cfDprodl phi ]%CF = #[phi ]%CF.
- -
-Lemma cforder_dprodr psi : #[cfDprodr psi ]%CF = #[psi ]%CF.
- -
-End DProduct.
- -
-Lemma cfDprodC (gT : finGroupType) (G K H : {group gT })
-               (KxH : K \x H = G) (HxK : H \x K = G) chi psi :
-  cfDprod KxH chi psi = cfDprod HxK psi chi.
- -
-Section Bigdproduct.
- -
-Variables (gT : finGroupType) (I : finType) (P : pred I).
-Variables (A : I → {group gT }) (G : {group gT }).
-Hypothesis defG : \big [dprod /1%g]_(i | P i ) A i = G.
- -
-Let sAG i : P i → A i \subset G.
- -
-Fact cfBigdprodi_subproof i :
-  gval (if P i then A i else 1%G) \x <<\bigcup_(j | P j && (j != i )) A j >> = G.
-Definition cfBigdprodi i := cfDprodl (cfBigdprodi_subproof i) \o 'Res [_, A i ].
- -
-Canonical cfBigdprodi_additive i := [additive of @cfBigdprodi i ].
-Canonical cfBigdprodi_linear i := [linear of @cfBigdprodi i ].
-Canonical cfBigdprodi_rmorphism i := [rmorphism of @cfBigdprodi i ].
-Canonical cfBigdprodi_lrmorphism i := [lrmorphism of @cfBigdprodi i ].
- -
-Lemma cfBigdprodi1 i (phi : 'CF (A i )) : cfBigdprodi phi 1%g = phi 1%g.
- -
-Lemma cfBigdprodi_eq1 i (phi : 'CF (A i )) :
-  P i → (cfBigdprodi phi == 1) = (phi == 1).
- -
-Lemma cfBigdprodiK i : P i → cancel (@cfBigdprodi i) 'Res [A i ].
- -
-Lemma cfBigdprodi_inj i : P i → injective (@cfBigdprodi i).
- -
-Lemma cfBigdprodEi i (phi : 'CF (A i )) x :
-    P i → (∀ j, P j → x j \in A j ) →
-  cfBigdprodi phi (\prod_(j | P j ) x j)%g = phi (x i).
- -
-Lemma cfBigdprodi_iso i : P i → isometry (@cfBigdprodi i).
- -
-Definition cfBigdprod (phi : ∀ i, 'CF (A i )) :=
-  \prod_(i | P i ) cfBigdprodi (phi i).
- -
-Lemma cfBigdprodE phi x :
-    (∀ i, P i → x i \in A i ) →
-  cfBigdprod phi (\prod_(i | P i ) x i)%g = \prod_(i | P i ) phi i (x i).
- -
-Lemma cfBigdprod1 phi : cfBigdprod phi 1%g = \prod_(i | P i ) phi i 1%g.
- -
-Lemma cfBigdprodK phi (Phi := cfBigdprod phi) i (a := phi i 1%g / Phi 1%g) :
-  Phi 1%g != 0 → P i → a != 0 ∧ a *: 'Res [A i ] Phi = phi i.
- -
-Lemma cfdot_bigdprod phi psi :
-  '[cfBigdprod phi , cfBigdprod psi ] = \prod_(i | P i ) '[phi i , psi i ].
- -
-End Bigdproduct.
- -
-Section MorphIsometry.
- -
-Variable gT : finGroupType.
-Implicit Types (D G H K : {group gT }) (aT rT : finGroupType).
- -
-Lemma cfMorph_iso aT rT (G D : {group aT }) (f : {morphism D >-> rT }) :
-  G \subset D → isometry (cfMorph : 'CF (f @* G ) → 'CF (G )).
- -
-Lemma cfIsom_iso rT G (R : {group rT }) (f : {morphism G >-> rT }) :
-  ∀ isoG : isom G R f, isometry (cfIsom isoG).
- -
-Lemma cfMod_iso H G : H <| G → isometry (@cfMod _ G H).
- -
-Lemma cfQuo_iso H G :
-  H <| G → {in [pred phi | H \subset cfker phi ] &, isometry (@cfQuo _ G H)}.
- -
-Lemma cfnorm_quo H G phi :
-  H <| G → H \subset cfker phi → '[phi / H ] = '[phi ]_G.
- -
-Lemma cfSdprod_iso K H G (defG : K ><| H = G) : isometry (cfSdprod defG).
- -
-End MorphIsometry.
- -
-Section Induced.
- -
-Variable gT : finGroupType.
- -
-Section Def.
- -
-Variables B A : {set gT }.
- -
-

- -

- The defalut value for the ~~ (H \subset G) case matches the one for cfRes - so that Frobenius reciprocity holds even in this degenerate case. -

-Definition ffun_cfInd (phi : 'CF (A )) :=
-  [ffun x ⇒ if H \subset G then #|A |%:R ^-1 × (\sum_(y in G ) phi (x ^ y))
-                            else #|G |%:R × '[phi , 1] *+ (x == 1%g)].
- -
-Fact cfInd_subproof phi : is_class_fun G (ffun_cfInd phi).
-Definition cfInd phi := Cfun 1 (cfInd_subproof phi).
- -
-Lemma cfInd_is_linear : linear cfInd.
-Canonical cfInd_additive := Additive cfInd_is_linear.
-Canonical cfInd_linear := Linear cfInd_is_linear.
- -
-End Def.
- -
- -
-Lemma cfIndE (G H : {group gT }) phi x :
-  H \subset G → 'Ind [G , H ] phi x = #|H |%:R ^-1 × (\sum_(y in G ) phi (x ^ y)).
- -
-Variables G K H : {group gT }.
-Implicit Types (phi : 'CF (H )) (psi : 'CF (G )).
- -
-Lemma cfIndEout phi :
-  ~~ (H \subset G ) → 'Ind [G ] phi = (#|G |%:R × '[phi , 1]) *: '1 _1%G.
- -
-Lemma cfIndEsdprod (phi : 'CF (K )) x :
-  K ><| H = G → 'Ind [G ] phi x = \sum_(w in H ) phi (x ^ w)%g.
- -
-Lemma cfInd_on A phi :
-  H \subset G → phi \in 'CF (H , A ) → 'Ind [G ] phi \in 'CF (G , class_support A G ).
- -
-Lemma cfInd_id phi : 'Ind [H ] phi = phi.
- -
-Lemma cfInd_normal phi : H <| G → 'Ind [G ] phi \in 'CF (G , H ).
- -
-Lemma cfInd1 phi : H \subset G → 'Ind [G ] phi 1%g = #|G : H |%:R × phi 1%g.
- -
-Lemma cfInd_cfun1 : H <| G → 'Ind [G , H ] 1 = #|G : H |%:R *: '1 _H.
- -
-Lemma cfnorm_Ind_cfun1 : H <| G → '['Ind [G , H ] 1] = #|G : H |%:R.
- -
-Lemma cfIndInd phi :
-  K \subset G → H \subset K → 'Ind [G ] ('Ind [K ] phi) = 'Ind [G ] phi.
- -
-

- -

- This is Isaacs, Lemma (5.2). -

-Lemma Frobenius_reciprocity phi psi : '[phi , 'Res [H ] psi ] = '['Ind [G ] phi , psi ].
-Definition cfdot_Res_r := Frobenius_reciprocity.
- -
-Lemma cfdot_Res_l psi phi : '['Res [H ] psi , phi ] = '[psi , 'Ind [G ] phi ].
- -
-Lemma cfIndM phi psi: H \subset G →
-     'Ind [G ] (phi × ('Res [H ] psi )) = 'Ind [G ] phi × psi.
- -
-End Induced.
- -
-Notation "''Ind[' G , H ]" := (@cfInd _ G H) (only parsing) : ring_scope.
-Notation "''Ind[' G ]" := 'Ind [G, _] : ring_scope.
-Notation "''Ind'" := 'Ind [_] (only parsing) : ring_scope.
- -
-Section MorphInduced.
- -
-Variables (aT rT : finGroupType) (D G H : {group aT }) (R S : {group rT }).
- -
-Lemma cfIndMorph (f : {morphism D >-> rT }) (phi : 'CF (f @* H )) :
-    'ker f \subset H → H \subset G → G \subset D →
-  'Ind [G ] (cfMorph phi) = cfMorph ('Ind [f @* G ] phi).
- -
-Variables (g : {morphism G >-> rT }) (h : {morphism H >-> rT }).
-Hypotheses (isoG : isom G R g) (isoH : isom H S h) (eq_hg : {in H , h =1 g }).
-Hypothesis sHG : H \subset G.
- -
-Lemma cfResIsom phi : 'Res [S ] (cfIsom isoG phi) = cfIsom isoH ('Res [H ] phi).
- -
-Lemma cfIndIsom phi : 'Ind [R ] (cfIsom isoH phi) = cfIsom isoG ('Ind [G ] phi).
- -
-End MorphInduced.
- -
-Section FieldAutomorphism.
- -
-Variables (u : {rmorphism algC → algC }) (gT rT : finGroupType).
-Variables (G K H : {group gT }) (f : {morphism G >-> rT }) (R : {group rT }).
-Implicit Types (phi : 'CF (G )) (S : seq 'CF (G )).
- -
-Lemma cfAutZ_nat n phi : (n %:R *: phi )^u = n %:R *: phi ^u.
- -
-Lemma cfAutZ_Cnat z phi : z \in Cnat → (z *: phi )^u = z *: phi ^u.
- -
-Lemma cfAutZ_Cint z phi : z \in Cint → (z *: phi )^u = z *: phi ^u.
- -
-Lemma cfAutK : cancel (@cfAut gT G u) (cfAut (algC_invaut_rmorphism u)).
- -
-Lemma cfAutVK : cancel (cfAut (algC_invaut_rmorphism u)) (@cfAut gT G u).
- -
-Lemma cfAut_inj : injective (@cfAut gT G u).
- -
-Lemma cfAut_eq1 phi : (cfAut u phi == 1) = (phi == 1).
- -
-Lemma support_cfAut phi : support phi ^u =i support phi.
- -
-Lemma map_cfAut_free S : cfAut_closed u S → free S → free (map (cfAut u) S).
- -
-Lemma cfAut_on A phi : (phi ^u \in 'CF (G , A )) = (phi \in 'CF (G , A )).
- -
-Lemma cfker_aut phi : cfker phi ^u = cfker phi.
- -
-Lemma cfAut_cfuni A : ('1 _A )^u = '1 _A :> 'CF (G ).
- -
-Lemma cforder_aut phi : #[phi ^u ]%CF = #[phi ]%CF.
- -
-Lemma cfAutRes phi : ('Res [H ] phi )^u = 'Res phi ^u.
- -
-Lemma cfAutMorph (psi : 'CF (f @* H )) : (cfMorph psi )^u = cfMorph psi ^u.
- -
-Lemma cfAutIsom (isoGR : isom G R f) phi :
-  (cfIsom isoGR phi )^u = cfIsom isoGR phi ^u.
- -
-Lemma cfAutQuo phi : (phi / H )^u = (phi ^u / H)%CF.
- -
-Lemma cfAutMod (psi : 'CF (G / H )) : (psi %% H )^u = (psi ^u %% H)%CF.
- -
-Lemma cfAutInd (psi : 'CF (H )) : ('Ind [G ] psi )^u = 'Ind psi ^u.
- -
-Hypothesis KxH : K \x H = G.
- -
-Lemma cfAutDprodl (phi : 'CF (K )) : (cfDprodl KxH phi )^u = cfDprodl KxH phi ^u.
- -
-Lemma cfAutDprodr (psi : 'CF (H )) : (cfDprodr KxH psi )^u = cfDprodr KxH psi ^u.
- -
-Lemma cfAutDprod (phi : 'CF (K )) (psi : 'CF (H )) :
-  (cfDprod KxH phi psi )^u = cfDprod KxH phi ^u psi ^u.
- -
-End FieldAutomorphism.
- -
- -
-Definition conj_cfRes := cfAutRes conjC.
-Definition cfker_conjC := cfker_aut conjC.
-Definition conj_cfQuo := cfAutQuo conjC.
-Definition conj_cfMod := cfAutMod conjC.
-Definition conj_cfInd := cfAutInd conjC.
-Definition cfconjC_eq1 := cfAut_eq1 conjC.
-