+ +

Library mathcomp.character.classfun

+ +

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

+ +

+ 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.
+ +
+