(Joint Center)Library MathComp.inertia

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice div.
Require Import fintype tuple finfun bigop prime ssralg ssrnum finset fingroup.
Require Import morphism perm automorphism quotient action zmodp cyclic center.
Require Import gproduct commutator gseries nilpotent pgroup sylow maximal.
Require Import frobenius.
Require Import matrix mxalgebra mxrepresentation vector algC classfun character.

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

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].
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 GH \subset 'I_G[phi].

Lemma norm_Inertia phi : 'I_G[phi] \subset 'N(H).

Lemma normal_Inertia phi : H \subset GH <| '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| = pprime pi != 0 → 'I['chi[H]_i] = 'C(H).

Lemma inertia_irr0 : 'I['chi[H]_0] = 'N(H).

Isaacs' 6.1.c
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 <| Gy \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_transl 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 <| Guniq (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 <| Gperm_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 <| Gj \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 <| GG \subset 'I[psi]'Res ('Ind[G, H] psi) = #|G : H|%:R *: psi.

This is Isaacs, Corollary (6.7).
This is Isaacs, Lemma (6.8).
Lemma dvdn_constt_Res1_irr1 i j :
    H <| Gj \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 <| Gpsi \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 <| GK <| Gy \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 <| GK <| Gy \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 Dy \in 'N(H) → (cfMorph phi ^ y)%CF = cfMorph (phi ^ f y).

Lemma inertia_morph_pre (phi : 'CF(f @* H)) :
  H <| GG \subset D'I_G[cfMorph phi] = G :&: f @*^-1 'I_(f @* G)[phi].

Lemma inertia_morph_im (phi : 'CF(f @* H)) :
  H <| GG \subset Df @* '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 Gy \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 <| GK <| Gy \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 <| GK <| Gy \in G
  ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.

Lemma inertia_mod_pre G H K (phi : 'CF(H / K)) :
  H <| GK <| 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 <| GK <| G → ('I_G[phi %% K] / K)%g = 'I_(G / K)[phi].

Lemma inertia_quo G H K (phi : 'CF(H)) :
    H <| GK <| GK \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 iy \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 iL \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)
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).
This is Isaacs, Theorem (6.19).
Theorem invariant_chief_irr_cases G K L s (theta := 'chi[K]_s) :
    chief_factor G L Kabelian (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| = pprime 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| = pprime pG \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 <| Gcoprime #|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 = thetacfDet 'chi_c1 = muc1 = c.

This is Isaacs, Theorem (6.25).
Theorem solvable_irr_extendible_from_det G N s (theta := 'chi[N]_s) :
    N <| Gsolvable (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 <| Glambda \is a linear_charG \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 <| Glambda \is a linear_charG \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 = lambdacoprime #|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 <| Gsolvable (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 = thetacoprime #|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)
Theorem Frobenius_Ind_irrP j :
  reflect (exists2 i, i != 0 & 'chi_j = 'Ind[G, K] 'chi_i)
          (~~ (K \subset cfker 'chi_j)).

End Frobenius.