Library mathcomp.character.classfun
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient finalg action gproduct.
From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
From mathcomp Require Import matrix vector falgebra ssrnum algC algnum.
From mathcomp Require Import archimedean.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient finalg action gproduct.
From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
From mathcomp Require Import matrix vector falgebra ssrnum algC algnum.
From mathcomp Require Import archimedean.
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.
Declare Scope cfun_scope.
Import Order.TTheory 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). (* only "''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}.
Local Notation G := <<B>>.
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).
Definition cfun_eqType : eqType := classfun.
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).
Local Notation "''1_' A" := (cfun_indicator A) : ring_scope.
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.
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_ringType : ringType := classfun.
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}.
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}.
Fact cfun_scaleAl a phi psi : a *: (phi × psi) = (a *: phi) × psi.
Fact cfun_scaleAr a phi psi : a *: (phi × psi) = phi × (a *: psi).
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_additive : additive cfAut.
Lemma cfAut_is_multiplicative : multiplicative cfAut.
Lemma cfAut_cfun1 : cfAut 1 = 1.
Lemma cfAut_scalable : scalable_for (u \; *:%R) cfAut.
Definition cfAut_closed (S : seq classfun) :=
{in S, ∀ phi, cfAut phi \in S}.
End Automorphism.
Definition Cfun := locked_with classfun_key (fun flag : nat ⇒ Classfun).
Definition cfun_eqType : eqType := classfun.
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).
Local Notation "''1_' A" := (cfun_indicator A) : ring_scope.
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.
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_ringType : ringType := classfun.
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}.
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}.
Fact cfun_scaleAl a phi psi : a *: (phi × psi) = (a *: phi) × psi.
Fact cfun_scaleAr a phi psi : a *: (phi × psi) = phi × (a *: psi).
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_additive : additive cfAut.
Lemma cfAut_is_multiplicative : multiplicative cfAut.
Lemma cfAut_cfun1 : cfAut 1 = 1.
Lemma cfAut_scalable : scalable_for (u \; *:%R) cfAut.
Definition cfAut_closed (S : seq classfun) :=
{in S, ∀ phi, cfAut phi \in S}.
End Automorphism.
FIX ME this has changed
Notation conjC := Num.conj_op.
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_vectType : vectType _ := 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 psi phi := cfdot phi psi.
Definition cfnorm phi := cfdot phi phi.
Coercion seq_of_cfun phi := [:: phi].
Definition cforder phi := \big[lcmn/1]_(x in <<B>>) #[phi x]%C.
End Defs.
Bind Scope cfun_scope with classfun.
Arguments classfun {gT} B%g.
Arguments classfun_on {gT} B%g A%g.
Arguments cfun_indicator {gT} B%g.
Arguments cfAut {gT B%g} u phi%CF.
Arguments cfReal {gT B%g} phi%CF.
Arguments cfdot {gT B%g} phi%CF psi%CF.
Arguments cfdotr {gT B%g} psi%CF phi%CF /.
Arguments cfnorm {gT B%g} phi%CF /.
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.
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_vectType : vectType _ := 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 psi phi := cfdot phi psi.
Definition cfnorm phi := cfdot phi phi.
Coercion seq_of_cfun phi := [:: phi].
Definition cforder phi := \big[lcmn/1]_(x in <<B>>) #[phi x]%C.
End Defs.
Bind Scope cfun_scope with classfun.
Arguments classfun {gT} B%g.
Arguments classfun_on {gT} B%g A%g.
Arguments cfun_indicator {gT} B%g.
Arguments cfAut {gT B%g} u phi%CF.
Arguments cfReal {gT B%g} phi%CF.
Arguments cfdot {gT B%g} phi%CF psi%CF.
Arguments cfdotr {gT B%g} psi%CF phi%CF /.
Arguments cfnorm {gT B%g} phi%CF /.
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.
FIX ME this has changed
Notation conjC := Num.conj_op.
Notation "phi ^*" := (cfAut conjC phi) : cfun_scope.
Notation cfConjC_closed := (cfAut_closed conjC).
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.
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.
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).
Arguments cfker {gT D%g} phi%CF.
Arguments cfaithful {gT D%g} phi%CF.
Arguments orthogonal {gT D%g} S1%CF S2%CF.
Arguments pairwise_orthogonal {gT D%g} S%CF.
Arguments orthonormal {gT D%g} S%CF.
Arguments isometry {gT rT D%g R%g} tau%CF.
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)).
Local Notation "''1_' A" := (cfun_indicator G A).
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)).
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).
Arguments cfker {gT D%g} phi%CF.
Arguments cfaithful {gT D%g} phi%CF.
Arguments orthogonal {gT D%g} S1%CF S2%CF.
Arguments pairwise_orthogonal {gT D%g} S%CF.
Arguments orthonormal {gT D%g} S%CF.
Arguments isometry {gT rT D%g R%g} tau%CF.
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)).
Local Notation "''1_' A" := (cfun_indicator G A).
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)).
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.
Arguments classfun_on {gT} B%g A%g.
Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
Arguments cfun_onP {gT G A phi}.
Arguments cfConjCK {gT G} phi : rename.
#[global] Hint Resolve cfun_onT : core.
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).
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].
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_leif 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).
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.
Arguments orthoP {gT G phi psi}.
Arguments orthoPl {gT G phi S}.
Arguments orthoPr {gT G S psi}.
Arguments orthogonalP {gT G S R}.
Arguments pairwise_orthogonalP {gT G S}.
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.
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}).
Local Notation H := <<A>>.
Local Notation G := <<B>>.
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.
Lemma cfRes_cfun1 : cfRes 1 = 1.
Lemma cfRes_is_multiplicative : multiplicative cfRes.
End Restrict.
Arguments cfRes {gT} A%g {B%g} phi%CF.
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.
Fact cfMorph_is_multiplicative : multiplicative 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.
Local Notation G1 := (isom_inv isoGR @* R).
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.
Lemma cfIsom_is_additive : additive cfIsom.
Lemma cfIsom_is_multiplicative : multiplicative cfIsom.
Lemma cfIsom_is_scalable : scalable 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.
Arguments cfIsom_inj {aT rT G f R} isoGR [phi1 phi2] : rename.
Section Coset.
Variables (gT : finGroupType) (G : {group gT}) (B : {set gT}).
Implicit Type rT : finGroupType.
Local Notation H := <<B>>%g.
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).
Local Notation "phi / 'B'" := (cfQuo phi) (at level 40) : cfun_scope.
Local Notation "phi %% 'B'" := (cfMod phi) (at level 40) : cfun_scope.
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.
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.
Arguments cfQuo {gT G%G} B%g phi%CF.
Arguments cfMod {gT G%G B%g} phi%CF.
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].
Lemma cfSdprod_is_additive : additive cfSdprod.
Lemma cfSdprod_is_multiplicative : multiplicative cfSdprod.
Lemma cfSdprod_is_scalable : scalable 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.
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].
Lemma cfSdprod_is_additive : additive cfSdprod.
Lemma cfSdprod_is_multiplicative : multiplicative cfSdprod.
Lemma cfSdprod_is_scalable : scalable 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.
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].
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}.
Local Notation G := <<B>>.
Local Notation H := <<A>>.
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].
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}.
Local Notation G := <<B>>.
Local Notation H := <<A>>.
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.
End Def.
Local Notation "''Ind[' B , A ]" := (@cfInd B A) : ring_scope.
Local Notation "''Ind[' B ]" := 'Ind[B, _] : ring_scope.
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.
End Def.
Local Notation "''Ind[' B , A ]" := (@cfInd B A) : ring_scope.
Local Notation "''Ind[' B ]" := 'Ind[B, _] : ring_scope.
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.
Arguments cfInd {gT} B%g {A%g} phi%CF.
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)).
Local Notation "phi ^u" := (cfAut u phi) (at level 3, format "phi ^u").
Lemma cfAutZ_nat n phi : (n%:R *: phi)^u = n%:R *: phi^u.
Lemma cfAutZ_Cnat z phi : z \in Num.nat → (z *: phi)^u = z *: phi^u.
Lemma cfAutZ_Cint z phi : z \in Num.int → (z *: phi)^u = z *: phi^u.
Lemma cfAutK : cancel (@cfAut gT G u) (cfAut (algC_invaut u)).
Lemma cfAutVK : cancel (cfAut (algC_invaut 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.
Arguments cfAutK u {gT G}.
Arguments cfAutVK u {gT G}.
Arguments cfAut_inj u {gT G} [phi1 phi2] : rename.
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.
Arguments cfInd {gT} B%g {A%g} phi%CF.
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)).
Local Notation "phi ^u" := (cfAut u phi) (at level 3, format "phi ^u").
Lemma cfAutZ_nat n phi : (n%:R *: phi)^u = n%:R *: phi^u.
Lemma cfAutZ_Cnat z phi : z \in Num.nat → (z *: phi)^u = z *: phi^u.
Lemma cfAutZ_Cint z phi : z \in Num.int → (z *: phi)^u = z *: phi^u.
Lemma cfAutK : cancel (@cfAut gT G u) (cfAut (algC_invaut u)).
Lemma cfAutVK : cancel (cfAut (algC_invaut 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.
Arguments cfAutK u {gT G}.
Arguments cfAutVK u {gT G}.
Arguments cfAut_inj u {gT G} [phi1 phi2] : rename.
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.