Library mathcomp.character.classfun
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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).
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.
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.
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)).
Implicit Arguments cfun_onP [A phi].
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).
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)).
Implicit Arguments cfun_onP [A phi].
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
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.
Implicit Arguments cfun_onP [gT G A phi].
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).
Implicit Arguments orthoPl [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.
Implicit Arguments orthoP [gT G phi psi].
Implicit Arguments orthoPl [gT G phi S].
Implicit Arguments orthoPr [gT G S psi].
Implicit Arguments orthogonalP [gT G R S].
Implicit Arguments pairwise_orthogonalP [gT G S].
Implicit Arguments orthonormalP [gT G S].
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.
Implicit Arguments dvdn_cforderP [gT G phi n].
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.
Implicit Arguments cfIsom_inj [aT rT G R f x1 x2].
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.
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.
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}.
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.
[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.
Implicit Arguments cfAutK [[gT] [G]].
Implicit Arguments cfAutVK [[gT] [G]].
Implicit Arguments cfAut_inj [gT G x1 x2].
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.
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.
Implicit Arguments cfAutK [[gT] [G]].
Implicit Arguments cfAutVK [[gT] [G]].
Implicit Arguments cfAut_inj [gT G x1 x2].
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.