Library mathcomp.character.character

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice ssrnat seq.
From mathcomp Require Import path div fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset gproduct fingroup morphism.
From mathcomp Require Import perm automorphism quotient finalg action zmodp.
From mathcomp Require Import commutator cyclic center pgroup nilpotent sylow.
From mathcomp Require Import abelian matrix mxalgebra mxpoly mxrepresentation.
From mathcomp Require Import vector ssrnum algC classfun.

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 Order.TTheory GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Local Notation algCF := [fieldType of algC].

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}).
Local Notation reprG := (mx_representation R G).

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.

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].
Local Notation soc := standard_socle.

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 A phi := xcfun phi A.
Arguments xcfun_r A phi /.

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.
Arguments xcfun_r {_ _} A phi /.
Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.

Definition pred_Nirr gT B := #|@classes gT B|.-1.
Arguments pred_Nirr {gT} B%g.
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.
Local Notation W := socle_of_Iirr.

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.

Arguments socle_of_Iirr {gT G%G} i%R.

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.

Arguments irr {gT} B%g.

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.
Local Notation W i := (@socle_of_Iirr _ G i).
Local Notation "''n_' i" := 'n_(W i).
Local Notation "''R_' i" := 'R_(W i).
Local Notation "''e_' i" := 'e_(W i).

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.

Local Remark cfIirr_key : unit.
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.

Arguments cfReg {gT} B%g.
Arguments irrP {gT G xi}.
Arguments irr_reprP {gT G xi}.
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).

Local Notation reprG := (mx_representation algCF G).

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

Local Notation c := irr_class.
Local Notation g i := (repr (c i)).
Local Notation iC := class_Iirr.

Definition character_table := \matrix_(i, j) 'chi[G]_i (g j).
Local Notation X := character_table.

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

Arguments class_IirrK {gT G%G} [xG%g] GxG : rename.
Arguments character_table {gT} G%g.

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.

Arguments irr_constt {gT B%g} phi%CF.

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.

Arguments Res_Iirr {gT A%g} B%g i%R.

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.

Arguments isom_Iirr_inj {aT rT G f R} isoGR [i1 i2] : rename.

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.

Arguments sdprod_Iirr_inj {gT K H G} defG [i1 i2] : rename.

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.

Arguments dprod_Iirr_inj {gT G K H} KxH [i1 i2] : rename.

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.

Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename.
Arguments conjC_IirrK {gT G} i : rename.

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

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

Arguments Ind_Iirr {gT A%g} B%g i%R.