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

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