- -

Library mathcomp.character.character

- -

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

- -

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

- -

- 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 : core.
- -
-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, 'CF (B ) → Iirr B :=
-  locked_with cfIirr_key (fun B chi ⇒ 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). -

-Corollary irr_sum_square : \sum_i ('chi [G ]_i 1%g) ^+ 2 = #|G |%:R.
- -
-

- -

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

- -

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

- -

- 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.
- -
- -
-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.
- -
-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 }).
- -
-

- -

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

- -

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

- -

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

- -

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

- -

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

- -

- This is Isaacs, Theorem (6.32) (due to Brauer). -

- -

- This is Isaacs (2.23)(a). -

-Lemma cap_cfker_lin_irr G :
- \bigcap_(i | 'chi [G ]_i \is a linear_char ) (cfker 'chi_i ) = G ^`(1)%g.
- -
-

- -

- This is Isaacs (2.23)(b) -

-Lemma card_lin_irr G :
- #|[pred i | 'chi [G ]_i \is a linear_char ]| = #|G : G ^`(1)%g|.
-

- -

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

- -

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

- -

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

- -

- 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 }).
- -
-

- -

- This is Isaacs (2.27)(a). -

-Lemma cfcenter_repr n (rG : mx_representation algCF G n) :
- 'Z (cfRepr rG )%CF = rcenter rG.
- -
-

- -

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

- -

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

- -

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

- -

- This is Isaacs (2.27)(d). -

-Lemma cfcenter_cyclic chi : cyclic ('Z (chi )%CF / cfker chi)%g.
- -
-

- -

- This is Isaacs (2.27)(e). -

-Lemma cfcenter_subset_center chi :
- ('Z (chi )%CF / cfker chi)%g \subset 'Z (G / cfker chi )%g.
- -
-

- -

- This is Isaacs (2.27)(f). -

-Lemma cfcenter_eq_center (i : Iirr G) :
- ('Z ('chi_i )%CF / cfker 'chi_i)%g = 'Z (G / cfker 'chi_i )%g.
- -
-

- -

- This is Isaacs (2.28). -

-Lemma cap_cfcenter_irr : \bigcap_i 'Z ('chi [G ]_i )%CF = 'Z (G ).
- -
-

- -

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

- -

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

- -

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

- -

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

- -

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

- -

- This is Isaacs Lemma (5.11). -

-Lemma cfker_Ind chi :
-    H \subset G → chi \is a character → chi != 0 →
-  cfker ('Ind [G , H ] chi) = gcore (cfker chi) G.
- -
-Lemma cfker_Ind_irr i :
-  H \subset G → cfker ('Ind [G , H ] 'chi_i) = gcore (cfker 'chi_i) G.
- -
-End Induced.
- -
-