+ +

Library mathcomp.character.character

+ +

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

+ +

+ This file contains the basic 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.
+ +
+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). +

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