Library mathcomp.character.character

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

From HB Require Import structures.
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 archimedean.

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.

Section AlgC.

Variable (gT : finGroupType).

Lemma groupC : group_closure_field algC 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).


Lemma trow_is_linear n1 m2 n2 (A : 'rV_n1) : linear (@trow n1 A m2 n2).


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.

Arguments grepr0 {R gT G}.

Section Char.

Variables (gT : finGroupType) (G : {group gT}).

Fact cfRepr_subproof n (rG : mx_representation algC 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 algC G n).
Let sG := DecSocleType rG.
Let iG : irrType algC 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 (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).
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).

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

Lemma NirrE : Nirr G = #|classes G|.

Fact Iirr_cast : Nirr G = #|sG|.

Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr).

Definition socle_of_Iirr (i : Iirr G) : sG :=
  enum_val (cast_ord Iirr_cast (i + offset)).
Definition irr_of_socle (Wi : sG) : Iirr G :=
  cast_ord (esym Iirr_cast) (enum_rank Wi) - offset.

Lemma socle_Iirr0 : W 0 = [1 sG]%irr.

Lemma socle_of_IirrK : cancel W irr_of_socle.

Lemma irr_of_socleK : cancel irr_of_socle W.
Hint Resolve socle_of_IirrK irr_of_socleK : core.

Lemma irr_of_socle_bij (A : {pred (Iirr G)}) : {on A, bijective irr_of_socle}.

Lemma socle_of_Iirr_bij (A : {pred sG}) : {on A, bijective W}.

End IrrClassDef.

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

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 algC 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 Num.nat.

Lemma irr1_gt0 i : 0 < 'chi_i 1%g.

Lemma irr1_neq0 i : 'chi_i 1%g != 0.

Lemma irr_neq0 i : 'chi_i != 0.


Definition cfIirr : B, 'CF(B) Iirr B :=
  locked_with cfIirr_key (fun B chiinord (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).
This is Isaacs, Theorem (2.8).
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_pred {G : {set gT}} :=
  fun phi : 'CF(G)[ i, coord (irr G) i phi \in Num.nat].
Arguments character_pred _ _ /.
Definition character {G : {set gT}} := [qualify a phi | @character_pred G phi].

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

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

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

End IsChar.
Arguments character_pred _ _ _ /.
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 algC 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_pred {B : {set gT}} :=
  fun phi : 'CF(B)(phi \is a character) && (phi 1%g == 1).
Arguments linear_char_pred _ _ /.
Definition linear_char {B : {set gT}} :=
  [qualify a phi | @linear_char_pred B phi].

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_divr : divr_closed (@linear_char G).

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.

Arguments linear_char_pred _ _ _ /.

Section OrthogonalityRelations.

Variables aT gT : finGroupType.

This is Isaacs, Lemma (2.15)
Lemma repr_rsim_diag (G : {group gT}) f (rG : mx_representation algC 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).
This is Isaacs, Theorem (2.13).
This is Isaacs, Corollary (2.14).
The character table.
The explicit value of the inverse is needed for the proof of the second orthogonality relation.
This is Isaacs, Theorem (2.18).
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 Num.nat.

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

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 | i == r] && [|| b == 0 | 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 algC 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 algC 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 algC 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 algC 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 algC (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).
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.

Arguments irr_prime_injP {gT G i}.

Determinant characters and determinential order.
Section DetRepr.

Variables (gT : finGroupType) (G : {group gT}).
Variables (n : nat) (rG : mx_representation 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.

Canonical cfDet_unlockable := Unlockable cfDet.unlock.

Section DetOrder.

Variables (gT : finGroupType) (G : {group gT}).


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 :