Library mathcomp.character.inertia

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.

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.

Implicit Arguments conjg_Iirr_inj [gT H x1 x2].

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

Corollary cfRes_prime_irr_cases G N s p (chi := 'chi[G]_s) :
    N <| G → #|G : N| = p → prime p →
  [\/ 'Res[N] chi \in irr N
   | exists2 c, injective c & 'Res[N] chi = \sum_(i < p) 'chi_(c i)].