# Library mathcomp.character.inertia

(* (c) Copyright 2006-2016 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.

This file contains the definitions and properties of inertia groups: (phi ^ y)%CF == the y-conjugate of phi : 'CF(G), i.e., the class function mapping x ^ y to phi x provided y normalises G. We take (phi ^ y)%CF = phi when y \notin 'N(G). (phi ^: G)%CF == the sequence of all distinct conjugates of phi : 'CF(H) by all y in G. 'I[phi] == the inertia group of phi : CF(H), i.e., the set of y such that (phi ^ y)%CF = phi AND H :^ y = y. 'I_G[phi] == the inertia group of phi in G, i.e., G :&: 'I[phi]. conjg_Iirr i y == the index j : Iirr G such that ('chi_i ^ y)%CF = 'chi_j. cfclass_Iirr G i == the image of G under conjg_Iirr i, i.e., the set of j such that 'chi_j \in ('chi_i ^: G)%CF. mul_Iirr i j == the index k such that 'chi_j * 'chi_i = 'chi[G]_k, or 0 if 'chi_j * 'chi_i is reducible. mul_mod_Iirr i j := mul_Iirr i (mod_Iirr j), for j : Iirr (G / H).

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.

Isaacs' 6.1.b
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_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.

To disambiguate basic inclucion lemma names we capitalize Inertia for lemmas concerning the localized inertia group 'I_G[phi].
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).

Isaacs' 6.1.c
Isaacs' 6.1.d
Isaac's 6.1.e
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.

This is Isaacs, Theorem (6.2)
This is Isaacs, Corollary (6.7).
This is Isaacs, Lemma (6.8).
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).

This does not depend on the (isoG : isom G R g) assumption.
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.

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

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

This is Isaacs, Theorem (6.11).
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.

This is Isaacs, Theorem (6.16)
This is Isaacs, Corollary (6.17) (due to Gallagher).
This is Isaacs, Theorem (6.19).
This is Isaacs, Corollary (6.19).
This is Isaacs, Corollary (6.20).
This is Isaacs, Lemma (6.24).
Lemma extend_to_cfdet G N s c0 u :
let theta := 'chi_s in let lambda := cfDet theta in let mu := 'chi_u in
N <| G coprime #|G : N| (truncC (theta 1%g))
'Res[N, G] 'chi_c0 = theta 'Res[N, G] mu = lambda
exists2 c, 'Res 'chi_c = theta cfDet 'chi_c = mu
& c1, 'Res 'chi_c1 = theta cfDet 'chi_c1 = mu c1 = c.

This is Isaacs, Theorem (6.25).
This is Isaacs, Theorem (6.26).
This is Isaacs, Corollary (6.27).
This is Isaacs, Corollary (6.28).
Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) :
N <| G solvable (G / N) G \subset 'I[theta]
coprime #|G : N| ('o(theta)%CF × truncC (theta 1%g))
c, [/\ 'Res 'chi[G]_c = theta, 'o('chi_c)%CF = 'o(theta)%CF
& d,
'Res 'chi_d = theta coprime #|G : N| 'o('chi_d)%CF
d = c].

End ExtendInvariantIrr.

Section Frobenius.

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

Because he only defines Frobenius groups in chapter 7, Isaacs does not state these theorems using the Frobenius property.
Hypothesis frobGK : [Frobenius G with kernel K].

This is Isaacs, Theorem 6.34(a1).
This is Isaacs, Theorem 6.34(a2)
This is Isaacs, Theorem 6.34(b)