# Library mathcomp.character.inertia

(* (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 ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype div tuple finfun bigop prime order.
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.
From mathcomp Require Import archimedean.

Set Implicit Arguments.

Import Order.TTheory 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)).
Local Notation G := <<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)).

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

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

Local Notation "''I[' phi ]" := (inertia phi) : group_scope.
Local Notation "''I_' G [ phi ]" := (G%g :&: 'I[phi]) : group_scope.

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

Local Notation "''I[' phi ]" := (inertia_group phi) : Group_scope.
Local Notation "''I_' G [ phi ]" := (G :&: 'I[phi])%G : Group_scope.

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

Local Notation "phi ^: G" := (cfclass phi G) : cfun_scope.

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.

Arguments inertia {gT B%g} phi%CF.
Arguments cfclass {gT A%g} phi%CF B%g.
Arguments conjg_Iirr_inj {gT H} y [i1 i2] : rename.

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.

Local Notation theta := 'chi_t.
Local Notation T := 'I_G[theta]%G.
Local Notation " 'T'" := 'I_(gval G)[theta]
(at level 0, format " 'T'") : group_scope.

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

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).
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 × Num.trunc (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)