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 : natClassfun).

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 phiphi^*)%CF.

Lemma cfConjC_cfun1 : (1^*)%CF = 1 :> 'CF(G).

Class function kernel and faithful class functions

Fact cfker_is_group phi : group_set (cfker phi).
Canonical cfker_group phi := Group (cfker_is_group phi).

Lemma cfker_sub phi : cfker phi \subset G.

Lemma cfker_norm phi : G \subset 'N(cfker phi).

Lemma cfker_normal phi : cfker phi <| G.

Lemma cfkerMl phi x y : x \in cfker phi phi (x × y)%g = phi y.

Lemma cfkerMr phi x y : x \in cfker phi phi (y × x)%g = phi y.

Lemma cfker1 phi x : x \in cfker phi phi x = phi 1%g.

Lemma cfker_cfun0 : @cfker _ G 0 = G.

Lemma cfker_add phi psi : cfker phi :&: cfker psi \subset cfker (phi + psi).

Lemma cfker_sum I r (P : pred I) (Phi : I 'CF(G)) :
  G :&: \bigcap_(i <- r | P i) cfker (Phi i)
   \subset cfker (\sum_(i <- r | P i) Phi i).

Lemma cfker_scale a phi : cfker phi \subset cfker (a *: phi).

Lemma cfker_scale_nz a phi : a != 0 cfker (a *: phi) = cfker phi.

Lemma cfker_opp phi : cfker (- phi) = cfker phi.

Lemma cfker_cfun1 : @cfker _ G 1 = G.

Lemma cfker_mul phi psi : cfker phi :&: cfker psi \subset cfker (phi × psi).

Lemma cfker_prod I r (P : pred I) (Phi : I 'CF(G)) :
  G :&: \bigcap_(i <- r | P i) cfker (Phi i)
   \subset cfker (\prod_(i <- r | P i) Phi i).

Lemma cfaithfulE phi : cfaithful phi = (cfker phi \subset [1]).

End ClassFun.

Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.

Hint Resolve cfun_onT.

Section DotProduct.

Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (M : {group gT}) (phi psi xi : 'CF(G)) (R S : seq 'CF(G)).

Lemma cfdotE phi psi :
  '[phi, psi] = #|G|%:R^-1 × \sum_(x in G) phi x × (psi x)^*.

Lemma cfdotElr A B phi psi :
     phi \in 'CF(G, A) psi \in 'CF(G, B)
  '[phi, psi] = #|G|%:R^-1 × \sum_(x in A :&: B) phi x × (psi x)^*.

Lemma cfdotEl A phi psi :
     phi \in 'CF(G, A)
  '[phi, psi] = #|G|%:R^-1 × \sum_(x in A) phi x × (psi x)^*.

Lemma cfdotEr A phi psi :
     psi \in 'CF(G, A)
  '[phi, psi] = #|G|%:R^-1 × \sum_(x in A) phi x × (psi x)^*.

Lemma cfdot_complement A phi psi :
  phi \in 'CF(G, A) psi \in 'CF(G, G :\: A) '[phi, psi] = 0.

Lemma cfnormE A phi :
  phi \in 'CF(G, A) '[phi] = #|G|%:R^-1 × (\sum_(x in A) `|phi x| ^+ 2).

Lemma eq_cfdotl A phi1 phi2 psi :
  psi \in 'CF(G, A) {in A, phi1 =1 phi2} '[phi1, psi] = '[phi2, psi].

Lemma cfdot_cfuni A B :
  A <| G B <| G '['1_A, '1_B]_G = #|A :&: B|%:R / #|G|%:R.

Lemma cfnorm1 : '[1]_G = 1.

Lemma cfdotrE psi phi : cfdotr psi phi = '[phi, psi].

Lemma cfdotr_is_linear xi : linear (cfdotr xi : 'CF(G) algC^o).
Canonical cfdotr_additive xi := Additive (cfdotr_is_linear xi).
Canonical cfdotr_linear xi := Linear (cfdotr_is_linear xi).

Lemma cfdot0l xi : '[0, xi] = 0.
Lemma cfdotNl xi phi : '[- phi, xi] = - '[phi, xi].
Lemma cfdotDl xi phi psi : '[phi + psi, xi] = '[phi, xi] + '[psi, xi].
Lemma cfdotBl xi phi psi : '[phi - psi, xi] = '[phi, xi] - '[psi, xi].
Lemma cfdotMnl xi phi n : '[phi *+ n, xi] = '[phi, xi] *+ n.
Lemma cfdot_suml xi I r (P : pred I) (phi : I 'CF(G)) :
  '[\sum_(i <- r | P i) phi i, xi] = \sum_(i <- r | P i) '[phi i, xi].
Lemma cfdotZl xi a phi : '[a *: phi, xi] = a × '[phi, xi].

Lemma cfdotC phi psi : '[phi, psi] = ('[psi, phi])^*.

Lemma eq_cfdotr A phi psi1 psi2 :
  phi \in 'CF(G, A) {in A, psi1 =1 psi2} '[phi, psi1] = '[phi, psi2].

Lemma cfdotBr xi phi psi : '[xi, phi - psi] = '[xi, phi] - '[xi, psi].
Canonical cfun_dot_additive xi := Additive (cfdotBr xi).

Lemma cfdot0r xi : '[xi, 0] = 0.
Lemma cfdotNr xi phi : '[xi, - phi] = - '[xi, phi].
Lemma cfdotDr xi phi psi : '[xi, phi + psi] = '[xi, phi] + '[xi, psi].
Lemma cfdotMnr xi phi n : '[xi, phi *+ n] = '[xi, phi] *+ n.
Lemma cfdot_sumr xi I r (P : pred I) (phi : I 'CF(G)) :
  '[xi, \sum_(i <- r | P i) phi i] = \sum_(i <- r | P i) '[xi, phi i].
Lemma cfdotZr a xi phi : '[xi, a *: phi] = a^* × '[xi, phi].

Lemma cfdot_cfAut (u : {rmorphism algC algC}) phi psi :
    {in image psi G, {morph u : x / x^*}}
  '[cfAut u phi, cfAut u psi] = u '[phi, psi].

Lemma cfdot_conjC phi psi : '[phi^*, psi^*] = '[phi, psi]^*.

Lemma cfdot_conjCl phi psi : '[phi^*, psi] = '[phi, psi^*]^*.

Lemma cfdot_conjCr phi psi : '[phi, psi^*] = '[phi^*, psi]^*.

Lemma cfnorm_ge0 phi : 0 '[phi].

Lemma cfnorm_eq0 phi : ('[phi] == 0) = (phi == 0).

Lemma cfnorm_gt0 phi : ('[phi] > 0) = (phi != 0).

Lemma sqrt_cfnorm_ge0 phi : 0 sqrtC '[phi].

Lemma sqrt_cfnorm_eq0 phi : (sqrtC '[phi] == 0) = (phi == 0).

Lemma sqrt_cfnorm_gt0 phi : (sqrtC '[phi] > 0) = (phi != 0).

Lemma cfnormZ a phi : '[a *: phi]= `|a| ^+ 2 × '[phi]_G.

Lemma cfnormN phi : '[- phi] = '[phi].

Lemma cfnorm_sign n phi : '[(-1) ^+ n *: phi] = '[phi].

Lemma cfnormD phi psi :
  let d := '[phi, psi] in '[phi + psi] = '[phi] + '[psi] + (d + d^*).

Lemma cfnormB phi psi :
  let d := '[phi, psi] in '[phi - psi] = '[phi] + '[psi] - (d + d^*).

Lemma cfnormDd phi psi : '[phi, psi] = 0 '[phi + psi] = '[phi] + '[psi].

Lemma cfnormBd phi psi : '[phi, psi] = 0 '[phi - psi] = '[phi] + '[psi].

Lemma cfnorm_conjC phi : '[phi^*] = '[phi].

Lemma cfCauchySchwarz phi psi :
  `|'[phi, psi]| ^+ 2 '[phi] × '[psi] ?= iff ~~ free (phi :: psi).

Lemma cfCauchySchwarz_sqrt phi psi :
  `|'[phi, psi]| sqrtC '[phi] × sqrtC '[psi] ?= iff ~~ free (phi :: psi).

Lemma cf_triangle_lerif phi psi :
  sqrtC '[phi + psi] sqrtC '[phi] + sqrtC '[psi]
           ?= iff ~~ free (phi :: psi) && (0 coord [tuple psi] 0 phi).

Lemma orthogonal_cons phi R S :
  orthogonal (phi :: R) S = orthogonal phi S && orthogonal R S.

Lemma orthoP phi psi : reflect ('[phi, psi] = 0) (orthogonal phi psi).

Lemma orthogonalP S R :
  reflect {in S & R, phi psi, '[phi, psi] = 0} (orthogonal S R).

Lemma orthoPl phi S :
  reflect {in S, psi, '[phi, psi] = 0} (orthogonal phi S).

Lemma orthogonal_sym : symmetric (@orthogonal _ G).

Lemma orthoPr S psi :
  reflect {in S, phi, '[phi, psi] = 0} (orthogonal S psi).

Lemma eq_orthogonal R1 R2 S1 S2 :
  R1 =i R2 S1 =i S2 orthogonal R1 S1 = orthogonal R2 S2.

Lemma orthogonal_catl R1 R2 S :
  orthogonal (R1 ++ R2) S = orthogonal R1 S && orthogonal R2 S.

Lemma orthogonal_catr R S1 S2 :
  orthogonal R (S1 ++ S2) = orthogonal R S1 && orthogonal R S2.

Lemma span_orthogonal S1 S2 phi1 phi2 :
    orthogonal S1 S2 phi1 \in <<S1>>%VS phi2 \in <<S2>>%VS
 '[phi1, phi2] = 0.

Lemma orthogonal_split S beta :
  {X : 'CF(G) & X \in <<S>>%VS &
      {Y | [/\ beta = X + Y, '[X, Y] = 0 & orthogonal Y S]}}.

Lemma map_orthogonal M (nu : 'CF(G) 'CF(M)) S R (A : pred 'CF(G)) :
  {in A &, isometry nu} {subset S A} {subset R A}
 orthogonal (map nu S) (map nu R) = orthogonal S R.

Lemma orthogonal_oppr S R : orthogonal S (map -%R R) = orthogonal S R.

Lemma orthogonal_oppl S R : orthogonal (map -%R S) R = orthogonal S R.

Lemma pairwise_orthogonalP S :
  reflect (uniq (0 :: S)
              {in S &, phi psi, phi != psi '[phi, psi] = 0})
          (pairwise_orthogonal S).

Lemma pairwise_orthogonal_cat R S :
  pairwise_orthogonal (R ++ S) =
    [&& pairwise_orthogonal R, pairwise_orthogonal S & orthogonal R S].

Lemma eq_pairwise_orthogonal R S :
  perm_eq R S pairwise_orthogonal R = pairwise_orthogonal S.

Lemma sub_pairwise_orthogonal S1 S2 :
    {subset S1 S2} uniq S1
  pairwise_orthogonal S2 pairwise_orthogonal S1.

Lemma orthogonal_free S : pairwise_orthogonal S free S.

Lemma filter_pairwise_orthogonal S p :
  pairwise_orthogonal S pairwise_orthogonal (filter p S).

Lemma orthonormal_not0 S : orthonormal S 0 \notin S.

Lemma orthonormalE S :
  orthonormal S = all [pred phi | '[phi] == 1] S && pairwise_orthogonal S.

Lemma orthonormal_orthogonal S : orthonormal S pairwise_orthogonal S.

Lemma orthonormal_cat R S :
  orthonormal (R ++ S) = [&& orthonormal R, orthonormal S & orthogonal R S].

Lemma eq_orthonormal R S : perm_eq R S orthonormal R = orthonormal S.

Lemma orthonormal_free S : orthonormal S free S.

Lemma orthonormalP S :
  reflect (uniq S {in S &, phi psi, '[phi, psi]_G = (phi == psi)%:R})
          (orthonormal S).

Lemma sub_orthonormal S1 S2 :
  {subset S1 S2} uniq S1 orthonormal S2 orthonormal S1.

Lemma orthonormal2P phi psi :
  reflect [/\ '[phi, psi] = 0, '[phi] = 1 & '[psi] = 1]
          (orthonormal [:: phi; psi]).

Lemma conjC_pair_orthogonal S chi :
    cfConjC_closed S ~~ has cfReal S pairwise_orthogonal S chi \in S
  pairwise_orthogonal (chi :: chi^*%CF).

Lemma cfdot_real_conjC phi psi : cfReal phi '[phi, psi^*]_G = '[phi, psi]^*.

Lemma extend_cfConjC_subset S X phi :
    cfConjC_closed S ~~ has cfReal S phi \in S phi \notin X
  cfConjC_subset X S cfConjC_subset [:: phi, phi^* & X]%CF S.

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.