+ +

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

+ +

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

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

+ +

+ Isaacs' 6.1.d +

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

+ +

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

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

+ +

+ This is Isaacs, Corollary (6.7). +

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

+ +

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

+ +

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

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

+ +

+ This is Isaacs, Corollary (6.17) (due to Gallagher). +

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

+ +

+ This is Isaacs, Theorem (6.19). +

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

+ +

+ This is Isaacs, Corollary (6.19). +

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

+ +

+ This is Isaacs, Corollary (6.20). +

+Corollary prime_invariant_irr_extendible G N s p :
+ N <| G → #|G : N | = p → prime p → G \subset 'I ['chi_s ] →
+ {t | 'Res [N , G ] 'chi_t = 'chi_s }.
+ +
+

+ +

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

+Theorem solvable_irr_extendible_from_det G N s (theta := 'chi [N ]_s) :
+    N <| G → solvable (G / N) →
+    G \subset 'I [theta ] → coprime #|G : N | (truncC (theta 1%g)) →
+  [∃ c, 'Res 'chi [G ]_c == theta ]
+    = [∃ u, 'Res 'chi [G ]_u == cfDet theta ].
+ +
+

+ +

+ This is Isaacs, Theorem (6.26). +

+Theorem extend_linear_char_from_Sylow G N (lambda : 'CF (N )) :
+    N <| G → lambda \is a linear_char → G \subset 'I [lambda ] →
+    (∀ p, p \in \pi ('o (lambda )%CF) →
+       exists2 Hp : {group gT },
+         [/\ N \subset Hp , Hp \subset G & p .-Sylow (G / N ) (Hp / N)%g]
+       & ∃ u, 'Res 'chi [Hp ]_u = lambda ) →
+  ∃ u, 'Res [N , G ] 'chi_u = lambda.
+ +
+

+ +

+ This is Isaacs, Corollary (6.27). +

+Corollary extend_coprime_linear_char G N (lambda : 'CF (N )) :
+    N <| G → lambda \is a linear_char → G \subset 'I [lambda ] →
+    coprime #|G : N | 'o (lambda )%CF →
+  ∃ u, [/\ 'Res 'chi [G ]_u = lambda , 'o ('chi_u )%CF = 'o (lambda )%CF
+              & ∀ v,
+                  'Res 'chi_v = lambda → coprime #|G : N | 'o ('chi_v )%CF →
+                v = u ].
+ +
+

+ +

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

+Theorem inertia_Frobenius_ker i : i != 0 → 'I_G ['chi [K ]_i ] = K.
+ +
+

+ +

+ This is Isaacs, Theorem 6.34(a2) +

+Theorem irr_induced_Frobenius_ker i : i != 0 → 'Ind [G , K ] 'chi_i \in irr G.
+ +
+

+ +

+ This is Isaacs, Theorem 6.34(b) +

+Theorem Frobenius_Ind_irrP j :
+ reflect (exists2 i, i != 0 & 'chi_j = 'Ind [G , K ] 'chi_i)
+ (~~ (K \subset cfker 'chi_j )).
+ +
+End Frobenius.
+