- -

Library mathcomp.character.inertia

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-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.
-