Library mathcomp.character.character

(* (c) Copyright 2006-2015 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 gblock_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 gtprod (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 Wsocle_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).
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.

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

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

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

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

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

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).
This is Isaacs (2.27)(f).
This is Isaacs (2.28).
This is Isaacs (2.29).
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).
This is Isaacs (2.32)(a).
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 :&: c