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.

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.

Section StandardRepresentation.

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

Record representation :=
  Representation {rdegree; mx_repr_of_repr :> reprG rdegree}.

Lemma mx_repr0 : mx_repr G (fun _ : gT ⇒ 1%:M : 'M[R]_0).

Definition grepr0 := Representation (MxRepresentation mx_repr0).

Lemma add_mx_repr (rG1 rG2 : representation) :
  mx_repr G (fun g ⇒ block_mx (rG1 g) 0 0 (rG2 g)).

Definition dadd_grepr rG1 rG2 :=
  Representation (MxRepresentation (add_mx_repr rG1 rG2)).

Section DsumRepr.

Variables (n : nat) (rG : reprG n).

Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation)
    (modU : mxmodule rG U) (modV : mxmodule rG V) (modW : mxmodule rG W) :
    (U + V :=: W)%MS → mxdirect (U + V) →
    mx_rsim (submod_repr modU) rU → mx_rsim (submod_repr modV) rV →
  mx_rsim (submod_repr modW) (dadd_grepr rU rV).

Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
    (modU : ∀ i, mxmodule rG (U i)) (modW : mxmodule rG W) :
    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
    (∀ i, mx_rsim (submod_repr (modU i)) (rU i : representation)) →
  mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).

Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW.

Lemma mx_rsim_socle (sG : socleType rG) (W : sG) (rW : representation) :
    let modW : mxmodule rG W := component_mx_module rG (socle_base W) in
    mx_rsim (socle_repr W) rW →
  mx_rsim (submod_repr modW) (muln_grepr rW (socle_mult W)).

End DsumRepr.

Section ProdRepr.

Variables (n1 n2 : nat) (rG1 : reprG n1) (rG2 : reprG n2).

Lemma prod_mx_repr : mx_repr G (fun g ⇒ tprod (rG1 g) (rG2 g)).

Definition prod_repr := MxRepresentation prod_mx_repr.

End ProdRepr.

Lemma prod_repr_lin n2 (rG1 : reprG 1) (rG2 : reprG n2) :
  {in G, ∀ x, let cast_n2 := esym (mul1n n2) in
      prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.

End StandardRepresentation.

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 W ⇒ socle_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).

Lemma cfReprReg : cfRepr (regular_repr algC 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).

Lemma xcfunZr a phi A : xcfun phi (a *: A) = a × xcfun phi A.

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

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

Lemma cfReg_sum : cfReg G = \sum_i 'chi_i 1%g *: 'chi_i.

Let aG := regular_repr algC G.
Let R_G := group_ring algC 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) = (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.

Theorem cfun_irr_sum phi : {a | phi = \sum_i a i *: 'chi[G]_i}.

Lemma cfRepr_standard n (rG : mx_representation algC 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).

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.

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

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

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

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.

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

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.

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

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