Library mathcomp.character.character
(* (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 notions of character theory, based on Isaacs.
irr G == tuple of the elements of 'CF(G) that are irreducible
characters of G.
Nirr G == number of irreducible characters of G.
Iirr G == index type for the irreducible characters of G.
:= 'I(Nirr G).
'chi_i == the i-th element of irr G, for i : Iirr G.
'chi[G]_i Note that 'chi_0 = 1, the principal character of G.
'Chi_i == an irreducible representation that affords 'chi_i.
socle_of_Iirr i == the Wedderburn component of the regular representation
of G, corresponding to 'Chi_i.
Iirr_of_socle == the inverse of socle_of_Iirr (which is one-to-one).
phi. [A]%CF == the image of A \in group_ring G under phi : 'CF(G).
cfRepr rG == the character afforded by the representation rG of G.
cfReg G == the regular character, afforded by the regular
representation of G.
detRepr rG == the linear character afforded by the determinant of rG.
cfDet phi == the linear character afforded by the determinant of a
representation affording phi.
'o(phi) == the "determinential order" of phi (the multiplicative
order of cfDet phi.
phi \is a character <=> phi : 'CF(G) is a character of G or 0.
i \in irr_constt phi <=> 'chi_i is an irreducible constituent of phi: phi
has a non-zero coordinate on 'chi_i over the basis irr G.
xi \is a linear_char xi <=> xi : 'CF(G) is a linear character of G.
'Z(chi)%CF == the center of chi when chi is a character of G, i.e.,
rcenter rG where rG is a representation that affords phi.
If phi is not a character then 'Z(chi)%CF = cfker phi.
aut_Iirr u i == the index of cfAut u 'chi_i in irr G.
conjC_Iirr i == the index of 'chi_i^*%CF in irr G.
morph_Iirr i == the index of cfMorph 'chi[f @* G]_i in irr G.
isom_Iirr isoG i == the index of cfIsom isoG 'chi[G]_i in irr R.
mod_Iirr i == the index of ('chi[G / H]_i %% H)%CF in irr G.
quo_Iirr i == the index of ('chi[G]_i / H)%CF in irr (G / H).
Ind_Iirr G i == the index of 'Ind[G, H] 'chi_i, provided it is an
irreducible character (such as when if H is the inertia
group of 'chi_i).
Res_Iirr H i == the index of 'Res[H, G] 'chi_i, provided it is an
irreducible character (such as when 'chi_i is linear).
sdprod_Iirr defG i == the index of cfSdprod defG 'chi_i in irr G, given
defG : K ><| H = G.
And, for KxK : K \x H = G.
dprodl_Iirr KxH i == the index of cfDprodl KxH 'chi[K]_i in irr G.
dprodr_Iirr KxH j == the index of cfDprodr KxH 'chi[H]_j in irr G.
dprod_Iirr KxH (i, j) == the index of cfDprod KxH 'chi[K]_i 'chi[H]_j.
inv_dprod_Iirr KxH == the inverse of dprod_Iirr KxH.
The following are used to define and exploit the character table:
character_table G == the character table of G, whose i-th row lists the
values taken by 'chi_i on the conjugacy classes
of G; this is a square Nirr G x NirrG matrix.
irr_class i == the conjugacy class of G with index i : Iirr G.
class_Iirr xG == the index of xG \in classes G, in Iirr G.
Set Implicit Arguments.
Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Section AlgC.
Variable (gT : finGroupType).
Lemma groupC : group_closure_field algCF gT.
End AlgC.
Section Tensor.
Variable (F : fieldType).
Fixpoint trow (n1 : nat) :
∀ (A : 'rV[F]_n1) m2 n2 (B : 'M[F]_(m2,n2)), 'M[F]_(m2,n1 × n2) :=
if n1 is n'1.+1
then
fun (A : 'M[F]_(1,(1 + n'1))) m2 n2 (B : 'M[F]_(m2,n2)) ⇒
(row_mx (lsubmx A 0 0 *: B) (trow (rsubmx A) B))
else (fun _ _ _ _ ⇒ 0).
Lemma trow0 n1 m2 n2 B : @trow n1 0 m2 n2 B = 0.
Definition trowb n1 m2 n2 B A := @trow n1 A m2 n2 B.
Lemma trowbE n1 m2 n2 A B : trowb B A = @trow n1 A m2 n2 B.
Lemma trowb_is_linear n1 m2 n2 (B : 'M_(m2,n2)) : linear (@trowb n1 m2 n2 B).
Canonical Structure trowb_linear n1 m2 n2 B :=
Linear (@trowb_is_linear n1 m2 n2 B).
Lemma trow_is_linear n1 m2 n2 (A : 'rV_n1) : linear (@trow n1 A m2 n2).
Canonical Structure trow_linear n1 m2 n2 A :=
Linear (@trow_is_linear n1 m2 n2 A).
Fixpoint tprod (m1 : nat) :
∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
'M[F]_(m1 × m2,n1 × n2) :=
if m1 is m'1.+1
return ∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
'M[F]_(m1 × m2,n1 × n2)
then
fun n1 (A : 'M[F]_(1 + m'1,n1)) m2 n2 B ⇒
(col_mx (trow (usubmx A) B) (tprod (dsubmx A) B))
else (fun _ _ _ _ _ ⇒ 0).
Lemma dsumx_mul m1 m2 n p A B :
dsubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = dsubmx (A : 'M_(m1 + m2, p)) ×m B.
Lemma usumx_mul m1 m2 n p A B :
usubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = usubmx (A : 'M_(m1 + m2, p)) ×m B.
Let trow_mul (m1 m2 n2 p2 : nat)
(A : 'rV_m1) (B1: 'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
trow A (B1 ×m B2) = B1 ×m trow A B2.
Lemma tprodE m1 n1 p1 (A1 :'M[F]_(m1,n1)) (A2 :'M[F]_(n1,p1))
m2 n2 p2 (B1 :'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
tprod (A1 ×m A2) (B1 ×m B2) = (tprod A1 B1) ×m (tprod A2 B2).
Let tprod_tr m1 n1 (A :'M[F]_(m1, 1 + n1)) m2 n2 (B :'M[F]_(m2, n2)) :
tprod A B = row_mx (trow (lsubmx A)^T B^T)^T (tprod (rsubmx A) B).
Lemma tprod1 m n : tprod (1%:M : 'M[F]_(m,m)) (1%:M : 'M[F]_(n,n)) = 1%:M.
Lemma mxtrace_prod m n (A :'M[F]_(m)) (B :'M[F]_(n)) :
\tr (tprod A B) = \tr A × \tr B.
End Tensor.
Representation sigma type and standard representations.
Section StandardRepresentation.
Variables (R : fieldType) (gT : finGroupType) (G : {group gT}).
Record representation :=
Representation {rdegree; mx_repr_of_repr :> reprG rdegree}.
Lemma mx_repr0 : mx_repr G (fun _ : gT ⇒ 1%:M : 'M[R]_0).
Definition grepr0 := Representation (MxRepresentation mx_repr0).
Lemma add_mx_repr (rG1 rG2 : representation) :
mx_repr G (fun g ⇒ block_mx (rG1 g) 0 0 (rG2 g)).
Definition dadd_grepr rG1 rG2 :=
Representation (MxRepresentation (add_mx_repr rG1 rG2)).
Section DsumRepr.
Variables (n : nat) (rG : reprG n).
Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation)
(modU : mxmodule rG U) (modV : mxmodule rG V) (modW : mxmodule rG W) :
(U + V :=: W)%MS → mxdirect (U + V) →
mx_rsim (submod_repr modU) rU → mx_rsim (submod_repr modV) rV →
mx_rsim (submod_repr modW) (dadd_grepr rU rV).
Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
(modU : ∀ i, mxmodule rG (U i)) (modW : mxmodule rG W) :
let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
(∀ i, mx_rsim (submod_repr (modU i)) (rU i : representation)) →
mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).
Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW.
Lemma mx_rsim_socle (sG : socleType rG) (W : sG) (rW : representation) :
let modW : mxmodule rG W := component_mx_module rG (socle_base W) in
mx_rsim (socle_repr W) rW →
mx_rsim (submod_repr modW) (muln_grepr rW (socle_mult W)).
End DsumRepr.
Section ProdRepr.
Variables (n1 n2 : nat) (rG1 : reprG n1) (rG2 : reprG n2).
Lemma prod_mx_repr : mx_repr G (fun g ⇒ tprod (rG1 g) (rG2 g)).
Definition prod_repr := MxRepresentation prod_mx_repr.
End ProdRepr.
Lemma prod_repr_lin n2 (rG1 : reprG 1) (rG2 : reprG n2) :
{in G, ∀ x, let cast_n2 := esym (mul1n n2) in
prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.
End StandardRepresentation.
Implicit Arguments grepr0 [R gT G].
Section Char.
Variables (gT : finGroupType) (G : {group gT}).
Fact cfRepr_subproof n (rG : mx_representation algCF G n) :
is_class_fun <<G>> [ffun x ⇒ \tr (rG x) *+ (x \in G)].
Definition cfRepr n rG := Cfun 0 (@cfRepr_subproof n rG).
Lemma cfRepr1 n rG : @cfRepr n rG 1%g = n%:R.
Lemma cfRepr_sim n1 n2 rG1 rG2 :
mx_rsim rG1 rG2 → @cfRepr n1 rG1 = @cfRepr n2 rG2.
Lemma cfRepr0 : cfRepr grepr0 = 0.
Lemma cfRepr_dadd rG1 rG2 :
cfRepr (dadd_grepr rG1 rG2) = cfRepr rG1 + cfRepr rG2.
Lemma cfRepr_dsum I r (P : pred I) rG :
cfRepr (\big[dadd_grepr/grepr0]_(i <- r | P i) rG i)
= \sum_(i <- r | P i) cfRepr (rG i).
Lemma cfRepr_muln rG k : cfRepr (muln_grepr rG k) = cfRepr rG *+ k.
Section StandardRepr.
Variables (n : nat) (rG : mx_representation algCF G n).
Let sG := DecSocleType rG.
Let iG : irrType algCF G := DecSocleType _.
Definition standard_irr (W : sG) := irr_comp iG (socle_repr W).
Definition standard_socle i := pick [pred W | standard_irr W == i].
Definition standard_irr_coef i := oapp (fun W ⇒ socle_mult W) 0%N (soc i).
Definition standard_grepr :=
\big[dadd_grepr/grepr0]_i
muln_grepr (Representation (socle_repr i)) (standard_irr_coef i).
Lemma mx_rsim_standard : mx_rsim rG standard_grepr.
End StandardRepr.
Definition cfReg (B : {set gT}) : 'CF(B) := #|B|%:R *: '1_[1].
Lemma cfRegE x : @cfReg G x = #|G|%:R *+ (x == 1%g).
Variables (R : fieldType) (gT : finGroupType) (G : {group gT}).
Record representation :=
Representation {rdegree; mx_repr_of_repr :> reprG rdegree}.
Lemma mx_repr0 : mx_repr G (fun _ : gT ⇒ 1%:M : 'M[R]_0).
Definition grepr0 := Representation (MxRepresentation mx_repr0).
Lemma add_mx_repr (rG1 rG2 : representation) :
mx_repr G (fun g ⇒ block_mx (rG1 g) 0 0 (rG2 g)).
Definition dadd_grepr rG1 rG2 :=
Representation (MxRepresentation (add_mx_repr rG1 rG2)).
Section DsumRepr.
Variables (n : nat) (rG : reprG n).
Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation)
(modU : mxmodule rG U) (modV : mxmodule rG V) (modW : mxmodule rG W) :
(U + V :=: W)%MS → mxdirect (U + V) →
mx_rsim (submod_repr modU) rU → mx_rsim (submod_repr modV) rV →
mx_rsim (submod_repr modW) (dadd_grepr rU rV).
Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
(modU : ∀ i, mxmodule rG (U i)) (modW : mxmodule rG W) :
let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
(∀ i, mx_rsim (submod_repr (modU i)) (rU i : representation)) →
mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).
Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW.
Lemma mx_rsim_socle (sG : socleType rG) (W : sG) (rW : representation) :
let modW : mxmodule rG W := component_mx_module rG (socle_base W) in
mx_rsim (socle_repr W) rW →
mx_rsim (submod_repr modW) (muln_grepr rW (socle_mult W)).
End DsumRepr.
Section ProdRepr.
Variables (n1 n2 : nat) (rG1 : reprG n1) (rG2 : reprG n2).
Lemma prod_mx_repr : mx_repr G (fun g ⇒ tprod (rG1 g) (rG2 g)).
Definition prod_repr := MxRepresentation prod_mx_repr.
End ProdRepr.
Lemma prod_repr_lin n2 (rG1 : reprG 1) (rG2 : reprG n2) :
{in G, ∀ x, let cast_n2 := esym (mul1n n2) in
prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.
End StandardRepresentation.
Implicit Arguments grepr0 [R gT G].
Section Char.
Variables (gT : finGroupType) (G : {group gT}).
Fact cfRepr_subproof n (rG : mx_representation algCF G n) :
is_class_fun <<G>> [ffun x ⇒ \tr (rG x) *+ (x \in G)].
Definition cfRepr n rG := Cfun 0 (@cfRepr_subproof n rG).
Lemma cfRepr1 n rG : @cfRepr n rG 1%g = n%:R.
Lemma cfRepr_sim n1 n2 rG1 rG2 :
mx_rsim rG1 rG2 → @cfRepr n1 rG1 = @cfRepr n2 rG2.
Lemma cfRepr0 : cfRepr grepr0 = 0.
Lemma cfRepr_dadd rG1 rG2 :
cfRepr (dadd_grepr rG1 rG2) = cfRepr rG1 + cfRepr rG2.
Lemma cfRepr_dsum I r (P : pred I) rG :
cfRepr (\big[dadd_grepr/grepr0]_(i <- r | P i) rG i)
= \sum_(i <- r | P i) cfRepr (rG i).
Lemma cfRepr_muln rG k : cfRepr (muln_grepr rG k) = cfRepr rG *+ k.
Section StandardRepr.
Variables (n : nat) (rG : mx_representation algCF G n).
Let sG := DecSocleType rG.
Let iG : irrType algCF G := DecSocleType _.
Definition standard_irr (W : sG) := irr_comp iG (socle_repr W).
Definition standard_socle i := pick [pred W | standard_irr W == i].
Definition standard_irr_coef i := oapp (fun W ⇒ socle_mult W) 0%N (soc i).
Definition standard_grepr :=
\big[dadd_grepr/grepr0]_i
muln_grepr (Representation (socle_repr i)) (standard_irr_coef i).
Lemma mx_rsim_standard : mx_rsim rG standard_grepr.
End StandardRepr.
Definition cfReg (B : {set gT}) : 'CF(B) := #|B|%:R *: '1_[1].
Lemma cfRegE x : @cfReg G x = #|G|%:R *+ (x == 1%g).
This is Isaacs, Lemma (2.10).
Lemma cfReprReg : cfRepr (regular_repr algCF G) = cfReg G.
Definition xcfun (chi : 'CF(G)) A :=
(gring_row A ×m (\col_(i < #|G|) chi (enum_val i))) 0 0.
Lemma xcfun_is_additive phi : additive (xcfun phi).
Canonical xcfun_additive phi := Additive (xcfun_is_additive phi).
Lemma xcfunZr a phi A : xcfun phi (a *: A) = a × xcfun phi A.
Definition xcfun (chi : 'CF(G)) A :=
(gring_row A ×m (\col_(i < #|G|) chi (enum_val i))) 0 0.
Lemma xcfun_is_additive phi : additive (xcfun phi).
Canonical xcfun_additive phi := Additive (xcfun_is_additive phi).
Lemma xcfunZr a phi A : xcfun phi (a *: A) = a × xcfun phi A.
In order to add a second canonical structure on xcfun
Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A.
Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A.
Fact xcfun_r_is_additive A : additive (xcfun_r A).
Canonical xcfun_r_additive A := Additive (xcfun_r_is_additive A).
Lemma xcfunZl a phi A : xcfun (a *: phi) A = a × xcfun phi A.
Lemma xcfun_repr n rG A : xcfun (@cfRepr n rG) A = \tr (gring_op rG A).
End Char.
Notation xcfun_r A := (xcfun_r_head tt A).
Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.
Definition pred_Nirr gT B := #|@classes gT B|.-1.
Notation Nirr G := (pred_Nirr G).+1.
Notation Iirr G := 'I_(Nirr G).
Section IrrClassDef.
Variables (gT : finGroupType) (G : {group gT}).
Let sG := DecSocleType (regular_repr algCF G).
Lemma NirrE : Nirr G = #|classes G|.
Fact Iirr_cast : Nirr G = #|sG|.
Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr).
Definition socle_of_Iirr (i : Iirr G) : sG :=
enum_val (cast_ord Iirr_cast (i + offset)).
Definition irr_of_socle (Wi : sG) : Iirr G :=
cast_ord (esym Iirr_cast) (enum_rank Wi) - offset.
Lemma socle_Iirr0 : W 0 = [1 sG]%irr.
Lemma socle_of_IirrK : cancel W irr_of_socle.
Lemma irr_of_socleK : cancel irr_of_socle W.
Hint Resolve socle_of_IirrK irr_of_socleK.
Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}.
End IrrClassDef.
Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i))
(at level 8, i at level 2, format "''Chi_' i").
Fact irr_key : unit.
Definition irr_def gT B : (Nirr B).-tuple 'CF(B) :=
let irr_of i := 'Res[B, <<B>>] (@cfRepr gT _ _ 'Chi_(inord i)) in
[tuple of mkseq irr_of (Nirr B)].
Definition irr := locked_with irr_key irr_def.
Notation "''chi_' i" := (tnth (irr _) i%R)
(at level 8, i at level 2, format "''chi_' i") : ring_scope.
Notation "''chi[' G ]_ i" := (tnth (irr G) i%R)
(at level 8, i at level 2, only parsing) : ring_scope.
Section IrrClass.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (i : Iirr G) (B : {set gT}).
Open Scope group_ring_scope.
Lemma congr_irr i1 i2 : i1 = i2 → 'chi_i1 = 'chi_i2.
Lemma Iirr1_neq0 : G :!=: 1%g → inord 1 != 0 :> Iirr G.
Lemma has_nonprincipal_irr : G :!=: 1%g → {i : Iirr G | i != 0}.
Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i.
Lemma irr0 : 'chi[G]_0 = 1.
Lemma cfun1_irr : 1 \in irr G.
Lemma mem_irr i : 'chi_i \in irr G.
Lemma irrP xi : reflect (∃ i, xi = 'chi_i) (xi \in irr G).
Let sG := DecSocleType (regular_repr algCF G).
Let C'G := algC'G G.
Let closG := @groupC _ G.
Lemma irr1_degree i : 'chi_i 1%g = ('n_i)%:R.
Lemma Cnat_irr1 i : 'chi_i 1%g \in Cnat.
Lemma irr1_gt0 i : 0 < 'chi_i 1%g.
Lemma irr1_neq0 i : 'chi_i 1%g != 0.
Lemma irr_neq0 i : 'chi_i != 0.
Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)).
Lemma cfIirrE chi : chi \in irr G → 'chi_(cfIirr chi) = chi.
Lemma cfIirrPE J (f : J → 'CF(G)) (P : pred J) :
(∀ j, P j → f j \in irr G) →
∀ j, P j → 'chi_(cfIirr (f j)) = f j.
Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A.
Fact xcfun_r_is_additive A : additive (xcfun_r A).
Canonical xcfun_r_additive A := Additive (xcfun_r_is_additive A).
Lemma xcfunZl a phi A : xcfun (a *: phi) A = a × xcfun phi A.
Lemma xcfun_repr n rG A : xcfun (@cfRepr n rG) A = \tr (gring_op rG A).
End Char.
Notation xcfun_r A := (xcfun_r_head tt A).
Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.
Definition pred_Nirr gT B := #|@classes gT B|.-1.
Notation Nirr G := (pred_Nirr G).+1.
Notation Iirr G := 'I_(Nirr G).
Section IrrClassDef.
Variables (gT : finGroupType) (G : {group gT}).
Let sG := DecSocleType (regular_repr algCF G).
Lemma NirrE : Nirr G = #|classes G|.
Fact Iirr_cast : Nirr G = #|sG|.
Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr).
Definition socle_of_Iirr (i : Iirr G) : sG :=
enum_val (cast_ord Iirr_cast (i + offset)).
Definition irr_of_socle (Wi : sG) : Iirr G :=
cast_ord (esym Iirr_cast) (enum_rank Wi) - offset.
Lemma socle_Iirr0 : W 0 = [1 sG]%irr.
Lemma socle_of_IirrK : cancel W irr_of_socle.
Lemma irr_of_socleK : cancel irr_of_socle W.
Hint Resolve socle_of_IirrK irr_of_socleK.
Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}.
End IrrClassDef.
Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i))
(at level 8, i at level 2, format "''Chi_' i").
Fact irr_key : unit.
Definition irr_def gT B : (Nirr B).-tuple 'CF(B) :=
let irr_of i := 'Res[B, <<B>>] (@cfRepr gT _ _ 'Chi_(inord i)) in
[tuple of mkseq irr_of (Nirr B)].
Definition irr := locked_with irr_key irr_def.
Notation "''chi_' i" := (tnth (irr _) i%R)
(at level 8, i at level 2, format "''chi_' i") : ring_scope.
Notation "''chi[' G ]_ i" := (tnth (irr G) i%R)
(at level 8, i at level 2, only parsing) : ring_scope.
Section IrrClass.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (i : Iirr G) (B : {set gT}).
Open Scope group_ring_scope.
Lemma congr_irr i1 i2 : i1 = i2 → 'chi_i1 = 'chi_i2.
Lemma Iirr1_neq0 : G :!=: 1%g → inord 1 != 0 :> Iirr G.
Lemma has_nonprincipal_irr : G :!=: 1%g → {i : Iirr G | i != 0}.
Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i.
Lemma irr0 : 'chi[G]_0 = 1.
Lemma cfun1_irr : 1 \in irr G.
Lemma mem_irr i : 'chi_i \in irr G.
Lemma irrP xi : reflect (∃ i, xi = 'chi_i) (xi \in irr G).
Let sG := DecSocleType (regular_repr algCF G).
Let C'G := algC'G G.
Let closG := @groupC _ G.
Lemma irr1_degree i : 'chi_i 1%g = ('n_i)%:R.
Lemma Cnat_irr1 i : 'chi_i 1%g \in Cnat.
Lemma irr1_gt0 i : 0 < 'chi_i 1%g.
Lemma irr1_neq0 i : 'chi_i 1%g != 0.
Lemma irr_neq0 i : 'chi_i != 0.
Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)).
Lemma cfIirrE chi : chi \in irr G → 'chi_(cfIirr chi) = chi.
Lemma cfIirrPE J (f : J → 'CF(G)) (P : pred J) :
(∀ j, P j → f j \in irr G) →
∀ j, P j → 'chi_(cfIirr (f j)) = f j.
This is Isaacs, Corollary (2.7).
This is Isaacs, Lemma (2.11).
Lemma cfReg_sum : cfReg G = \sum_i 'chi_i 1%g *: 'chi_i.
Let aG := regular_repr algCF G.
Let R_G := group_ring algCF G.
Lemma xcfun_annihilate i j A : i != j → (A \in 'R_j)%MS → ('chi_i).[A]%CF = 0.
Lemma xcfunG phi x : x \in G → phi.[aG x]%CF = phi x.
Lemma xcfun_mul_id i A :
(A \in R_G)%MS → ('chi_i).['e_i ×m A]%CF = ('chi_i).[A]%CF.
Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j).
Lemma irr_free : free (irr G).
Lemma irr_inj : injective (tnth (irr G)).
Lemma irrK : cancel (tnth (irr G)) (@cfIirr G).
Lemma irr_eq1 i : ('chi_i == 1) = (i == 0).
Lemma cforder_irr_eq1 i : (#['chi_i]%CF == 1%N) = (i == 0).
Lemma irr_basis : basis_of 'CF(G)%VS (irr G).
Lemma eq_sum_nth_irr a : \sum_i a i *: 'chi[G]_i = \sum_i a i *: (irr G)`_i.
Let aG := regular_repr algCF G.
Let R_G := group_ring algCF G.
Lemma xcfun_annihilate i j A : i != j → (A \in 'R_j)%MS → ('chi_i).[A]%CF = 0.
Lemma xcfunG phi x : x \in G → phi.[aG x]%CF = phi x.
Lemma xcfun_mul_id i A :
(A \in R_G)%MS → ('chi_i).['e_i ×m A]%CF = ('chi_i).[A]%CF.
Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j).
Lemma irr_free : free (irr G).
Lemma irr_inj : injective (tnth (irr G)).
Lemma irrK : cancel (tnth (irr G)) (@cfIirr G).
Lemma irr_eq1 i : ('chi_i == 1) = (i == 0).
Lemma cforder_irr_eq1 i : (#['chi_i]%CF == 1%N) = (i == 0).
Lemma irr_basis : basis_of 'CF(G)%VS (irr G).
Lemma eq_sum_nth_irr a : \sum_i a i *: 'chi[G]_i = \sum_i a i *: (irr G)`_i.
This is Isaacs, Theorem (2.8).
Theorem cfun_irr_sum phi : {a | phi = \sum_i a i *: 'chi[G]_i}.
Lemma cfRepr_standard n (rG : mx_representation algCF G n) :
cfRepr (standard_grepr rG)
= \sum_i (standard_irr_coef rG (W i))%:R *: 'chi_i.
Lemma cfRepr_inj n1 n2 rG1 rG2 :
@cfRepr _ G n1 rG1 = @cfRepr _ G n2 rG2 → mx_rsim rG1 rG2.
Lemma cfRepr_rsimP n1 n2 rG1 rG2 :
reflect (mx_rsim rG1 rG2) (@cfRepr _ G n1 rG1 == @cfRepr _ G n2 rG2).
Lemma irr_reprP xi :
reflect (exists2 rG : representation _ G, mx_irreducible rG & xi = cfRepr rG)
(xi \in irr G).
Lemma cfRepr_standard n (rG : mx_representation algCF G n) :
cfRepr (standard_grepr rG)
= \sum_i (standard_irr_coef rG (W i))%:R *: 'chi_i.
Lemma cfRepr_inj n1 n2 rG1 rG2 :
@cfRepr _ G n1 rG1 = @cfRepr _ G n2 rG2 → mx_rsim rG1 rG2.
Lemma cfRepr_rsimP n1 n2 rG1 rG2 :
reflect (mx_rsim rG1 rG2) (@cfRepr _ G n1 rG1 == @cfRepr _ G n2 rG2).
Lemma irr_reprP xi :
reflect (exists2 rG : representation _ G, mx_irreducible rG & xi = cfRepr rG)
(xi \in irr G).
This is Isaacs, Theorem (2.12).
Lemma Wedderburn_id_expansion i :
'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g × 'chi_i x^-1%g *: aG x.
End IrrClass.
Implicit Arguments irr_inj [[gT] [G] x1 x2].
Section IsChar.
Variable gT : finGroupType.
Definition character {G : {set gT}} :=
[qualify a phi : 'CF(G) | [∀ i, coord (irr G) i phi \in Cnat]].
Fact character_key G : pred_key (@character G).
Canonical character_keyed G := KeyedQualifier (character_key G).
Variable G : {group gT}.
Implicit Types (phi chi xi : 'CF(G)) (i : Iirr G).
Lemma irr_char i : 'chi_i \is a character.
Lemma cfun1_char : (1 : 'CF(G)) \is a character.
Lemma cfun0_char : (0 : 'CF(G)) \is a character.
Fact add_char : addr_closed (@character G).
Canonical character_addrPred := AddrPred add_char.
Lemma char_sum_irrP {phi} :
reflect (∃ n, phi = \sum_i (n i)%:R *: 'chi_i) (phi \is a character).
Lemma char_sum_irr chi :
chi \is a character → {r | chi = \sum_(i <- r) 'chi_i}.
Lemma Cnat_char1 chi : chi \is a character → chi 1%g \in Cnat.
Lemma char1_ge0 chi : chi \is a character → 0 ≤ chi 1%g.
Lemma char1_eq0 chi : chi \is a character → (chi 1%g == 0) = (chi == 0).
Lemma char1_gt0 chi : chi \is a character → (0 < chi 1%g) = (chi != 0).
Lemma char_reprP phi :
reflect (∃ rG : representation algCF G, phi = cfRepr rG)
(phi \is a character).
Lemma cfRepr_char n (rG : reprG n) : cfRepr rG \is a character.
Lemma cfReg_char : cfReg G \is a character.
Lemma cfRepr_prod n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
cfRepr rG1 × cfRepr rG2 = cfRepr (prod_repr rG1 rG2).
Lemma mul_char : mulr_closed (@character G).
Canonical char_mulrPred := MulrPred mul_char.
Canonical char_semiringPred := SemiringPred mul_char.
End IsChar.
Implicit Arguments char_reprP [gT G phi].
Section AutChar.
Variables (gT : finGroupType) (G : {group gT}).
Implicit Type u : {rmorphism algC → algC}.
Implicit Type chi : 'CF(G).
Lemma cfRepr_map u n (rG : mx_representation algCF G n) :
cfRepr (map_repr u rG) = cfAut u (cfRepr rG).
Lemma cfAut_char u chi : (cfAut u chi \is a character) = (chi \is a character).
Lemma cfConjC_char chi : (chi^*%CF \is a character) = (chi \is a character).
Lemma cfAut_char1 u (chi : 'CF(G)) :
chi \is a character → cfAut u chi 1%g = chi 1%g.
Lemma cfAut_irr1 u i : (cfAut u 'chi[G]_i) 1%g = 'chi_i 1%g.
Lemma cfConjC_char1 (chi : 'CF(G)) :
chi \is a character → chi^*%CF 1%g = chi 1%g.
Lemma cfConjC_irr1 u i : ('chi[G]_i)^*%CF 1%g = 'chi_i 1%g.
End AutChar.
Section Linear.
Variables (gT : finGroupType) (G : {group gT}).
Definition linear_char {B : {set gT}} :=
[qualify a phi : 'CF(B) | (phi \is a character) && (phi 1%g == 1)].
Section OneChar.
Variable xi : 'CF(G).
Hypothesis CFxi : xi \is a linear_char.
Lemma lin_char1: xi 1%g = 1.
Lemma lin_charW : xi \is a character.
Lemma cfun1_lin_char : (1 : 'CF(G)) \is a linear_char.
Lemma lin_charM : {in G &, {morph xi : x y / (x × y)%g >-> x × y}}.
Lemma lin_char_prod I r (P : pred I) (x : I → gT) :
(∀ i, P i → x i \in G) →
xi (\prod_(i <- r | P i) x i)%g = \prod_(i <- r | P i) xi (x i).
Let xiMV x : x \in G → xi x × xi (x^-1)%g = 1.
Lemma lin_char_neq0 x : x \in G → xi x != 0.
Lemma lin_charV x : x \in G → xi x^-1%g = (xi x)^-1.
Lemma lin_charX x n : x \in G → xi (x ^+ n)%g = xi x ^+ n.
Lemma lin_char_unity_root x : x \in G → xi x ^+ #[x] = 1.
Lemma normC_lin_char x : x \in G → `|xi x| = 1.
Lemma lin_charV_conj x : x \in G → xi x^-1%g = (xi x)^*.
Lemma lin_char_irr : xi \in irr G.
Lemma mul_conjC_lin_char : xi × xi^*%CF = 1.
Lemma lin_char_unitr : xi \in GRing.unit.
Lemma invr_lin_char : xi^-1 = xi^*%CF.
Lemma fful_lin_char_inj : cfaithful xi → {in G &, injective xi}.
End OneChar.
Lemma cfAut_lin_char u (xi : 'CF(G)) :
(cfAut u xi \is a linear_char) = (xi \is a linear_char).
Lemma cfConjC_lin_char (xi : 'CF(G)) :
(xi^*%CF \is a linear_char) = (xi \is a linear_char).
Lemma card_Iirr_abelian : abelian G → #|Iirr G| = #|G|.
Lemma card_Iirr_cyclic : cyclic G → #|Iirr G| = #|G|.
Lemma char_abelianP :
reflect (∀ i : Iirr G, 'chi_i \is a linear_char) (abelian G).
Lemma irr_repr_lin_char (i : Iirr G) x :
x \in G → 'chi_i \is a linear_char →
irr_repr (socle_of_Iirr i) x = ('chi_i x)%:M.
Fact linear_char_key B : pred_key (@linear_char B).
Canonical linear_char_keted B := KeyedQualifier (linear_char_key B).
Fact linear_char_divr : divr_closed (@linear_char G).
Canonical lin_char_mulrPred := MulrPred linear_char_divr.
Canonical lin_char_divrPred := DivrPred linear_char_divr.
Lemma irr_cyclic_lin i : cyclic G → 'chi[G]_i \is a linear_char.
Lemma irr_prime_lin i : prime #|G| → 'chi[G]_i \is a linear_char.
End Linear.
Section OrthogonalityRelations.
Variables aT gT : finGroupType.
'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g × 'chi_i x^-1%g *: aG x.
End IrrClass.
Implicit Arguments irr_inj [[gT] [G] x1 x2].
Section IsChar.
Variable gT : finGroupType.
Definition character {G : {set gT}} :=
[qualify a phi : 'CF(G) | [∀ i, coord (irr G) i phi \in Cnat]].
Fact character_key G : pred_key (@character G).
Canonical character_keyed G := KeyedQualifier (character_key G).
Variable G : {group gT}.
Implicit Types (phi chi xi : 'CF(G)) (i : Iirr G).
Lemma irr_char i : 'chi_i \is a character.
Lemma cfun1_char : (1 : 'CF(G)) \is a character.
Lemma cfun0_char : (0 : 'CF(G)) \is a character.
Fact add_char : addr_closed (@character G).
Canonical character_addrPred := AddrPred add_char.
Lemma char_sum_irrP {phi} :
reflect (∃ n, phi = \sum_i (n i)%:R *: 'chi_i) (phi \is a character).
Lemma char_sum_irr chi :
chi \is a character → {r | chi = \sum_(i <- r) 'chi_i}.
Lemma Cnat_char1 chi : chi \is a character → chi 1%g \in Cnat.
Lemma char1_ge0 chi : chi \is a character → 0 ≤ chi 1%g.
Lemma char1_eq0 chi : chi \is a character → (chi 1%g == 0) = (chi == 0).
Lemma char1_gt0 chi : chi \is a character → (0 < chi 1%g) = (chi != 0).
Lemma char_reprP phi :
reflect (∃ rG : representation algCF G, phi = cfRepr rG)
(phi \is a character).
Lemma cfRepr_char n (rG : reprG n) : cfRepr rG \is a character.
Lemma cfReg_char : cfReg G \is a character.
Lemma cfRepr_prod n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
cfRepr rG1 × cfRepr rG2 = cfRepr (prod_repr rG1 rG2).
Lemma mul_char : mulr_closed (@character G).
Canonical char_mulrPred := MulrPred mul_char.
Canonical char_semiringPred := SemiringPred mul_char.
End IsChar.
Implicit Arguments char_reprP [gT G phi].
Section AutChar.
Variables (gT : finGroupType) (G : {group gT}).
Implicit Type u : {rmorphism algC → algC}.
Implicit Type chi : 'CF(G).
Lemma cfRepr_map u n (rG : mx_representation algCF G n) :
cfRepr (map_repr u rG) = cfAut u (cfRepr rG).
Lemma cfAut_char u chi : (cfAut u chi \is a character) = (chi \is a character).
Lemma cfConjC_char chi : (chi^*%CF \is a character) = (chi \is a character).
Lemma cfAut_char1 u (chi : 'CF(G)) :
chi \is a character → cfAut u chi 1%g = chi 1%g.
Lemma cfAut_irr1 u i : (cfAut u 'chi[G]_i) 1%g = 'chi_i 1%g.
Lemma cfConjC_char1 (chi : 'CF(G)) :
chi \is a character → chi^*%CF 1%g = chi 1%g.
Lemma cfConjC_irr1 u i : ('chi[G]_i)^*%CF 1%g = 'chi_i 1%g.
End AutChar.
Section Linear.
Variables (gT : finGroupType) (G : {group gT}).
Definition linear_char {B : {set gT}} :=
[qualify a phi : 'CF(B) | (phi \is a character) && (phi 1%g == 1)].
Section OneChar.
Variable xi : 'CF(G).
Hypothesis CFxi : xi \is a linear_char.
Lemma lin_char1: xi 1%g = 1.
Lemma lin_charW : xi \is a character.
Lemma cfun1_lin_char : (1 : 'CF(G)) \is a linear_char.
Lemma lin_charM : {in G &, {morph xi : x y / (x × y)%g >-> x × y}}.
Lemma lin_char_prod I r (P : pred I) (x : I → gT) :
(∀ i, P i → x i \in G) →
xi (\prod_(i <- r | P i) x i)%g = \prod_(i <- r | P i) xi (x i).
Let xiMV x : x \in G → xi x × xi (x^-1)%g = 1.
Lemma lin_char_neq0 x : x \in G → xi x != 0.
Lemma lin_charV x : x \in G → xi x^-1%g = (xi x)^-1.
Lemma lin_charX x n : x \in G → xi (x ^+ n)%g = xi x ^+ n.
Lemma lin_char_unity_root x : x \in G → xi x ^+ #[x] = 1.
Lemma normC_lin_char x : x \in G → `|xi x| = 1.
Lemma lin_charV_conj x : x \in G → xi x^-1%g = (xi x)^*.
Lemma lin_char_irr : xi \in irr G.
Lemma mul_conjC_lin_char : xi × xi^*%CF = 1.
Lemma lin_char_unitr : xi \in GRing.unit.
Lemma invr_lin_char : xi^-1 = xi^*%CF.
Lemma fful_lin_char_inj : cfaithful xi → {in G &, injective xi}.
End OneChar.
Lemma cfAut_lin_char u (xi : 'CF(G)) :
(cfAut u xi \is a linear_char) = (xi \is a linear_char).
Lemma cfConjC_lin_char (xi : 'CF(G)) :
(xi^*%CF \is a linear_char) = (xi \is a linear_char).
Lemma card_Iirr_abelian : abelian G → #|Iirr G| = #|G|.
Lemma card_Iirr_cyclic : cyclic G → #|Iirr G| = #|G|.
Lemma char_abelianP :
reflect (∀ i : Iirr G, 'chi_i \is a linear_char) (abelian G).
Lemma irr_repr_lin_char (i : Iirr G) x :
x \in G → 'chi_i \is a linear_char →
irr_repr (socle_of_Iirr i) x = ('chi_i x)%:M.
Fact linear_char_key B : pred_key (@linear_char B).
Canonical linear_char_keted B := KeyedQualifier (linear_char_key B).
Fact linear_char_divr : divr_closed (@linear_char G).
Canonical lin_char_mulrPred := MulrPred linear_char_divr.
Canonical lin_char_divrPred := DivrPred linear_char_divr.
Lemma irr_cyclic_lin i : cyclic G → 'chi[G]_i \is a linear_char.
Lemma irr_prime_lin i : prime #|G| → 'chi[G]_i \is a linear_char.
End Linear.
Section OrthogonalityRelations.
Variables aT gT : finGroupType.
This is Isaacs, Lemma (2.15)
Lemma repr_rsim_diag (G : {group gT}) f (rG : mx_representation algCF G f) x :
x \in G → let chi := cfRepr rG in
∃ e,
[/\ (*a*) exists2 B, B \in unitmx & rG x = invmx B ×m diag_mx e ×m B,
(*b*) (∀ i, e 0 i ^+ #[x] = 1) ∧ (∀ i, `|e 0 i| = 1),
(*c*) chi x = \sum_i e 0 i ∧ `|chi x| ≤ chi 1%g
& (*d*) chi x^-1%g = (chi x)^*].
Variables (A : {group aT}) (G : {group gT}).
x \in G → let chi := cfRepr rG in
∃ e,
[/\ (*a*) exists2 B, B \in unitmx & rG x = invmx B ×m diag_mx e ×m B,
(*b*) (∀ i, e 0 i ^+ #[x] = 1) ∧ (∀ i, `|e 0 i| = 1),
(*c*) chi x = \sum_i e 0 i ∧ `|chi x| ≤ chi 1%g
& (*d*) chi x^-1%g = (chi x)^*].
Variables (A : {group aT}) (G : {group gT}).
This is Isaacs, Lemma (2.15) (d).
Lemma char_inv (chi : 'CF(G)) x : chi \is a character → chi x^-1%g = (chi x)^*.
Lemma irr_inv i x : 'chi[G]_i x^-1%g = ('chi_i x)^*.
Lemma irr_inv i x : 'chi[G]_i x^-1%g = ('chi_i x)^*.
This is Isaacs, Theorem (2.13).
Theorem generalized_orthogonality_relation y (i j : Iirr G) :
#|G|%:R^-1 × (\sum_(x in G) 'chi_i (x × y)%g × 'chi_j x^-1%g)
= (i == j)%:R × ('chi_i y / 'chi_i 1%g).
#|G|%:R^-1 × (\sum_(x in G) 'chi_i (x × y)%g × 'chi_j x^-1%g)
= (i == j)%:R × ('chi_i y / 'chi_i 1%g).
This is Isaacs, Corollary (2.14).
Corollary first_orthogonality_relation (i j : Iirr G) :
#|G|%:R^-1 × (\sum_(x in G) 'chi_i x × 'chi_j x^-1%g) = (i == j)%:R.
#|G|%:R^-1 × (\sum_(x in G) 'chi_i x × 'chi_j x^-1%g) = (i == j)%:R.
The character table.
Definition irr_class i := enum_val (cast_ord (NirrE G) i).
Definition class_Iirr xG :=
cast_ord (esym (NirrE G)) (enum_rank_in (classes1 G) xG).
Definition character_table := \matrix_(i, j) 'chi[G]_i (g j).
Lemma irr_classP i : c i \in classes G.
Lemma repr_irr_classK i : g i ^: G = c i.
Lemma irr_classK : cancel c iC.
Lemma class_IirrK : {in classes G, cancel iC c}.
Lemma reindex_irr_class R idx (op : @Monoid.com_law R idx) F :
\big[op/idx]_(xG in classes G) F xG = \big[op/idx]_i F (c i).
The explicit value of the inverse is needed for the proof of the second
orthogonality relation.
Let X' := \matrix_(i, j) (#|'C_G[g i]|%:R^-1 × ('chi[G]_j (g i))^*).
Let XX'_1: X ×m X' = 1%:M.
Lemma character_table_unit : X \in unitmx.
Let uX := character_table_unit.
Let XX'_1: X ×m X' = 1%:M.
Lemma character_table_unit : X \in unitmx.
Let uX := character_table_unit.
This is Isaacs, Theorem (2.18).
Theorem second_orthogonality_relation x y :
y \in G →
\sum_i 'chi[G]_i x × ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).
Lemma eq_irr_mem_classP x y :
y \in G → reflect (∀ i, 'chi[G]_i x = 'chi_i y) (x \in y ^: G).
y \in G →
\sum_i 'chi[G]_i x × ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).
Lemma eq_irr_mem_classP x y :
y \in G → reflect (∀ i, 'chi[G]_i x = 'chi_i y) (x \in y ^: G).
This is Isaacs, Theorem (6.32) (due to Brauer).
Lemma card_afix_irr_classes (ito : action A (Iirr G)) (cto : action A _) a :
a \in A → [acts A, on classes G | cto] →
(∀ i x y, x \in G → y \in cto (x ^: G) a →
'chi_i x = 'chi_(ito i a) y) →
#|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.
End OrthogonalityRelations.
Section InnerProduct.
Variable (gT : finGroupType) (G : {group gT}).
Lemma cfdot_irr i j : '['chi_i, 'chi_j]_G = (i == j)%:R.
Lemma cfnorm_irr i : '['chi[G]_i] = 1.
Lemma irr_orthonormal : orthonormal (irr G).
Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i].
Lemma cfun_sum_cfdot phi : phi = \sum_i '[phi, 'chi_i]_G *: 'chi_i.
Lemma cfdot_sum_irr phi psi :
'[phi, psi]_G = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i]^*.
Lemma Cnat_cfdot_char_irr i phi :
phi \is a character → '[phi, 'chi_i]_G \in Cnat.
Lemma cfdot_char_r phi chi :
chi \is a character → '[phi, chi]_G = \sum_i '[phi, 'chi_i] × '[chi, 'chi_i].
Lemma Cnat_cfdot_char chi xi :
chi \is a character → xi \is a character → '[chi, xi]_G \in Cnat.
Lemma cfdotC_char chi xi :
chi \is a character→ xi \is a character → '[chi, xi]_G = '[xi, chi].
Lemma irrEchar chi : (chi \in irr G) = (chi \is a character) && ('[chi] == 1).
Lemma irrWchar chi : chi \in irr G → chi \is a character.
Lemma irrWnorm chi : chi \in irr G → '[chi] = 1.
Lemma mul_lin_irr xi chi :
xi \is a linear_char → chi \in irr G → xi × chi \in irr G.
Lemma eq_scaled_irr a b i j :
(a *: 'chi[G]_i == b *: 'chi_j) = (a == b) && ((a == 0) || (i == j)).
Lemma eq_signed_irr (s t : bool) i j :
((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j).
Lemma eq_scale_irr a (i j : Iirr G) :
(a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j).
Lemma eq_addZ_irr a b (i j r t : Iirr G) :
(a *: 'chi_i + b *: 'chi_j == a *: 'chi_r + b *: 'chi_t)
= [|| [&& (a == 0) || (i == r) & (b == 0) || (j == t)],
[&& i == t, j == r & a == b] | [&& i == j, r == t & a == - b]].
Lemma eq_subZnat_irr (a b : nat) (i j r t : Iirr G) :
(a%:R *: 'chi_i - b%:R *: 'chi_j == a%:R *: 'chi_r - b%:R *: 'chi_t)
= [|| a == 0%N | i == r] && [|| b == 0%N | j == t]
|| [&& i == j, r == t & a == b].
End InnerProduct.
Section IrrConstt.
Variable (gT : finGroupType) (G H : {group gT}).
Lemma char1_ge_norm (chi : 'CF(G)) x :
chi \is a character → `|chi x| ≤ chi 1%g.
Lemma max_cfRepr_norm_scalar n (rG : mx_representation algCF G n) x :
x \in G → `|cfRepr rG x| = cfRepr rG 1%g →
exists2 c, `|c| = 1 & rG x = c%:M.
Lemma max_cfRepr_mx1 n (rG : mx_representation algCF G n) x :
x \in G → cfRepr rG x = cfRepr rG 1%g → rG x = 1%:M.
Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0].
Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0).
Lemma constt_charP (i : Iirr G) chi :
chi \is a character →
reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi')
(i \in irr_constt chi).
Lemma cfun_sum_constt (phi : 'CF(G)) :
phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i.
Lemma neq0_has_constt (phi : 'CF(G)) :
phi != 0 → ∃ i, i \in irr_constt phi.
Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i.
Lemma char1_ge_constt (i : Iirr G) chi :
chi \is a character → i \in irr_constt chi → 'chi_i 1%g ≤ chi 1%g.
Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
phi \is a character → psi \is a character →
i \in irr_constt phi → j \in irr_constt psi →
'[phi, psi] = 0 → '['chi_i, 'chi_j] = 0.
End IrrConstt.
Section Kernel.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}).
Lemma cfker_repr n (rG : mx_representation algCF G n) :
cfker (cfRepr rG) = rker rG.
Lemma cfkerEchar chi :
chi \is a character → cfker chi = [set x in G | chi x == chi 1%g].
Lemma cfker_nzcharE chi :
chi \is a character → chi != 0 → cfker chi = [set x | chi x == chi 1%g].
Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g].
Lemma cfker_irr0 : cfker 'chi[G]_0 = G.
Lemma cfaithful_reg : cfaithful (cfReg G).
Lemma cfkerE chi :
chi \is a character →
cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i.
Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1].
Lemma cfker_constt i chi :
chi \is a character → i \in irr_constt chi →
cfker chi \subset cfker 'chi[G]_i.
Section KerLin.
Variable xi : 'CF(G).
Hypothesis lin_xi : xi \is a linear_char.
Let Nxi: xi \is a character.
Lemma lin_char_der1 : G^`(1)%g \subset cfker xi.
Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g.
Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|.
Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N.
End KerLin.
End Kernel.
Section Restrict.
Variable (gT : finGroupType) (G H : {group gT}).
Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) :
cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG).
Lemma cfRes_char chi : chi \is a character → 'Res[H, G] chi \is a character.
Lemma cfRes_eq0 phi : phi \is a character → ('Res[H, G] phi == 0) = (phi == 0).
Lemma cfRes_lin_char chi :
chi \is a linear_char → 'Res[H, G] chi \is a linear_char.
Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0.
Lemma cfRes_lin_lin (chi : 'CF(G)) :
chi \is a character → 'Res[H] chi \is a linear_char → chi \is a linear_char.
Lemma cfRes_irr_irr chi :
chi \is a character → 'Res[H] chi \in irr H → chi \in irr G.
Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i).
Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0.
Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
End Restrict.
Section MoreConstt.
Variables (gT : finGroupType) (G H : {group gT}).
Lemma constt_Ind_Res i j :
i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)).
Lemma cfdot_Res_ge_constt i j psi :
psi \is a character → j \in irr_constt psi →
'['Res[H, G] 'chi_j, 'chi_i] ≤ '['Res[H] psi, 'chi_i].
Lemma constt_Res_trans j psi :
psi \is a character → j \in irr_constt psi →
{subset irr_constt ('Res[H, G] 'chi_j) ≤ irr_constt ('Res[H] psi)}.
End MoreConstt.
Section Morphim.
Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Implicit Type chi : 'CF(f @* G).
Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD :
cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG).
Lemma cfMorph_char chi : chi \is a character → cfMorph chi \is a character.
Lemma cfMorph_lin_char chi :
chi \is a linear_char → cfMorph chi \is a linear_char.
Lemma cfMorph_charE chi :
G \subset D → (cfMorph chi \is a character) = (chi \is a character).
Lemma cfMorph_lin_charE chi :
G \subset D → (cfMorph chi \is a linear_char) = (chi \is a linear_char).
Lemma cfMorph_irr chi :
G \subset D → (cfMorph chi \in irr G) = (chi \in irr (f @* G)).
Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i).
Lemma morph_Iirr0 : morph_Iirr 0 = 0.
Hypothesis sGD : G \subset D.
Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i.
Lemma morph_Iirr_inj : injective morph_Iirr.
Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0).
End Morphim.
Section Isom.
Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
Variables (R : {group rT}) (isoGR : isom G R f).
Implicit Type chi : 'CF(G).
Lemma cfIsom_char chi :
(cfIsom isoGR chi \is a character) = (chi \is a character).
Lemma cfIsom_lin_char chi :
(cfIsom isoGR chi \is a linear_char) = (chi \is a linear_char).
Lemma cfIsom_irr chi : (cfIsom isoGR chi \in irr R) = (chi \in irr G).
Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i).
Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i.
Lemma isom_Iirr_inj : injective isom_Iirr.
Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0).
Lemma isom_Iirr0 : isom_Iirr 0 = 0.
End Isom.
Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2].
Section IsomInv.
Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
Variables (R : {group rT}) (isoGR : isom G R f).
Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)).
Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR).
End IsomInv.
Section Sdprod.
Variables (gT : finGroupType) (K H G : {group gT}).
Hypothesis defG : K ><| H = G.
Let nKG: G \subset 'N(K).
Lemma cfSdprod_char chi :
(cfSdprod defG chi \is a character) = (chi \is a character).
Lemma cfSdprod_lin_char chi :
(cfSdprod defG chi \is a linear_char) = (chi \is a linear_char).
Lemma cfSdprod_irr chi : (cfSdprod defG chi \in irr G) = (chi \in irr H).
Definition sdprod_Iirr j := cfIirr (cfSdprod defG 'chi_j).
Lemma sdprod_IirrE j : 'chi_(sdprod_Iirr j) = cfSdprod defG 'chi_j.
Lemma sdprod_IirrK : cancel sdprod_Iirr (Res_Iirr H).
Lemma sdprod_Iirr_inj : injective sdprod_Iirr.
Lemma sdprod_Iirr_eq0 i : (sdprod_Iirr i == 0) = (i == 0).
Lemma sdprod_Iirr0 : sdprod_Iirr 0 = 0.
Lemma Res_sdprod_irr phi :
K \subset cfker phi → phi \in irr G → 'Res phi \in irr H.
Lemma sdprod_Res_IirrE i :
K \subset cfker 'chi[G]_i → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
Lemma sdprod_Res_IirrK i :
K \subset cfker 'chi_i → sdprod_Iirr (Res_Iirr H i) = i.
End Sdprod.
Implicit Arguments sdprod_Iirr_inj [gT K H G x1 x2].
Section DProd.
Variables (gT : finGroupType) (G K H : {group gT}).
Hypothesis KxH : K \x H = G.
Lemma cfDprodKl_abelian j : abelian H → cancel ((cfDprod KxH)^~ 'chi_j) 'Res.
Lemma cfDprodKr_abelian i : abelian K → cancel (cfDprod KxH 'chi_i) 'Res.
Lemma cfDprodl_char phi :
(cfDprodl KxH phi \is a character) = (phi \is a character).
Lemma cfDprodr_char psi :
(cfDprodr KxH psi \is a character) = (psi \is a character).
Lemma cfDprod_char phi psi :
phi \is a character → psi \is a character →
cfDprod KxH phi psi \is a character.
Lemma cfDprod_eq1 phi psi :
phi \is a character → psi \is a character →
(cfDprod KxH phi psi == 1) = (phi == 1) && (psi == 1).
Lemma cfDprodl_lin_char phi :
(cfDprodl KxH phi \is a linear_char) = (phi \is a linear_char).
Lemma cfDprodr_lin_char psi :
(cfDprodr KxH psi \is a linear_char) = (psi \is a linear_char).
Lemma cfDprod_lin_char phi psi :
phi \is a linear_char → psi \is a linear_char →
cfDprod KxH phi psi \is a linear_char.
Lemma cfDprodl_irr chi : (cfDprodl KxH chi \in irr G) = (chi \in irr K).
Lemma cfDprodr_irr chi : (cfDprodr KxH chi \in irr G) = (chi \in irr H).
Definition dprodl_Iirr i := cfIirr (cfDprodl KxH 'chi_i).
Lemma dprodl_IirrE i : 'chi_(dprodl_Iirr i) = cfDprodl KxH 'chi_i.
Lemma dprodl_IirrK : cancel dprodl_Iirr (Res_Iirr K).
Lemma dprodl_Iirr_eq0 i : (dprodl_Iirr i == 0) = (i == 0).
Lemma dprodl_Iirr0 : dprodl_Iirr 0 = 0.
Definition dprodr_Iirr j := cfIirr (cfDprodr KxH 'chi_j).
Lemma dprodr_IirrE j : 'chi_(dprodr_Iirr j) = cfDprodr KxH 'chi_j.
Lemma dprodr_IirrK : cancel dprodr_Iirr (Res_Iirr H).
Lemma dprodr_Iirr_eq0 j : (dprodr_Iirr j == 0) = (j == 0).
Lemma dprodr_Iirr0 : dprodr_Iirr 0 = 0.
Lemma cfDprod_irr i j : cfDprod KxH 'chi_i 'chi_j \in irr G.
Definition dprod_Iirr ij := cfIirr (cfDprod KxH 'chi_ij.1 'chi_ij.2).
Lemma dprod_IirrE i j : 'chi_(dprod_Iirr (i, j)) = cfDprod KxH 'chi_i 'chi_j.
Lemma dprod_IirrEl i : 'chi_(dprod_Iirr (i, 0)) = cfDprodl KxH 'chi_i.
Lemma dprod_IirrEr j : 'chi_(dprod_Iirr (0, j)) = cfDprodr KxH 'chi_j.
Lemma dprod_Iirr_inj : injective dprod_Iirr.
Lemma dprod_Iirr0 : dprod_Iirr (0, 0) = 0.
Lemma dprod_Iirr0l j : dprod_Iirr (0, j) = dprodr_Iirr j.
Lemma dprod_Iirr0r i : dprod_Iirr (i, 0) = dprodl_Iirr i.
Lemma dprod_Iirr_eq0 i j : (dprod_Iirr (i, j) == 0) = (i == 0) && (j == 0).
Lemma cfdot_dprod_irr i1 i2 j1 j2 :
'['chi_(dprod_Iirr (i1, j1)), 'chi_(dprod_Iirr (i2, j2))]
= ((i1 == i2) && (j1 == j2))%:R.
Lemma dprod_Iirr_onto k : k \in codom dprod_Iirr.
Definition inv_dprod_Iirr i := iinv (dprod_Iirr_onto i).
Lemma dprod_IirrK : cancel dprod_Iirr inv_dprod_Iirr.
Lemma inv_dprod_IirrK : cancel inv_dprod_Iirr dprod_Iirr.
Lemma inv_dprod_Iirr0 : inv_dprod_Iirr 0 = (0, 0).
End DProd.
Implicit Arguments dprod_Iirr_inj [gT G K H x1 x2].
Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT})
(KxH : K \x H = G) (HxK : H \x K = G) i j :
dprod_Iirr KxH (i, j) = dprod_Iirr HxK (j, i).
Section BigDprod.
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.
Lemma cfBigdprodi_char i (phi : 'CF(A i)) :
phi \is a character → cfBigdprodi defG phi \is a character.
Lemma cfBigdprodi_charE i (phi : 'CF(A i)) :
P i → (cfBigdprodi defG phi \is a character) = (phi \is a character).
Lemma cfBigdprod_char phi :
(∀ i, P i → phi i \is a character) →
cfBigdprod defG phi \is a character.
Lemma cfBigdprodi_lin_char i (phi : 'CF(A i)) :
phi \is a linear_char → cfBigdprodi defG phi \is a linear_char.
Lemma cfBigdprodi_lin_charE i (phi : 'CF(A i)) :
P i → (cfBigdprodi defG phi \is a linear_char) = (phi \is a linear_char).
Lemma cfBigdprod_lin_char phi :
(∀ i, P i → phi i \is a linear_char) →
cfBigdprod defG phi \is a linear_char.
Lemma cfBigdprodi_irr i chi :
P i → (cfBigdprodi defG chi \in irr G) = (chi \in irr (A i)).
Lemma cfBigdprod_irr chi :
(∀ i, P i → chi i \in irr (A i)) → cfBigdprod defG chi \in irr G.
Lemma cfBigdprod_eq1 phi :
(∀ i, P i → phi i \is a character) →
(cfBigdprod defG phi == 1) = [∀ (i | P i), phi i == 1].
Lemma cfBigdprod_Res_lin chi :
chi \is a linear_char → cfBigdprod defG (fun i ⇒ 'Res[A i] chi) = chi.
Lemma cfBigdprodKlin phi :
(∀ i, P i → phi i \is a linear_char) →
∀ i, P i → 'Res (cfBigdprod defG phi) = phi i.
Lemma cfBigdprodKabelian Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
abelian G → ∀ i, P i → 'Res (cfBigdprod defG phi) = 'chi_(Iphi i).
End BigDprod.
Section Aut.
Variables (gT : finGroupType) (G : {group gT}).
Implicit Type u : {rmorphism algC → algC}.
Lemma conjC_charAut u (chi : 'CF(G)) x :
chi \is a character → (u (chi x))^* = u (chi x)^*.
Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*.
Lemma cfdot_aut_char u (phi chi : 'CF(G)) :
chi \is a character → '[cfAut u phi, cfAut u chi] = u '[phi, chi].
Lemma cfdot_aut_irr u phi i :
'[cfAut u phi, cfAut u 'chi[G]_i] = u '[phi, 'chi_i].
Lemma cfAut_irr u chi : (cfAut u chi \in irr G) = (chi \in irr G).
Lemma cfConjC_irr i : (('chi_i)^*)%CF \in irr G.
Lemma irr_aut_closed u : cfAut_closed u (irr G).
Definition aut_Iirr u i := cfIirr (cfAut u 'chi[G]_i).
Lemma aut_IirrE u i : 'chi_(aut_Iirr u i) = cfAut u 'chi_i.
Definition conjC_Iirr := aut_Iirr conjC.
Lemma conjC_IirrE i : 'chi[G]_(conjC_Iirr i) = ('chi_i)^*%CF.
Lemma conjC_IirrK : involutive conjC_Iirr.
Lemma aut_Iirr0 u : aut_Iirr u 0 = 0 :> Iirr G.
Lemma conjC_Iirr0 : conjC_Iirr 0 = 0 :> Iirr G.
Lemma aut_Iirr_eq0 u i : (aut_Iirr u i == 0) = (i == 0).
Lemma conjC_Iirr_eq0 i : (conjC_Iirr i == 0 :> Iirr G) = (i == 0).
Lemma aut_Iirr_inj u : injective (aut_Iirr u).
End Aut.
Implicit Arguments aut_Iirr_inj [gT G x1 x2].
Section Coset.
Variable (gT : finGroupType).
Implicit Types G H : {group gT}.
Lemma cfQuo_char G H (chi : 'CF(G)) :
chi \is a character → (chi / H)%CF \is a character.
Lemma cfQuo_lin_char G H (chi : 'CF(G)) :
chi \is a linear_char → (chi / H)%CF \is a linear_char.
Lemma cfMod_char G H (chi : 'CF(G / H)) :
chi \is a character → (chi %% H)%CF \is a character.
Lemma cfMod_lin_char G H (chi : 'CF(G / H)) :
chi \is a linear_char → (chi %% H)%CF \is a linear_char.
Lemma cfMod_charE G H (chi : 'CF(G / H)) :
H <| G → (chi %% H \is a character)%CF = (chi \is a character).
Lemma cfMod_lin_charE G H (chi : 'CF(G / H)) :
H <| G → (chi %% H \is a linear_char)%CF = (chi \is a linear_char).
Lemma cfQuo_charE G H (chi : 'CF(G)) :
H <| G → H \subset cfker chi →
(chi / H \is a character)%CF = (chi \is a character).
Lemma cfQuo_lin_charE G H (chi : 'CF(G)) :
H <| G → H \subset cfker chi →
(chi / H \is a linear_char)%CF = (chi \is a linear_char).
Lemma cfMod_irr G H chi :
H <| G → (chi %% H \in irr G)%CF = (chi \in irr (G / H)).
Definition mod_Iirr G H i := cfIirr ('chi[G / H]_i %% H)%CF.
Lemma mod_Iirr0 G H : mod_Iirr (0 : Iirr (G / H)) = 0.
Lemma mod_IirrE G H i : H <| G → 'chi_(mod_Iirr i) = ('chi[G / H]_i %% H)%CF.
Lemma mod_Iirr_eq0 G H i :
H <| G → (mod_Iirr i == 0) = (i == 0 :> Iirr (G / H)).
Lemma cfQuo_irr G H chi :
H <| G → H \subset cfker chi →
((chi / H)%CF \in irr (G / H)) = (chi \in irr G).
Definition quo_Iirr G H i := cfIirr ('chi[G]_i / H)%CF.
Lemma quo_Iirr0 G H : quo_Iirr H (0 : Iirr G) = 0.
Lemma quo_IirrE G H i :
H <| G → H \subset cfker 'chi[G]_i → 'chi_(quo_Iirr H i) = ('chi_i / H)%CF.
Lemma quo_Iirr_eq0 G H i :
H <| G → H \subset cfker 'chi[G]_i → (quo_Iirr H i == 0) = (i == 0).
Lemma mod_IirrK G H : H <| G → cancel (@mod_Iirr G H) (@quo_Iirr G H).
Lemma quo_IirrK G H i :
H <| G → H \subset cfker 'chi[G]_i → mod_Iirr (quo_Iirr H i) = i.
Lemma quo_IirrKeq G H :
H <| G →
∀ i, (mod_Iirr (quo_Iirr H i) == i) = (H \subset cfker 'chi[G]_i).
Lemma mod_Iirr_bij H G :
H <| G → {on [pred i | H \subset cfker 'chi_i], bijective (@mod_Iirr G H)}.
Lemma sum_norm_irr_quo H G x :
x \in G → H <| G →
\sum_i `|'chi[G / H]_i (coset H x)| ^+ 2
= \sum_(i | H \subset cfker 'chi_i) `|'chi[G]_i x| ^+ 2.
Lemma cap_cfker_normal G H :
H <| G → \bigcap_(i | H \subset cfker 'chi[G]_i) (cfker 'chi_i) = H.
Lemma cfker_reg_quo G H : H <| G → cfker (cfReg (G / H)%g %% H) = H.
End Coset.
Section DerivedGroup.
Variable gT : finGroupType.
Implicit Types G H : {group gT}.
Lemma lin_irr_der1 G i :
('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i).
Lemma subGcfker G i : (G \subset cfker 'chi[G]_i) = (i == 0).
Lemma irr_prime_injP G i :
prime #|G| → reflect {in G &, injective 'chi[G]_i} (i != 0).
a \in A → [acts A, on classes G | cto] →
(∀ i x y, x \in G → y \in cto (x ^: G) a →
'chi_i x = 'chi_(ito i a) y) →
#|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.
End OrthogonalityRelations.
Section InnerProduct.
Variable (gT : finGroupType) (G : {group gT}).
Lemma cfdot_irr i j : '['chi_i, 'chi_j]_G = (i == j)%:R.
Lemma cfnorm_irr i : '['chi[G]_i] = 1.
Lemma irr_orthonormal : orthonormal (irr G).
Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i].
Lemma cfun_sum_cfdot phi : phi = \sum_i '[phi, 'chi_i]_G *: 'chi_i.
Lemma cfdot_sum_irr phi psi :
'[phi, psi]_G = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i]^*.
Lemma Cnat_cfdot_char_irr i phi :
phi \is a character → '[phi, 'chi_i]_G \in Cnat.
Lemma cfdot_char_r phi chi :
chi \is a character → '[phi, chi]_G = \sum_i '[phi, 'chi_i] × '[chi, 'chi_i].
Lemma Cnat_cfdot_char chi xi :
chi \is a character → xi \is a character → '[chi, xi]_G \in Cnat.
Lemma cfdotC_char chi xi :
chi \is a character→ xi \is a character → '[chi, xi]_G = '[xi, chi].
Lemma irrEchar chi : (chi \in irr G) = (chi \is a character) && ('[chi] == 1).
Lemma irrWchar chi : chi \in irr G → chi \is a character.
Lemma irrWnorm chi : chi \in irr G → '[chi] = 1.
Lemma mul_lin_irr xi chi :
xi \is a linear_char → chi \in irr G → xi × chi \in irr G.
Lemma eq_scaled_irr a b i j :
(a *: 'chi[G]_i == b *: 'chi_j) = (a == b) && ((a == 0) || (i == j)).
Lemma eq_signed_irr (s t : bool) i j :
((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j).
Lemma eq_scale_irr a (i j : Iirr G) :
(a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j).
Lemma eq_addZ_irr a b (i j r t : Iirr G) :
(a *: 'chi_i + b *: 'chi_j == a *: 'chi_r + b *: 'chi_t)
= [|| [&& (a == 0) || (i == r) & (b == 0) || (j == t)],
[&& i == t, j == r & a == b] | [&& i == j, r == t & a == - b]].
Lemma eq_subZnat_irr (a b : nat) (i j r t : Iirr G) :
(a%:R *: 'chi_i - b%:R *: 'chi_j == a%:R *: 'chi_r - b%:R *: 'chi_t)
= [|| a == 0%N | i == r] && [|| b == 0%N | j == t]
|| [&& i == j, r == t & a == b].
End InnerProduct.
Section IrrConstt.
Variable (gT : finGroupType) (G H : {group gT}).
Lemma char1_ge_norm (chi : 'CF(G)) x :
chi \is a character → `|chi x| ≤ chi 1%g.
Lemma max_cfRepr_norm_scalar n (rG : mx_representation algCF G n) x :
x \in G → `|cfRepr rG x| = cfRepr rG 1%g →
exists2 c, `|c| = 1 & rG x = c%:M.
Lemma max_cfRepr_mx1 n (rG : mx_representation algCF G n) x :
x \in G → cfRepr rG x = cfRepr rG 1%g → rG x = 1%:M.
Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0].
Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0).
Lemma constt_charP (i : Iirr G) chi :
chi \is a character →
reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi')
(i \in irr_constt chi).
Lemma cfun_sum_constt (phi : 'CF(G)) :
phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i.
Lemma neq0_has_constt (phi : 'CF(G)) :
phi != 0 → ∃ i, i \in irr_constt phi.
Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i.
Lemma char1_ge_constt (i : Iirr G) chi :
chi \is a character → i \in irr_constt chi → 'chi_i 1%g ≤ chi 1%g.
Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
phi \is a character → psi \is a character →
i \in irr_constt phi → j \in irr_constt psi →
'[phi, psi] = 0 → '['chi_i, 'chi_j] = 0.
End IrrConstt.
Section Kernel.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}).
Lemma cfker_repr n (rG : mx_representation algCF G n) :
cfker (cfRepr rG) = rker rG.
Lemma cfkerEchar chi :
chi \is a character → cfker chi = [set x in G | chi x == chi 1%g].
Lemma cfker_nzcharE chi :
chi \is a character → chi != 0 → cfker chi = [set x | chi x == chi 1%g].
Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g].
Lemma cfker_irr0 : cfker 'chi[G]_0 = G.
Lemma cfaithful_reg : cfaithful (cfReg G).
Lemma cfkerE chi :
chi \is a character →
cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i.
Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1].
Lemma cfker_constt i chi :
chi \is a character → i \in irr_constt chi →
cfker chi \subset cfker 'chi[G]_i.
Section KerLin.
Variable xi : 'CF(G).
Hypothesis lin_xi : xi \is a linear_char.
Let Nxi: xi \is a character.
Lemma lin_char_der1 : G^`(1)%g \subset cfker xi.
Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g.
Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|.
Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N.
End KerLin.
End Kernel.
Section Restrict.
Variable (gT : finGroupType) (G H : {group gT}).
Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) :
cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG).
Lemma cfRes_char chi : chi \is a character → 'Res[H, G] chi \is a character.
Lemma cfRes_eq0 phi : phi \is a character → ('Res[H, G] phi == 0) = (phi == 0).
Lemma cfRes_lin_char chi :
chi \is a linear_char → 'Res[H, G] chi \is a linear_char.
Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0.
Lemma cfRes_lin_lin (chi : 'CF(G)) :
chi \is a character → 'Res[H] chi \is a linear_char → chi \is a linear_char.
Lemma cfRes_irr_irr chi :
chi \is a character → 'Res[H] chi \in irr H → chi \in irr G.
Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i).
Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0.
Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
End Restrict.
Section MoreConstt.
Variables (gT : finGroupType) (G H : {group gT}).
Lemma constt_Ind_Res i j :
i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)).
Lemma cfdot_Res_ge_constt i j psi :
psi \is a character → j \in irr_constt psi →
'['Res[H, G] 'chi_j, 'chi_i] ≤ '['Res[H] psi, 'chi_i].
Lemma constt_Res_trans j psi :
psi \is a character → j \in irr_constt psi →
{subset irr_constt ('Res[H, G] 'chi_j) ≤ irr_constt ('Res[H] psi)}.
End MoreConstt.
Section Morphim.
Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
Implicit Type chi : 'CF(f @* G).
Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD :
cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG).
Lemma cfMorph_char chi : chi \is a character → cfMorph chi \is a character.
Lemma cfMorph_lin_char chi :
chi \is a linear_char → cfMorph chi \is a linear_char.
Lemma cfMorph_charE chi :
G \subset D → (cfMorph chi \is a character) = (chi \is a character).
Lemma cfMorph_lin_charE chi :
G \subset D → (cfMorph chi \is a linear_char) = (chi \is a linear_char).
Lemma cfMorph_irr chi :
G \subset D → (cfMorph chi \in irr G) = (chi \in irr (f @* G)).
Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i).
Lemma morph_Iirr0 : morph_Iirr 0 = 0.
Hypothesis sGD : G \subset D.
Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i.
Lemma morph_Iirr_inj : injective morph_Iirr.
Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0).
End Morphim.
Section Isom.
Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
Variables (R : {group rT}) (isoGR : isom G R f).
Implicit Type chi : 'CF(G).
Lemma cfIsom_char chi :
(cfIsom isoGR chi \is a character) = (chi \is a character).
Lemma cfIsom_lin_char chi :
(cfIsom isoGR chi \is a linear_char) = (chi \is a linear_char).
Lemma cfIsom_irr chi : (cfIsom isoGR chi \in irr R) = (chi \in irr G).
Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i).
Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i.
Lemma isom_Iirr_inj : injective isom_Iirr.
Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0).
Lemma isom_Iirr0 : isom_Iirr 0 = 0.
End Isom.
Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2].
Section IsomInv.
Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
Variables (R : {group rT}) (isoGR : isom G R f).
Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)).
Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR).
End IsomInv.
Section Sdprod.
Variables (gT : finGroupType) (K H G : {group gT}).
Hypothesis defG : K ><| H = G.
Let nKG: G \subset 'N(K).
Lemma cfSdprod_char chi :
(cfSdprod defG chi \is a character) = (chi \is a character).
Lemma cfSdprod_lin_char chi :
(cfSdprod defG chi \is a linear_char) = (chi \is a linear_char).
Lemma cfSdprod_irr chi : (cfSdprod defG chi \in irr G) = (chi \in irr H).
Definition sdprod_Iirr j := cfIirr (cfSdprod defG 'chi_j).
Lemma sdprod_IirrE j : 'chi_(sdprod_Iirr j) = cfSdprod defG 'chi_j.
Lemma sdprod_IirrK : cancel sdprod_Iirr (Res_Iirr H).
Lemma sdprod_Iirr_inj : injective sdprod_Iirr.
Lemma sdprod_Iirr_eq0 i : (sdprod_Iirr i == 0) = (i == 0).
Lemma sdprod_Iirr0 : sdprod_Iirr 0 = 0.
Lemma Res_sdprod_irr phi :
K \subset cfker phi → phi \in irr G → 'Res phi \in irr H.
Lemma sdprod_Res_IirrE i :
K \subset cfker 'chi[G]_i → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
Lemma sdprod_Res_IirrK i :
K \subset cfker 'chi_i → sdprod_Iirr (Res_Iirr H i) = i.
End Sdprod.
Implicit Arguments sdprod_Iirr_inj [gT K H G x1 x2].
Section DProd.
Variables (gT : finGroupType) (G K H : {group gT}).
Hypothesis KxH : K \x H = G.
Lemma cfDprodKl_abelian j : abelian H → cancel ((cfDprod KxH)^~ 'chi_j) 'Res.
Lemma cfDprodKr_abelian i : abelian K → cancel (cfDprod KxH 'chi_i) 'Res.
Lemma cfDprodl_char phi :
(cfDprodl KxH phi \is a character) = (phi \is a character).
Lemma cfDprodr_char psi :
(cfDprodr KxH psi \is a character) = (psi \is a character).
Lemma cfDprod_char phi psi :
phi \is a character → psi \is a character →
cfDprod KxH phi psi \is a character.
Lemma cfDprod_eq1 phi psi :
phi \is a character → psi \is a character →
(cfDprod KxH phi psi == 1) = (phi == 1) && (psi == 1).
Lemma cfDprodl_lin_char phi :
(cfDprodl KxH phi \is a linear_char) = (phi \is a linear_char).
Lemma cfDprodr_lin_char psi :
(cfDprodr KxH psi \is a linear_char) = (psi \is a linear_char).
Lemma cfDprod_lin_char phi psi :
phi \is a linear_char → psi \is a linear_char →
cfDprod KxH phi psi \is a linear_char.
Lemma cfDprodl_irr chi : (cfDprodl KxH chi \in irr G) = (chi \in irr K).
Lemma cfDprodr_irr chi : (cfDprodr KxH chi \in irr G) = (chi \in irr H).
Definition dprodl_Iirr i := cfIirr (cfDprodl KxH 'chi_i).
Lemma dprodl_IirrE i : 'chi_(dprodl_Iirr i) = cfDprodl KxH 'chi_i.
Lemma dprodl_IirrK : cancel dprodl_Iirr (Res_Iirr K).
Lemma dprodl_Iirr_eq0 i : (dprodl_Iirr i == 0) = (i == 0).
Lemma dprodl_Iirr0 : dprodl_Iirr 0 = 0.
Definition dprodr_Iirr j := cfIirr (cfDprodr KxH 'chi_j).
Lemma dprodr_IirrE j : 'chi_(dprodr_Iirr j) = cfDprodr KxH 'chi_j.
Lemma dprodr_IirrK : cancel dprodr_Iirr (Res_Iirr H).
Lemma dprodr_Iirr_eq0 j : (dprodr_Iirr j == 0) = (j == 0).
Lemma dprodr_Iirr0 : dprodr_Iirr 0 = 0.
Lemma cfDprod_irr i j : cfDprod KxH 'chi_i 'chi_j \in irr G.
Definition dprod_Iirr ij := cfIirr (cfDprod KxH 'chi_ij.1 'chi_ij.2).
Lemma dprod_IirrE i j : 'chi_(dprod_Iirr (i, j)) = cfDprod KxH 'chi_i 'chi_j.
Lemma dprod_IirrEl i : 'chi_(dprod_Iirr (i, 0)) = cfDprodl KxH 'chi_i.
Lemma dprod_IirrEr j : 'chi_(dprod_Iirr (0, j)) = cfDprodr KxH 'chi_j.
Lemma dprod_Iirr_inj : injective dprod_Iirr.
Lemma dprod_Iirr0 : dprod_Iirr (0, 0) = 0.
Lemma dprod_Iirr0l j : dprod_Iirr (0, j) = dprodr_Iirr j.
Lemma dprod_Iirr0r i : dprod_Iirr (i, 0) = dprodl_Iirr i.
Lemma dprod_Iirr_eq0 i j : (dprod_Iirr (i, j) == 0) = (i == 0) && (j == 0).
Lemma cfdot_dprod_irr i1 i2 j1 j2 :
'['chi_(dprod_Iirr (i1, j1)), 'chi_(dprod_Iirr (i2, j2))]
= ((i1 == i2) && (j1 == j2))%:R.
Lemma dprod_Iirr_onto k : k \in codom dprod_Iirr.
Definition inv_dprod_Iirr i := iinv (dprod_Iirr_onto i).
Lemma dprod_IirrK : cancel dprod_Iirr inv_dprod_Iirr.
Lemma inv_dprod_IirrK : cancel inv_dprod_Iirr dprod_Iirr.
Lemma inv_dprod_Iirr0 : inv_dprod_Iirr 0 = (0, 0).
End DProd.
Implicit Arguments dprod_Iirr_inj [gT G K H x1 x2].
Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT})
(KxH : K \x H = G) (HxK : H \x K = G) i j :
dprod_Iirr KxH (i, j) = dprod_Iirr HxK (j, i).
Section BigDprod.
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.
Lemma cfBigdprodi_char i (phi : 'CF(A i)) :
phi \is a character → cfBigdprodi defG phi \is a character.
Lemma cfBigdprodi_charE i (phi : 'CF(A i)) :
P i → (cfBigdprodi defG phi \is a character) = (phi \is a character).
Lemma cfBigdprod_char phi :
(∀ i, P i → phi i \is a character) →
cfBigdprod defG phi \is a character.
Lemma cfBigdprodi_lin_char i (phi : 'CF(A i)) :
phi \is a linear_char → cfBigdprodi defG phi \is a linear_char.
Lemma cfBigdprodi_lin_charE i (phi : 'CF(A i)) :
P i → (cfBigdprodi defG phi \is a linear_char) = (phi \is a linear_char).
Lemma cfBigdprod_lin_char phi :
(∀ i, P i → phi i \is a linear_char) →
cfBigdprod defG phi \is a linear_char.
Lemma cfBigdprodi_irr i chi :
P i → (cfBigdprodi defG chi \in irr G) = (chi \in irr (A i)).
Lemma cfBigdprod_irr chi :
(∀ i, P i → chi i \in irr (A i)) → cfBigdprod defG chi \in irr G.
Lemma cfBigdprod_eq1 phi :
(∀ i, P i → phi i \is a character) →
(cfBigdprod defG phi == 1) = [∀ (i | P i), phi i == 1].
Lemma cfBigdprod_Res_lin chi :
chi \is a linear_char → cfBigdprod defG (fun i ⇒ 'Res[A i] chi) = chi.
Lemma cfBigdprodKlin phi :
(∀ i, P i → phi i \is a linear_char) →
∀ i, P i → 'Res (cfBigdprod defG phi) = phi i.
Lemma cfBigdprodKabelian Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
abelian G → ∀ i, P i → 'Res (cfBigdprod defG phi) = 'chi_(Iphi i).
End BigDprod.
Section Aut.
Variables (gT : finGroupType) (G : {group gT}).
Implicit Type u : {rmorphism algC → algC}.
Lemma conjC_charAut u (chi : 'CF(G)) x :
chi \is a character → (u (chi x))^* = u (chi x)^*.
Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*.
Lemma cfdot_aut_char u (phi chi : 'CF(G)) :
chi \is a character → '[cfAut u phi, cfAut u chi] = u '[phi, chi].
Lemma cfdot_aut_irr u phi i :
'[cfAut u phi, cfAut u 'chi[G]_i] = u '[phi, 'chi_i].
Lemma cfAut_irr u chi : (cfAut u chi \in irr G) = (chi \in irr G).
Lemma cfConjC_irr i : (('chi_i)^*)%CF \in irr G.
Lemma irr_aut_closed u : cfAut_closed u (irr G).
Definition aut_Iirr u i := cfIirr (cfAut u 'chi[G]_i).
Lemma aut_IirrE u i : 'chi_(aut_Iirr u i) = cfAut u 'chi_i.
Definition conjC_Iirr := aut_Iirr conjC.
Lemma conjC_IirrE i : 'chi[G]_(conjC_Iirr i) = ('chi_i)^*%CF.
Lemma conjC_IirrK : involutive conjC_Iirr.
Lemma aut_Iirr0 u : aut_Iirr u 0 = 0 :> Iirr G.
Lemma conjC_Iirr0 : conjC_Iirr 0 = 0 :> Iirr G.
Lemma aut_Iirr_eq0 u i : (aut_Iirr u i == 0) = (i == 0).
Lemma conjC_Iirr_eq0 i : (conjC_Iirr i == 0 :> Iirr G) = (i == 0).
Lemma aut_Iirr_inj u : injective (aut_Iirr u).
End Aut.
Implicit Arguments aut_Iirr_inj [gT G x1 x2].
Section Coset.
Variable (gT : finGroupType).
Implicit Types G H : {group gT}.
Lemma cfQuo_char G H (chi : 'CF(G)) :
chi \is a character → (chi / H)%CF \is a character.
Lemma cfQuo_lin_char G H (chi : 'CF(G)) :
chi \is a linear_char → (chi / H)%CF \is a linear_char.
Lemma cfMod_char G H (chi : 'CF(G / H)) :
chi \is a character → (chi %% H)%CF \is a character.
Lemma cfMod_lin_char G H (chi : 'CF(G / H)) :
chi \is a linear_char → (chi %% H)%CF \is a linear_char.
Lemma cfMod_charE G H (chi : 'CF(G / H)) :
H <| G → (chi %% H \is a character)%CF = (chi \is a character).
Lemma cfMod_lin_charE G H (chi : 'CF(G / H)) :
H <| G → (chi %% H \is a linear_char)%CF = (chi \is a linear_char).
Lemma cfQuo_charE G H (chi : 'CF(G)) :
H <| G → H \subset cfker chi →
(chi / H \is a character)%CF = (chi \is a character).
Lemma cfQuo_lin_charE G H (chi : 'CF(G)) :
H <| G → H \subset cfker chi →
(chi / H \is a linear_char)%CF = (chi \is a linear_char).
Lemma cfMod_irr G H chi :
H <| G → (chi %% H \in irr G)%CF = (chi \in irr (G / H)).
Definition mod_Iirr G H i := cfIirr ('chi[G / H]_i %% H)%CF.
Lemma mod_Iirr0 G H : mod_Iirr (0 : Iirr (G / H)) = 0.
Lemma mod_IirrE G H i : H <| G → 'chi_(mod_Iirr i) = ('chi[G / H]_i %% H)%CF.
Lemma mod_Iirr_eq0 G H i :
H <| G → (mod_Iirr i == 0) = (i == 0 :> Iirr (G / H)).
Lemma cfQuo_irr G H chi :
H <| G → H \subset cfker chi →
((chi / H)%CF \in irr (G / H)) = (chi \in irr G).
Definition quo_Iirr G H i := cfIirr ('chi[G]_i / H)%CF.
Lemma quo_Iirr0 G H : quo_Iirr H (0 : Iirr G) = 0.
Lemma quo_IirrE G H i :
H <| G → H \subset cfker 'chi[G]_i → 'chi_(quo_Iirr H i) = ('chi_i / H)%CF.
Lemma quo_Iirr_eq0 G H i :
H <| G → H \subset cfker 'chi[G]_i → (quo_Iirr H i == 0) = (i == 0).
Lemma mod_IirrK G H : H <| G → cancel (@mod_Iirr G H) (@quo_Iirr G H).
Lemma quo_IirrK G H i :
H <| G → H \subset cfker 'chi[G]_i → mod_Iirr (quo_Iirr H i) = i.
Lemma quo_IirrKeq G H :
H <| G →
∀ i, (mod_Iirr (quo_Iirr H i) == i) = (H \subset cfker 'chi[G]_i).
Lemma mod_Iirr_bij H G :
H <| G → {on [pred i | H \subset cfker 'chi_i], bijective (@mod_Iirr G H)}.
Lemma sum_norm_irr_quo H G x :
x \in G → H <| G →
\sum_i `|'chi[G / H]_i (coset H x)| ^+ 2
= \sum_(i | H \subset cfker 'chi_i) `|'chi[G]_i x| ^+ 2.
Lemma cap_cfker_normal G H :
H <| G → \bigcap_(i | H \subset cfker 'chi[G]_i) (cfker 'chi_i) = H.
Lemma cfker_reg_quo G H : H <| G → cfker (cfReg (G / H)%g %% H) = H.
End Coset.
Section DerivedGroup.
Variable gT : finGroupType.
Implicit Types G H : {group gT}.
Lemma lin_irr_der1 G i :
('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i).
Lemma subGcfker G i : (G \subset cfker 'chi[G]_i) = (i == 0).
Lemma irr_prime_injP G i :
prime #|G| → reflect {in G &, injective 'chi[G]_i} (i != 0).
This is Isaacs (2.23)(a).
This is Isaacs (2.23)(b)
Alternative: use the equivalent result in modular representation theory
transitivity #|@socle_of_Iirr _ G @^-1: linear_irr _|; last first.
rewrite (on_card_preimset (socle_of_Iirr_bij _)).
by rewrite card_linear_irr ?algC'G; last apply: groupC.
by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
A non-trivial solvable group has a nonprincipal linear character.
Lemma solvable_has_lin_char G :
G :!=: 1%g → solvable G →
exists2 i, 'chi[G]_i \is a linear_char & 'chi_i != 1.
G :!=: 1%g → solvable G →
exists2 i, 'chi[G]_i \is a linear_char & 'chi_i != 1.
A combinatorial group isommorphic to the linear characters.
Lemma lin_char_group G :
{linG : finGroupType & {cF : linG → 'CF(G) |
[/\ injective cF, #|linG| = #|G : G^`(1)|,
∀ u, cF u \is a linear_char
& ∀ phi, phi \is a linear_char → ∃ u, phi = cF u]
& [/\ cF 1%g = 1%R,
{morph cF : u v / (u × v)%g >-> (u × v)%R},
∀ k, {morph cF : u / (u^+ k)%g >-> u ^+ k},
{morph cF: u / u^-1%g >-> u^-1%CF}
& {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.
Lemma cfExp_prime_transitive G (i j : Iirr G) :
prime #|G| → i != 0 → j != 0 →
exists2 k, coprime k #['chi_i]%CF & 'chi_j = 'chi_i ^+ k.
{linG : finGroupType & {cF : linG → 'CF(G) |
[/\ injective cF, #|linG| = #|G : G^`(1)|,
∀ u, cF u \is a linear_char
& ∀ phi, phi \is a linear_char → ∃ u, phi = cF u]
& [/\ cF 1%g = 1%R,
{morph cF : u v / (u × v)%g >-> (u × v)%R},
∀ k, {morph cF : u / (u^+ k)%g >-> u ^+ k},
{morph cF: u / u^-1%g >-> u^-1%CF}
& {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.
Lemma cfExp_prime_transitive G (i j : Iirr G) :
prime #|G| → i != 0 → j != 0 →
exists2 k, coprime k #['chi_i]%CF & 'chi_j = 'chi_i ^+ k.
This is Isaacs (2.24).
Lemma card_subcent1_coset G H x :
x \in G → H <| G → (#|'C_(G / H)[coset H x]| ≤ #|'C_G[x]|)%N.
End DerivedGroup.
Implicit Arguments irr_prime_injP [gT G i].
x \in G → H <| G → (#|'C_(G / H)[coset H x]| ≤ #|'C_G[x]|)%N.
End DerivedGroup.
Implicit Arguments irr_prime_injP [gT G i].
Determinant characters and determinential order.
Section DetOrder.
Variables (gT : finGroupType) (G : {group gT}).
Section DetRepr.
Variables (n : nat) (rG : mx_representation [fieldType of algC] G n).
Definition det_repr_mx x : 'M_1 := (\det (rG x))%:M.
Fact det_is_repr : mx_repr G det_repr_mx.
Canonical det_repr := MxRepresentation det_is_repr.
Definition detRepr := cfRepr det_repr.
Lemma detRepr_lin_char : detRepr \is a linear_char.
End DetRepr.
Definition cfDet phi := \prod_i detRepr 'Chi_i ^+ truncC '[phi, 'chi[G]_i].
Lemma cfDet_lin_char phi : cfDet phi \is a linear_char.
Lemma cfDetD :
{in character &, {morph cfDet : phi psi / phi + psi >-> phi × psi}}.
Lemma cfDet0 : cfDet 0 = 1.
Lemma cfDetMn k :
{in character, {morph cfDet : phi / phi *+ k >-> phi ^+ k}}.
Lemma cfDetRepr n rG : cfDet (cfRepr rG) = @detRepr n rG.
Lemma cfDet_id xi : xi \is a linear_char → cfDet xi = xi.
Definition cfDet_order phi := #[cfDet phi]%CF.
Definition cfDet_order_lin xi :
xi \is a linear_char → cfDet_order xi = #[xi]%CF.
Definition cfDet_order_dvdG phi : cfDet_order phi %| #|G|.
End DetOrder.
Notation "''o' ( phi )" := (cfDet_order phi)
(at level 8, format "''o' ( phi )") : cfun_scope.
Section CfDetOps.
Implicit Types gT aT rT : finGroupType.
Lemma cfDetRes gT (G H : {group gT}) phi :
phi \is a character → cfDet ('Res[H, G] phi) = 'Res (cfDet phi).
Lemma cfDetMorph aT rT (D G : {group aT}) (f : {morphism D >-> rT})
(phi : 'CF(f @* G)) :
phi \is a character → cfDet (cfMorph phi) = cfMorph (cfDet phi).
Lemma cfDetIsom aT rT (G : {group aT}) (R : {group rT})
(f : {morphism G >-> rT}) (isoGR : isom G R f) phi :
cfDet (cfIsom isoGR phi) = cfIsom isoGR (cfDet phi).
Lemma cfDet_mul_lin gT (G : {group gT}) (lambda phi : 'CF(G)) :
lambda \is a linear_char → phi \is a character →
cfDet (lambda × phi) = lambda ^+ truncC (phi 1%g) × cfDet phi.
End CfDetOps.
Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) :=
if phi \is a character then [set g in G | `|phi g| == phi 1%g] else cfker phi.
Notation "''Z' ( phi )" := (cfcenter phi) : cfun_scope.
Section Center.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (phi chi : 'CF(G)) (H : {group gT}).
Variables (gT : finGroupType) (G : {group gT}).
Section DetRepr.
Variables (n : nat) (rG : mx_representation [fieldType of algC] G n).
Definition det_repr_mx x : 'M_1 := (\det (rG x))%:M.
Fact det_is_repr : mx_repr G det_repr_mx.
Canonical det_repr := MxRepresentation det_is_repr.
Definition detRepr := cfRepr det_repr.
Lemma detRepr_lin_char : detRepr \is a linear_char.
End DetRepr.
Definition cfDet phi := \prod_i detRepr 'Chi_i ^+ truncC '[phi, 'chi[G]_i].
Lemma cfDet_lin_char phi : cfDet phi \is a linear_char.
Lemma cfDetD :
{in character &, {morph cfDet : phi psi / phi + psi >-> phi × psi}}.
Lemma cfDet0 : cfDet 0 = 1.
Lemma cfDetMn k :
{in character, {morph cfDet : phi / phi *+ k >-> phi ^+ k}}.
Lemma cfDetRepr n rG : cfDet (cfRepr rG) = @detRepr n rG.
Lemma cfDet_id xi : xi \is a linear_char → cfDet xi = xi.
Definition cfDet_order phi := #[cfDet phi]%CF.
Definition cfDet_order_lin xi :
xi \is a linear_char → cfDet_order xi = #[xi]%CF.
Definition cfDet_order_dvdG phi : cfDet_order phi %| #|G|.
End DetOrder.
Notation "''o' ( phi )" := (cfDet_order phi)
(at level 8, format "''o' ( phi )") : cfun_scope.
Section CfDetOps.
Implicit Types gT aT rT : finGroupType.
Lemma cfDetRes gT (G H : {group gT}) phi :
phi \is a character → cfDet ('Res[H, G] phi) = 'Res (cfDet phi).
Lemma cfDetMorph aT rT (D G : {group aT}) (f : {morphism D >-> rT})
(phi : 'CF(f @* G)) :
phi \is a character → cfDet (cfMorph phi) = cfMorph (cfDet phi).
Lemma cfDetIsom aT rT (G : {group aT}) (R : {group rT})
(f : {morphism G >-> rT}) (isoGR : isom G R f) phi :
cfDet (cfIsom isoGR phi) = cfIsom isoGR (cfDet phi).
Lemma cfDet_mul_lin gT (G : {group gT}) (lambda phi : 'CF(G)) :
lambda \is a linear_char → phi \is a character →
cfDet (lambda × phi) = lambda ^+ truncC (phi 1%g) × cfDet phi.
End CfDetOps.
Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) :=
if phi \is a character then [set g in G | `|phi g| == phi 1%g] else cfker phi.
Notation "''Z' ( phi )" := (cfcenter phi) : cfun_scope.
Section Center.
Variable (gT : finGroupType) (G : {group gT}).
Implicit Types (phi chi : 'CF(G)) (H : {group gT}).
This is Isaacs (2.27)(a).
This is part of Isaacs (2.27)(b).
Fact cfcenter_group_set phi : group_set ('Z(phi))%CF.
Canonical cfcenter_group f := Group (cfcenter_group_set f).
Lemma char_cfcenterE chi x :
chi \is a character → x \in G →
(x \in ('Z(chi))%CF) = (`|chi x| == chi 1%g).
Lemma irr_cfcenterE i x :
x \in G → (x \in 'Z('chi[G]_i)%CF) = (`|'chi_i x| == 'chi_i 1%g).
Canonical cfcenter_group f := Group (cfcenter_group_set f).
Lemma char_cfcenterE chi x :
chi \is a character → x \in G →
(x \in ('Z(chi))%CF) = (`|chi x| == chi 1%g).
Lemma irr_cfcenterE i x :
x \in G → (x \in 'Z('chi[G]_i)%CF) = (`|'chi_i x| == 'chi_i 1%g).
This is also Isaacs (2.27)(b).
Lemma cfcenter_sub phi : ('Z(phi))%CF \subset G.
Lemma cfker_center_normal phi : cfker phi <| 'Z(phi)%CF.
Lemma cfcenter_normal phi : 'Z(phi)%CF <| G.
Lemma cfker_center_normal phi : cfker phi <| 'Z(phi)%CF.
Lemma cfcenter_normal phi : 'Z(phi)%CF <| G.
This is Isaacs (2.27)(c).
Lemma cfcenter_Res chi :
exists2 chi1, chi1 \is a linear_char & 'Res['Z(chi)%CF] chi = chi 1%g *: chi1.
exists2 chi1, chi1 \is a linear_char & 'Res['Z(chi)%CF] chi = chi 1%g *: chi1.
This is Isaacs (2.27)(d).
This is Isaacs (2.27)(e).
This is Isaacs (2.27)(f).
This is Isaacs (2.28).
This is Isaacs (2.29).
Lemma cfnorm_Res_lerif H phi :
H \subset G →
'['Res[H] phi] ≤ #|G : H|%:R × '[phi] ?= iff (phi \in 'CF(G, H)).
H \subset G →
'['Res[H] phi] ≤ #|G : H|%:R × '[phi] ?= iff (phi \in 'CF(G, H)).
This is Isaacs (2.30).
Lemma irr1_bound (i : Iirr G) :
('chi_i 1%g) ^+ 2 ≤ #|G : 'Z('chi_i)%CF|%:R
?= iff ('chi_i \in 'CF(G, 'Z('chi_i)%CF)).
('chi_i 1%g) ^+ 2 ≤ #|G : 'Z('chi_i)%CF|%:R
?= iff ('chi_i \in 'CF(G, 'Z('chi_i)%CF)).
This is Isaacs (2.31).
Lemma irr1_abelian_bound (i : Iirr G) :
abelian (G / 'Z('chi_i)%CF) → ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.
abelian (G / 'Z('chi_i)%CF) → ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.
This is Isaacs (2.32)(a).
Lemma irr_faithful_center i : cfaithful 'chi[G]_i → cyclic 'Z(G).
Lemma cfcenter_fful_irr i : cfaithful 'chi[G]_i → 'Z('chi_i)%CF = 'Z(G).
Lemma cfcenter_fful_irr i : cfaithful 'chi[G]_i → 'Z('chi_i)%CF = 'Z(G).
This is Isaacs (2.32)(b).
Lemma pgroup_cyclic_faithful (p : nat) :
p.-group G → cyclic 'Z(G) → ∃ i, cfaithful 'chi[G]_i.
End Center.
Section Induced.
Variables (gT : finGroupType) (G H : {group gT}).
Implicit Types (phi : 'CF(G)) (chi : 'CF(H)).
Lemma cfInd_char chi : chi \is a character → 'Ind[G] chi \is a character.
Lemma cfInd_eq0 chi :
H \subset G → chi \is a character → ('Ind[G] chi == 0) = (chi == 0).
Lemma Ind_irr_neq0 i : H \subset G → 'Ind[G, H] 'chi_i != 0.
Definition Ind_Iirr (A B : {set gT}) i := cfIirr ('Ind[B, A] 'chi_i).
Lemma constt_cfRes_irr i : {j | j \in irr_constt ('Res[H, G] 'chi_i)}.
Lemma constt_cfInd_irr i :
H \subset G → {j | j \in irr_constt ('Ind[G, H] 'chi_i)}.
Lemma cfker_Res phi :
H \subset G → phi \is a character → cfker ('Res[H] phi) = H :&: cfker phi.
p.-group G → cyclic 'Z(G) → ∃ i, cfaithful 'chi[G]_i.
End Center.
Section Induced.
Variables (gT : finGroupType) (G H : {group gT}).
Implicit Types (phi : 'CF(G)) (chi : 'CF(H)).
Lemma cfInd_char chi : chi \is a character → 'Ind[G] chi \is a character.
Lemma cfInd_eq0 chi :
H \subset G → chi \is a character → ('Ind[G] chi == 0) = (chi == 0).
Lemma Ind_irr_neq0 i : H \subset G → 'Ind[G, H] 'chi_i != 0.
Definition Ind_Iirr (A B : {set gT}) i := cfIirr ('Ind[B, A] 'chi_i).
Lemma constt_cfRes_irr i : {j | j \in irr_constt ('Res[H, G] 'chi_i)}.
Lemma constt_cfInd_irr i :
H \subset G → {j | j \in irr_constt ('Ind[G, H] 'chi_i)}.
Lemma cfker_Res phi :
H \subset G → phi \is a character → cfker ('Res[H] phi) = H :&: cfker phi.
This is Isaacs Lemma (5.11).