Library mathcomp.character.inertia

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

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Reserved Notation "''I[' phi ]"
  (at level 8, format "''I[' phi ]").
Reserved Notation "''I_' G [ phi ]"
  (at level 8, G at level 2, format "''I_' G [ phi ]").

Section ConjDef.

Variables (gT : finGroupType) (B : {set gT}) (y : gT) (phi : 'CF(B)).

Fact cfConjg_subproof :
  is_class_fun G [ffun x ⇒ phi (if y \in 'N(G) then x ^ y^-1 else x)].
Definition cfConjg := Cfun 1 cfConjg_subproof.

End ConjDef.

Notation "f ^ y" := (cfConjg y f) : cfun_scope.

Section Conj.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Type phi : 'CF(G).

Lemma cfConjgE phi y x : y \in 'N(G) → (phi ^ y)%CF x = phi (x ^ y^-1)%g.

Lemma cfConjgEJ phi y x : y \in 'N(G) → (phi ^ y)%CF (x ^ y) = phi x.

Lemma cfConjgEout phi y : y \notin 'N(G) → (phi ^ y = phi)%CF.

Lemma cfConjgEin phi y (nGy : y \in 'N(G)) :
  (phi ^ y)%CF = cfIsom (norm_conj_isom nGy) phi.

Lemma cfConjgMnorm phi :
  {in 'N(G) &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.

Lemma cfConjg_id phi y : y \in G → (phi ^ y)%CF = phi.

Lemma cfConjgM L phi :
  G <| L → {in L &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.

Lemma cfConjgJ1 phi : (phi ^ 1)%CF = phi.

Lemma cfConjgK y : cancel (cfConjg y) (cfConjg y^-1 : 'CF(G) → 'CF(G)).

Lemma cfConjgKV y : cancel (cfConjg y^-1) (cfConjg y : 'CF(G) → 'CF(G)).

Lemma cfConjg1 phi y : (phi ^ y)%CF 1%g = phi 1%g.

Fact cfConjg_is_linear y : linear (cfConjg y : 'CF(G) → 'CF(G)).
Canonical cfConjg_additive y := Additive (cfConjg_is_linear y).
Canonical cfConjg_linear y := AddLinear (cfConjg_is_linear y).

Lemma cfConjg_cfuniJ A y : y \in 'N(G) → ('1_A ^ y)%CF = '1_(A :^ y) :> 'CF(G).

Lemma cfConjg_cfuni A y : y \in 'N(A) → ('1_A ^ y)%CF = '1_A :> 'CF(G).

Lemma cfConjg_cfun1 y : (1 ^ y)%CF = 1 :> 'CF(G).

Fact cfConjg_is_multiplicative y : multiplicative (cfConjg y : _ → 'CF(G)).
Canonical cfConjg_rmorphism y := AddRMorphism (cfConjg_is_multiplicative y).
Canonical cfConjg_lrmorphism y := [lrmorphism of cfConjg y].

Lemma cfConjg_eq1 phi y : ((phi ^ y)%CF == 1) = (phi == 1).

Lemma cfAutConjg phi u y : cfAut u (phi ^ y) = (cfAut u phi ^ y)%CF.

Lemma conj_cfConjg phi y : (phi ^ y)^*%CF = (phi^* ^ y)%CF.

Lemma cfker_conjg phi y : y \in 'N(G) → cfker (phi ^ y) = cfker phi :^ y.

Lemma cfDetConjg phi y : cfDet (phi ^ y) = (cfDet phi ^ y)%CF.

End Conj.

Section Inertia.

Variable gT : finGroupType.

Definition inertia (B : {set gT}) (phi : 'CF(B)) :=
  [set y in 'N(B) | (phi ^ y)%CF == phi].


Fact group_set_inertia (H : {group gT}) phi : group_set 'I[phi : 'CF(H)].
Canonical inertia_group H phi := Group (@group_set_inertia H phi).


Variables G H : {group gT}.
Implicit Type phi : 'CF(H).

Lemma inertiaJ phi y : y \in 'I[phi] → (phi ^ y)%CF = phi.

Lemma inertia_valJ phi x y : y \in 'I[phi] → phi (x ^ y)%g = phi x.

Lemma Inertia_sub phi : 'I_G[phi] \subset G.

Lemma norm_inertia phi : 'I[phi] \subset 'N(H).

Lemma sub_inertia phi : H \subset 'I[phi].

Lemma normal_inertia phi : H <| 'I[phi].

Lemma sub_Inertia phi : H \subset G → H \subset 'I_G[phi].

Lemma norm_Inertia phi : 'I_G[phi] \subset 'N(H).

Lemma normal_Inertia phi : H \subset G → H <| 'I_G[phi].

Lemma cfConjg_eqE phi :
    H <| G →
  {in G &, ∀ y z, (phi ^ y == phi ^ z)%CF = (z \in 'I_G[phi] :* y)}.

Lemma cent_sub_inertia phi : 'C(H) \subset 'I[phi].

Lemma cent_sub_Inertia phi : 'C_G(H) \subset 'I_G[phi].

Lemma center_sub_Inertia phi : H \subset G → 'Z(G) \subset 'I_G[phi].

Lemma conjg_inertia phi y : y \in 'N(H) → 'I[phi] :^ y = 'I[phi ^ y].

Lemma inertia0 : 'I[0 : 'CF(H)] = 'N(H).

Lemma inertia_add phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi + psi].

Lemma inertia_sum I r (P : pred I) (Phi : I → 'CF(H)) :
  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
     \subset 'I[\sum_(i <- r | P i) Phi i].

Lemma inertia_scale a phi : 'I[phi] \subset 'I[a *: phi].

Lemma inertia_scale_nz a phi : a != 0 → 'I[a *: phi] = 'I[phi].

Lemma inertia_opp phi : 'I[- phi] = 'I[phi].

Lemma inertia1 : 'I[1 : 'CF(H)] = 'N(H).

Lemma Inertia1 : H <| G → 'I_G[1 : 'CF(H)] = G.

Lemma inertia_mul phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi × psi].

Lemma inertia_prod I r (P : pred I) (Phi : I → 'CF(H)) :
  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
     \subset 'I[\prod_(i <- r | P i) Phi i].

Lemma inertia_injective (chi : 'CF(H)) :
  {in H &, injective chi} → 'I[chi] = 'C(H).

Lemma inertia_irr_prime p i :
  #|H| = p → prime p → i != 0 → 'I['chi[H]_i] = 'C(H).

Lemma inertia_irr0 : 'I['chi[H]_0] = 'N(H).

Lemma cfConjg_iso y : isometry (cfConjg y : 'CF(H) → 'CF(H)).

Lemma cfdot_Res_conjg psi phi y :
  y \in G → '['Res[H, G] psi, phi ^ y] = '['Res[H] psi, phi].

Lemma cfConjg_char (chi : 'CF(H)) y :
  chi \is a character → (chi ^ y)%CF \is a character.

Lemma cfConjg_lin_char (chi : 'CF(H)) y :
  chi \is a linear_char → (chi ^ y)%CF \is a linear_char.

Lemma cfConjg_irr y chi : chi \in irr H → (chi ^ y)%CF \in irr H.

Definition conjg_Iirr i y := cfIirr ('chi[H]_i ^ y)%CF.

Lemma conjg_IirrE i y : 'chi_(conjg_Iirr i y) = ('chi_i ^ y)%CF.

Lemma conjg_IirrK y : cancel (conjg_Iirr^~ y) (conjg_Iirr^~ y^-1%g).

Lemma conjg_IirrKV y : cancel (conjg_Iirr^~ y^-1%g) (conjg_Iirr^~ y).

Lemma conjg_Iirr_inj y : injective (conjg_Iirr^~ y).

Lemma conjg_Iirr_eq0 i y : (conjg_Iirr i y == 0) = (i == 0).

Lemma conjg_Iirr0 x : conjg_Iirr 0 x = 0.

Lemma cfdot_irr_conjg i y :
  H <| G → y \in G → '['chi_i, 'chi_i ^ y]_H = (y \in 'I_G['chi_i])%:R.

Definition cfclass (A : {set gT}) (phi : 'CF(A)) (B : {set gT}) :=
  [seq (phi ^ repr Tx)%CF | Tx in rcosets 'I_B[phi] B].


Lemma size_cfclass i : size ('chi[H]_i ^: G)%CF = #|G : 'I_G['chi_i]|.

Lemma cfclassP (A : {group gT}) phi psi :
  reflect (exists2 y, y \in A & psi = phi ^ y)%CF (psi \in phi ^: A)%CF.

Lemma cfclassInorm phi : (phi ^: 'N_G(H) =i phi ^: G)%CF.

Lemma cfclass_refl phi : phi \in (phi ^: G)%CF.

Lemma cfclass_transr phi psi :
  (psi \in phi ^: G)%CF → (phi ^: G =i psi ^: G)%CF.

Lemma cfclass_sym phi psi : (psi \in phi ^: G)%CF = (phi \in psi ^: G)%CF.

Lemma cfclass_uniq phi : H <| G → uniq (phi ^: G)%CF.

Lemma cfclass_invariant phi : G \subset 'I[phi] → (phi ^: G)%CF = phi.

Lemma cfclass1 : H <| G → (1 ^: G)%CF = [:: 1 : 'CF(H)].

Definition cfclass_Iirr (A : {set gT}) i := conjg_Iirr i @: A.

Lemma cfclass_IirrE i j :
  (j \in cfclass_Iirr G i) = ('chi_j \in 'chi_i ^: G)%CF.

Lemma eq_cfclass_IirrE i j :
  (cfclass_Iirr G j == cfclass_Iirr G i) = (j \in cfclass_Iirr G i).

Lemma im_cfclass_Iirr i :
  H <| G → perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF.

Lemma card_cfclass_Iirr i : H <| G → #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.

Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) → R) i :
     H <| G →
  \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
     = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.

Lemma cfResInd j:
    H <| G →
  'Res[H] ('Ind[G] 'chi_j) = #|H|%:R^-1 *: (\sum_(y in G) 'chi_j ^ y)%CF.

Lemma Clifford_Res_sum_cfclass i j :
     H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
  'Res[H] 'chi_i =
     '['Res[H] 'chi_i, 'chi_j] *: (\sum_(chi <- ('chi_j ^: G)%CF) chi).

Lemma cfRes_Ind_invariant psi :
  H <| G → G \subset 'I[psi] → 'Res ('Ind[G, H] psi) = #|G : H|%:R *: psi.

Corollary constt0_Res_cfker i :
  H <| G → 0 \in irr_constt ('Res[H] 'chi[G]_i) → H \subset cfker 'chi[G]_i.

Lemma dvdn_constt_Res1_irr1 i j :
    H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
  ∃ n, 'chi_i 1%g = n%:R × 'chi_j 1%g.

Lemma cfclass_Ind phi psi :
  H <| G → psi \in (phi ^: G)%CF → 'Ind[G] phi = 'Ind[G] psi.

End Inertia.


Notation "''I[' phi ] " := (inertia phi) : group_scope.
Notation "''I[' phi ] " := (inertia_group phi) : Group_scope.
Notation "''I_' G [ phi ] " := (G%g :&: 'I[phi]) : group_scope.
Notation "''I_' G [ phi ] " := (G :&: 'I[phi])%G : Group_scope.
Notation "phi ^: G" := (cfclass phi G) : cfun_scope.

Section ConjRestrict.

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

Lemma cfConjgRes_norm phi y :
  y \in 'N(K) → y \in 'N(H) → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.

Lemma cfConjgRes phi y :
  H <| G → K <| G → y \in G → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.

Lemma sub_inertia_Res phi :
  G \subset 'N(K) → 'I_G[phi] \subset 'I_G['Res[K, H] phi].

Lemma cfConjgInd_norm phi y :
  y \in 'N(K) → y \in 'N(H) → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.

Lemma cfConjgInd phi y :
  H <| G → K <| G → y \in G → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.

Lemma sub_inertia_Ind phi :
  G \subset 'N(H) → 'I_G[phi] \subset 'I_G['Ind[H, K] phi].

End ConjRestrict.

Section MoreInertia.

Variables (gT : finGroupType) (G H : {group gT}) (i : Iirr H).
Let T := 'I_G['chi_i].

Lemma inertia_id : 'I_T['chi_i] = T.

Lemma cfclass_inertia : ('chi[H]_i ^: T)%CF = [:: 'chi_i].

End MoreInertia.

Section ConjMorph.

Variables (aT rT : finGroupType) (D G H : {group aT}) (f : {morphism D >-> rT}).

Lemma cfConjgMorph (phi : 'CF(f @* H)) y :
  y \in D → y \in 'N(H) → (cfMorph phi ^ y)%CF = cfMorph (phi ^ f y).

Lemma inertia_morph_pre (phi : 'CF(f @* H)) :
  H <| G → G \subset D → 'I_G[cfMorph phi] = G :&: f @*^-1 'I_(f @* G)[phi].

Lemma inertia_morph_im (phi : 'CF(f @* H)) :
  H <| G → G \subset D → f @* 'I_G[cfMorph phi] = 'I_(f @* G)[phi].

Variables (R S : {group rT}).
Variables (g : {morphism G >-> rT}) (h : {morphism H >-> rT}).
Hypotheses (isoG : isom G R g) (isoH : isom H S h).
Hypotheses (eq_hg : {in H, h =1 g}) (sHG : H \subset G).

Lemma cfConjgIsom phi y :
  y \in G → y \in 'N(H) → (cfIsom isoH phi ^ g y)%CF = cfIsom isoH (phi ^ y).

Lemma inertia_isom phi : 'I_R[cfIsom isoH phi] = g @* 'I_G[phi].

End ConjMorph.

Section ConjQuotient.

Variables gT : finGroupType.
Implicit Types G H K : {group gT}.

Lemma cfConjgMod_norm H K (phi : 'CF(H / K)) y :
  y \in 'N(K) → y \in 'N(H) → ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.

Lemma cfConjgMod G H K (phi : 'CF(H / K)) y :
    H <| G → K <| G → y \in G →
  ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.

Lemma cfConjgQuo_norm H K (phi : 'CF(H)) y :
  y \in 'N(K) → y \in 'N(H) → ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.

Lemma cfConjgQuo G H K (phi : 'CF(H)) y :
    H <| G → K <| G → y \in G →
  ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.

Lemma inertia_mod_pre G H K (phi : 'CF(H / K)) :
  H <| G → K <| G → 'I_G[phi %% K] = G :&: coset K @*^-1 'I_(G / K)[phi].

Lemma inertia_mod_quo G H K (phi : 'CF(H / K)) :
  H <| G → K <| G → ('I_G[phi %% K] / K)%g = 'I_(G / K)[phi].

Lemma inertia_quo G H K (phi : 'CF(H)) :
    H <| G → K <| G → K \subset cfker phi →
  'I_(G / K)[phi / K] = ('I_G[phi] / K)%g.

End ConjQuotient.

Section InertiaSdprod.

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

Hypothesis defG : K ><| H = G.

Lemma cfConjgSdprod phi y :
    y \in 'N(K) → y \in 'N(H) →
  (cfSdprod defG phi ^ y = cfSdprod defG (phi ^ y))%CF.

Lemma inertia_sdprod (L : {group gT}) phi :
  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfSdprod defG phi] = 'I_L[phi].

End InertiaSdprod.

Section InertiaDprod.

Variables (gT : finGroupType) (G K H : {group gT}).
Implicit Type L : {group gT}.
Hypothesis KxH : K \x H = G.

Lemma cfConjgDprodl phi y :
    y \in 'N(K) → y \in 'N(H) →
  (cfDprodl KxH phi ^ y = cfDprodl KxH (phi ^ y))%CF.

Lemma cfConjgDprodr psi y :
    y \in 'N(K) → y \in 'N(H) →
  (cfDprodr KxH psi ^ y = cfDprodr KxH (psi ^ y))%CF.

Lemma cfConjgDprod phi psi y :
    y \in 'N(K) → y \in 'N(H) →
  (cfDprod KxH phi psi ^ y = cfDprod KxH (phi ^ y) (psi ^ y))%CF.

Lemma inertia_dprodl L phi :
  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodl KxH phi] = 'I_L[phi].

Lemma inertia_dprodr L psi :
  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodr KxH psi] = 'I_L[psi].

Lemma inertia_dprod L (phi : 'CF(K)) (psi : 'CF(H)) :
    L \subset 'N(K) → L \subset 'N(H) → phi 1%g != 0 → psi 1%g != 0 →
  'I_L[cfDprod KxH phi psi] = 'I_L[phi] :&: 'I_L[psi].

Lemma inertia_dprod_irr L i j :
    L \subset 'N(K) → L \subset 'N(H) →
  'I_L[cfDprod KxH 'chi_i 'chi_j] = 'I_L['chi_i] :&: 'I_L['chi_j].

End InertiaDprod.

Section InertiaBigdprod.

Variables (gT : finGroupType) (I : finType) (P : pred I).
Variables (A : I → {group gT}) (G : {group gT}).
Implicit Type L : {group gT}.
Hypothesis defG : \big[dprod/1%g]_(i | P i) A i = G.

Section ConjBig.

Variable y : gT.
Hypothesis nAy: ∀ i, P i → y \in 'N(A i).

Lemma cfConjgBigdprodi i (phi : 'CF(A i)) :
   (cfBigdprodi defG phi ^ y = cfBigdprodi defG (phi ^ y))%CF.

Lemma cfConjgBigdprod phi :
  (cfBigdprod defG phi ^ y = cfBigdprod defG (fun i ⇒ phi i ^ y))%CF.

End ConjBig.

Section InertiaBig.

Variable L : {group gT}.
Hypothesis nAL : ∀ i, P i → L \subset 'N(A i).

Lemma inertia_bigdprodi i (phi : 'CF(A i)) :
  P i → 'I_L[cfBigdprodi defG phi] = 'I_L[phi].

Lemma inertia_bigdprod phi (Phi := cfBigdprod defG phi) :
  Phi 1%g != 0 → 'I_L[Phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].

Lemma inertia_bigdprod_irr Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
  'I_L[cfBigdprod defG phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].

End InertiaBig.

End InertiaBigdprod.

Section ConsttInertiaBijection.

Variables (gT : finGroupType) (H G : {group gT}) (t : Iirr H).
Hypothesis nsHG : H <| G.


Let calA := irr_constt ('Ind[T] theta).
Let calB := irr_constt ('Ind[G] theta).

Theorem constt_Inertia_bijection :
 [/\ (*a*) {in calA, ∀ s, 'Ind[G] 'chi_s \in irr G},
     (*b*) {in calA &, injective (Ind_Iirr G)},
           Ind_Iirr G @: calA =i calB,
     (*c*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
             [predI irr_constt ('Res chi) & calA] =i pred1 s}
   & (*d*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
             '['Res psi, theta] = '['Res chi, theta]}].

End ConsttInertiaBijection.

Section ExtendInvariantIrr.

Variable gT : finGroupType.
Implicit Types G H K L M N : {group gT}.

Section ConsttIndExtendible.

Variables (G N : {group gT}) (t : Iirr N) (c : Iirr G).
Let theta := 'chi_t.
Let chi := 'chi_c.

Definition mul_Iirr b := cfIirr ('chi_b × chi).
Definition mul_mod_Iirr (b : Iirr (G / N)) := mul_Iirr (mod_Iirr b).

Hypotheses (nsNG : N <| G) (cNt : 'Res[N] chi = theta).
Let sNG : N \subset G.
Let nNG : G \subset 'N(N).

Lemma extendible_irr_invariant : G \subset 'I[theta].
Let IGtheta := extendible_irr_invariant.

Theorem constt_Ind_mul_ext f (phi := 'chi_f) (psi := phi × theta) :
  G \subset 'I[phi] → psi \in irr N →
  let calS := irr_constt ('Ind phi) in
  [/\ {in calS, ∀ b, 'chi_b × chi \in irr G},
      {in calS &, injective mul_Iirr},
      irr_constt ('Ind psi) =i [seq mul_Iirr b | b in calS]
    & 'Ind psi = \sum_(b in calS) '['Ind phi, 'chi_b] *: 'chi_(mul_Iirr b)].

Corollary constt_Ind_ext :
  [/\ ∀ b : Iirr (G / N), 'chi_(mod_Iirr b) × chi \in irr G,
      injective mul_mod_Iirr,
      irr_constt ('Ind theta) =i codom mul_mod_Iirr
    & 'Ind theta = \sum_b 'chi_b 1%g *: 'chi_(mul_mod_Iirr b)].

End ConsttIndExtendible.

Theorem invariant_chief_irr_cases G K L s (theta := 'chi[K]_s) :
    chief_factor G L K → abelian (K / L) → G \subset 'I[theta] →
  let t := #|K : L| in
  [\/ 'Res[L] theta \in irr L,
      exists2 e, ∃ p, 'Res[L] theta = e%:R *: 'chi_p & (e ^ 2)%N = t
   | exists2 p, injective p & 'Res[L] theta = \sum_(i < t) 'chi_(p i)].