(Joint Center)Library PFsection9

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime binomial ssralg poly finset.
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
Require Import gfunctor gproduct cyclic commutator center gseries nilpotent.
Require Import pgroup sylow hall abelian maximal frobenius.
Require Import matrix mxalgebra mxrepresentation mxabelem vector.
Require Import BGsection1 BGsection3 BGsection7 BGsection15 BGsection16.
Require Import algC classfun character inertia vcharacter.
Require Import PFsection1 PFsection2 PFsection3 PFsection4.
Require Import PFsection5 PFsection6 PFsection8.

This file covers Peterfalvi, Section 9: On the maximal subgroups of Types II, III and IV. For defW : W1 \x W2 = W, MtypeP : of_typeP M U defW, and H := M`_\F we define : Ptype_Fcore_kernel MtypeP == a maximal normal subgroup of M contained (locally) H0 in H and containing 'C_H(U), provided M is a maximal subgroup not of type V. Ptype_Fcore_kernel MtypeP == the stabiliser of Hbar := H / H0 in U; this (locally to this file) C is locked for performance reasons. typeP_Galois MtypeP <=> U acts irreducibly on Hbar; this implies that M / H0C is isomorphic to a Galois group acting on the additive and a subgroup of the multiplicative group of a finite field). > This predicate reflects alternative (b) in Peterfalvi (9.7).

Set Implicit Arguments.

Import GroupScope GRing.Theory FinRing.Theory.

Section Nine.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types (p q : nat) (x y z : gT).
Implicit Types H K L N P Q R S T U V W : {group gT}.

Peterfalvi (9.1) is covered by BGsection3.Frobenius_Wielandt_fixpoint.
These assumptions correspond to Peterfalvi, Hypothesis (9.2).

Variables M U W W1 W2 : {group gT}.
Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP: of_typeP M U defW).
Hypothesis notMtype5 : FTtype M != 5.

Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
Local Notation H := `M`_\F%G.
Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
Local Notation HU := M^`(1)%G.
Local Notation "` 'HU'" := `M^`(1) (at level 0) : group_scope.
Local Notation U' := U^`(1)%G.
Local Notation "` 'U''" := `U^`(1) (at level 0) : group_scope.

Let q := #|W1|.

Let defM : HU ><| W1 = M.
Let defHU : H ><| U = HU.
Let nUW1 : W1 \subset 'N(U).
Let cHU' : U' \subset 'C(H).

Let notMtype1 : FTtype M != 1%N.

Local Notation Mtype24 := (compl_of_typeII_IV maxM MtypeP notMtype5).
Let ntU : U :!=: 1.
Let pr_q : prime q.
Let ntW2 : W2 :!=: 1.
Let sW2H : W2 \subset H.
Let defW2 : 'C_H(W1) = W2.

Lemma Ptype_Fcore_sdprod : H ><| (U <*> W1) = M.
Local Notation defHUW1 := Ptype_Fcore_sdprod.

Lemma Ptype_Fcore_coprime : coprime #|H| #|U <*> W1|.
Let coH_UW1 := Ptype_Fcore_coprime.
Let coHU : coprime #|H| #|U|.

Let not_cHU : ~~ (U \subset 'C(H)).

Lemma Ptype_compl_Frobenius : [Frobenius U <*> W1 = U ><| W1].
Local Notation frobUW1 := Ptype_compl_Frobenius.

Let nilH : nilpotent H.
Let solH : solvable H.

This is Peterfalvi (9.3).
Lemma typeII_IV_core (p := #|W2|) :
  if FTtype M == 2 then 'C_H(U) = 1 #|H| = (#|W2| ^ q)%N
  else [/\ prime p, 'C_H(U <*> W1) = 1 & #|H| = (p ^ q × #|'C_H(U)|)%N].

Existential witnesses for Peterfalvi (9.4).
Definition Ptype_Fcore_kernel of of_typeP M U defW :=
  odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0].
Let H0 := (Ptype_Fcore_kernel MtypeP).
Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
Local Notation Hbar := (H / `H0)%G.
Local Notation "` 'Hbar'" := (`H / `H0)%g (at level 0) : group_scope.
Let p := pdiv #|Hbar|.

This corresponds to Peterfalvi (9.4).
This is Peterfalvi, Hypothesis (9.5).
Fact Ptype_Fcompl_kernel_key : unit.
Definition Ptype_Fcompl_kernel :=
  locked_with Ptype_Fcompl_kernel_key 'C_U(Hbar | 'Q)%G.
Local Notation C := Ptype_Fcompl_kernel.
Local Notation "` 'C'" := (gval C) (at level 0, only parsing) : group_scope.
Local Notation Ubar := (U / `C)%G.
Local Notation "` 'Ubar'" := (`U / `C)%g (at level 0) : group_scope.
Local Notation W1bar := (W1 / `H0)%G.
Local Notation "` 'W1bar'" := (`W1 / `H0)%g (at level 0) : group_scope.
Local Notation W2bar := 'C_Hbar(`W1bar)%G.
Local Notation "` 'W2bar'" := 'C_`Hbar(`W1bar) (at level 0) : group_scope.
Let c := #|C|.
Let u := #|Ubar|.
Local Notation tau := (FT_Dade0 maxM).
Local Notation "chi ^\tau" := (tau chi).
Let calX := Iirr_kerD M^`(1) H 1.
Let calS := seqIndD M^`(1) M M`_\F 1.
Let X_ Y := Iirr_kerD M^`(1) H Y.
Let S_ Y := seqIndD M^`(1) M M`_\F Y.

Local Notation inMb := (coset (gval H0)).

Local Notation H0C := (`H0 <*> `C)%G.
Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
Local Notation HC := (`H <*> `C)%G.
Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
Local Notation H0U' := (`H0 <*> `U')%G.
Local Notation "` 'H0U''" := (gval H0 <*> `U')%G (at level 0) : group_scope.
Local Notation H0C' := (`H0 <*> `C^`(1)%g)%G.
Local Notation "` 'H0C''" := (`H0 <*> `C^`(1)) (at level 0) : group_scope.

Let defW2bar : W2bar :=: W2 / H0.

Let sCU : C \subset U.

Let nsCUW1 : C <| U <*> W1.

Lemma Ptype_Fcore_extensions_normal :
  [/\ H0C <| M, HC <| M, H0U' <| M & H0C' <| M].
Local Notation nsH0xx_M := Ptype_Fcore_extensions_normal.

Let Du: u = #|HU : HC|.

This is Peterfalvi (9.6).
The first assertion of (9.4)(b) (the rest is subsumed by (9.6)).
This is Peterfalvi (9.7)(a).
Lemma typeP_Galois_Pn :
    ~~ typeP_Galois
  {H1 : {group coset_of H0} |
    [/\ #|H1| = p, U / H0 \subset 'N(H1), [acts U, on H1 | 'Q],
        \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar
      & let a := #|U : 'C_U(H1 | 'Q)| in
        [/\ a > 1, a %| p.-1, cyclic (U / 'C_U(H1 | 'Q))
          & V : {group 'rV['Z_a]_q.-1}, Ubar \isog V]]}.

This is Peterfalvi (9.7)(b). Note that part of this statement feeds directly into the final chapter of the proof (BGappendixC), and is not used before, so it may be useful to reformulate to suit the needs of this part. For example, we supply separately the three component of the semi-direct product isomorphism, because no use is made of the global isomorphism. We also state explicitly that the image of W2bar is Fp because this is the fact used in B & G, Appendix C, it is readily available during the proof, whereas it can only be derived from the original statement of (9.7)(b) by using Galois theory. Indeed the Galois part of the isomorphism is only needed for this -- so with the formulation below it will not be used. In order to avoid the use of the Wedderburn theorem on finite division rings we build the field F from the enveloping algebra of the representation of U rather than its endomorphism ring: then the fact that Ubar is abelian yields commutativity directly.
Lemma typeP_Galois_P :
    typeP_Galois
  {F : finFieldType & {phi : {morphism Hbar >-> F}
     & {psi : {morphism U >-> {unit F}} & {eta : {morphism W1 >-> {perm F}}
   & alpha : {perm F}, reflect (rmorphism alpha) (alpha \in eta @* W1)
   & [/\ 'injm eta, {in Hbar & W1, morph_act 'Q 'P phi eta}
       & {in U & W1, x w, val (psi (x ^ w)) = eta w (val (psi x))}]}
   & 'ker psi = C {in Hbar & U, morph_act 'Q 'U phi psi}}
   & [/\ #|F| = (p ^ q)%N, isom Hbar [set: F] phi & phi @* W2bar = <[1%R : F]>]}
   & [/\ cyclic Ubar, coprime u p.-1 & u %| (p ^ q).-1 %/ p.-1]}.

Local Open Scope ring_scope.

Let redM := [predC irr M].
Let mu_ := filter redM (S_ H0).

This subproof is shared between (9.8)(b) and (9.9)(b).
Let nb_redM_H0 : size mu_ = p.-1 {subset mu_ S_ H0C}.

Let isIndHC (zeta : 'CF(M)) :=
  [/\ zeta 1%g = (q × u)%:R, zeta \in S_ H0C
    & exists2 xi : 'CF(HC), xi \is a linear_char & zeta = 'Ind xi].

This is Peterfalvi (9.8).
Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) :
    let a := #|U : 'C_U(sval (typeP_Galois_Pn not_Galois) | 'Q)| in
  [/\ (*a*) {in X_ H0, s, (a %| 'chi_s 1%g)%C},
      (*b*) size mu_ = p.-1 {in mu_, mu_j, isIndHC mu_j},
      (*c*) t, isIndHC 'chi_t
    & (*d*) let irr_qa := [pred zeta in irr M | zeta 1%g == (q × a)%:R] in
            let lb_n := (p.-1 × #|U|)%N in let lb_d := (a ^ 2 × #|U'|)%N in
            (lb_d %| lb_n lb_n %/ lb_d count irr_qa (S_ H0U'))%N].

Import ssrnum Num.Theory.

This is Peterfalvi (9.9); we have exported the fact that HU / H0 is a Frobenius group in case (c), as this is directly used in (9.10).
Lemma typeP_Galois_characters (is_Galois : typeP_Galois) :
  [/\ (*a*) {in X_ H0, s, (u %| 'chi_s 1%g)%Cx},
            {in X_ H0C', s, 'chi_s 1%g = u%:R
             (exists2 xi : 'CF(HC), xi \is a linear_char & 'chi_s = 'Ind xi)},
      (*b*) size mu_ = p.-1 {in mu_, mu_j, isIndHC mu_j}
    & (*c*) all redM (S_ H0C') →
            [/\ C :=: 1%g, u = (p ^ q).-1 %/ p.-1
              & [Frobenius HU / H0 = Hbar ><| (U / H0)]]].

This combination of (9.8)(b) and (9.9)(b) covers most uses of these lemmas in sections 10-14.
Lemma typeP_reducible_core_Ind (ptiWM := FT_primeTI_hyp MtypeP) :
  [/\ size mu_ = p.-1, has predT mu_,
      {subset mu_ [seq primeTIred ptiWM j | j in predC1 0]}
    & {in mu_, mu_j, isIndHC mu_j}].

This is Peterfalvi (9.10), formulated as a constructive alternative.
Lemma typeP_reducible_core_cases :
  {t : Iirr M & 'chi_t \in S_ H0C' 'chi_t 1%g = (q × u)%:R
              & {xi | xi \is a linear_char & 'chi_t = 'Ind[M, HC] xi}}
  + [/\ typeP_Galois, [Frobenius HU / H0 = Hbar ><| (U / H0)],
        cyclic U, #|U| = (p ^ q).-1 %/ p.-1
      & FTtype M == 2 → [Frobenius HU = H ><| U]].

Import ssrint.

This is Peterfalvi (9.11) We had to cover a small gap in step (9.11.4) of the proof, which starts by proving that U1 \subset {1} u A(M), then asserts this obviously implies HU1 \subset {1} u A(M). It is not, as while {1} u A(M) does contain H, it is not (necessarily) a subgroup. We had to use the solvability of HU1 in a significant way (using Philip Hall's theorems) to bridge the gap; it's also possible to exploit lemma (2.1) (partition_cent_rcoset in PFsection1) in a slightly different argument, but the inference is nontrivial in either case.