(Joint Center)Library BGsection14

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div path fintype.
Require Import bigop finset prime fingroup morphism perm automorphism quotient.
Require Import action gproduct gfunctor pgroup cyclic center commutator.
Require Import gseries nilpotent sylow abelian maximal hall frobenius.
Require Import ssralg ssrnum ssrint rat.
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
Require Import BGsection7 BGsection9 BGsection10 BGsection12 BGsection13.

This file covers B & G, section 14, starting with the definition of the sigma-decomposition of elements, sigma-supergroups, and basic categories of maximal subgroups: sigma_decomposition x == the set of nontrivial constituents x.`_\sigma(M), with M ranging over maximal sugroups of G. (x is the product of these). \ell_\sigma[x] == #|sigma_decomposition x|. 'M_\sigma(X) == the set of maximal subgroups M such that X is a a subset of M`_\sigma. 'M_\sigma[x] := 'M_\sigma(< [x]>) \kappa(M) == the set of primes p in \tau1(M) or \tau3(M), such that 'C_(M`_\sigma)(P) != 1 for some subgroup of M of order p, i.e., the primes for which M fails to be a Frobenius group. kappa_complement M U K <-> U and K are respectively {kappa, sigma}'- and kappa-Hall subgroups of M, whose product is a sigma-complement of M. This corresponds to the notation introduced at the start of section 15 in B & G, but is needed here to capture the use of bound variables of 14.2(a) in the statement of Lemma 14.12. 'M_'F == the set of maximal groups M for which \kappa(M) is empty, i.e., the maximal groups of Frobenius type (in the final classification, this becomes Type I). 'M_'P == the complement to 'M_'F in 'M, i.e., the set of M for which at least E1 has a proper prime action on M`_\sigma. 'M_'P1 == the set of maximal subgroups M such that \pi(M) is the disjoint union of \sigma(M) and \kappa(M), i.e., for which the entire complement acts in a prime manner (this troublesome subset of 'M_'P is ultimately refined into Types III-V in the final classification). 'M_'P2 == the complement to 'M_'P1 in 'M_'P; this becomes Type II in the final classification. 'N[x] == if x != 1 and 'M_\sigma[x] > 1, the unique group in 'M('C[x]) (see B & G, Theorem 14.4), and the trivial group otherwise. 'R[x] := 'C_('N[x]`_\sigma) [x]; if \ell_\sigma[x] == 1, this is the normal Hall subgroup of 'C[x] that acts sharply transitively by conjugagtion on 'M`_\sigma[x] (again, by Theorem 14.4). M^~~ == the union of all the cosets x *: 'R[x], with x ranging over (M`_\sigma)^#. This will become the support set for the Dade isometry for M in the character theory part of the proof. It seems 'R[x] and 'N[x]`_\sigma play a somewhat the role of a signalizer functor in the FT proof; in particular 'R[x] will be used to construct the Dade isometry in the character theory part of the proof.

Set Implicit Arguments.

Local Open Scope ring_scope.
Local Open Scope nat_scope.
Import GRing.Theory Num.Theory GroupScope.

Section Definitons.

Variable gT : minSimpleOddGroupType.
Implicit Type x : gT.
Implicit Type M X : {set gT}.

Definition sigma_decomposition x :=
  [set x.`_\sigma(M) | M : {group gT} in 'M]^#.
Definition sigma_length x := #|sigma_decomposition x|.

Definition sigma_mmax_of X := [set M in 'M | X \subset M`_\sigma].

Definition FT_signalizer_base x :=
  if #|sigma_mmax_of <[x]>| > 1 then odflt 1%G (pick (mem 'M('C[x]))) else 1%G.

Definition FT_signalizer x := 'C_((FT_signalizer_base x)`_\sigma)[x].

Definition sigma_cover M := \bigcup_(x in (M`_\sigma)^#) x *: FT_signalizer x.

Definition tau13 M := [predU \tau1(M) & \tau3(M)].

Fact kappa_key : unit.
Definition kappa_def M : nat_pred :=
  [pred p in tau13 M | [ P in 'E_p^1(M), 'C_(M`_\sigma)(P) != 1]].
Definition kappa := locked_with kappa_key kappa_def.
Canonical kappa_unlockable := [unlockable fun kappa].

Definition sigma_kappa M := [predU \sigma(M) & kappa M].

Definition kappa_complement (M U K : {set gT}) :=
  [/\ (sigma_kappa M)^'.-Hall(M) U, (kappa M).-Hall(M) K & group_set (U × K)].

Definition TypeF_maxgroups := [set M in 'M | (kappa M)^'.-group M].

Definition TypeP_maxgroups := 'M :\: TypeF_maxgroups.

Definition TypeP1_maxgroups :=
  [set M in TypeP_maxgroups | (sigma_kappa M).-group M].

Definition TypeP2_maxgroups := TypeP_maxgroups :\: TypeP1_maxgroups.

End Definitons.

Notation "\ell_ \sigma ( x )" := (sigma_length x)
  (at level 8, format "\ell_ \sigma ( x )") : group_scope.

Notation "''M_' \sigma ( X )" := (sigma_mmax_of X)
  (at level 8, format "''M_' \sigma ( X )") : group_scope.

Notation "''M_' \sigma [ x ]" := (sigma_mmax_of <[x]>)
  (at level 8, format "''M_' \sigma [ x ]") : group_scope.

Notation "''N' [ x ]" := (FT_signalizer_base x)
  (at level 8, format "''N' [ x ]") : group_scope.

Notation "''R' [ x ]" := (FT_signalizer x)
  (at level 8, format "''R' [ x ]") : group_scope.

Notation "M ^~~" := (sigma_cover M)
  (at level 2, format "M ^~~") : group_scope.

Notation "\tau13 ( M )" := (tau13 M)
  (at level 8, format "\tau13 ( M )") : group_scope.

Notation "\kappa ( M )" := (kappa M)
  (at level 8, format "\kappa ( M )") : group_scope.

Notation "\sigma_kappa ( M )" := (sigma_kappa M)
  (at level 8, format "\sigma_kappa ( M )") : group_scope.

Notation "''M_' ''F'" := (TypeF_maxgroups _)
  (at level 2, format "''M_' ''F'") : group_scope.

Notation "''M_' ''P'" := (TypeP_maxgroups _)
  (at level 2, format "''M_' ''P'") : group_scope.

Notation "''M_' ''P1'" := (TypeP1_maxgroups _)
  (at level 2, format "''M_' ''P1'") : group_scope.

Notation "''M_' ''P2'" := (TypeP2_maxgroups _)
  (at level 2, format "''M_' ''P2'") : group_scope.

Section Section14.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types p q q_star r : nat.
Implicit Types x y z : gT.
Implicit Types A E H K L M Mstar N P Q Qstar R S T U V W X Y Z : {group gT}.

Basic properties of the sigma decomposition.
General remarks about the sigma-decomposition, p. 105 of B & G.
Basic properties of \kappa and the maximal group subclasses.
Lemma kappaJ M x : \kappa(M :^ x) =i \kappa(M).

Lemma kappa_tau13 M p : p \in \kappa(M)(p \in \tau1(M)) || (p \in \tau3(M)).

Lemma kappa_sigma' M : {subset \kappa(M) \sigma(M)^'}.

Remark rank_kappa M p : p \in \kappa(M)'r_p(M) = 1%N.

Lemma kappa_pi M : {subset \kappa(M) \pi(M)}.

Remark kappa_nonregular M p P :
  p \in \kappa(M)P \in 'E_p^1(M)'C_(M`_\sigma)(P) != 1.

Lemma ex_kappa_compl M K :
    M \in 'M\kappa(M).-Hall(M) K
   U : {group gT}, kappa_complement M U K.

Lemma FtypeP M : reflect (M \in 'M \kappa(M) =i pred0) (M \in 'M_'F).

Lemma PtypeP M : reflect (M \in 'M p, p \in \kappa(M)) (M \in 'M_'P).

Lemma trivg_kappa M K :
  M \in 'M\kappa(M).-Hall(M) K(K :==: 1) = (M \in 'M_'F).

Could go in Section 10.
Lemma not_sigma_mmax M : M \in 'M~~ \sigma(M).-group M.

Lemma trivg_kappa_compl M U K :
  M \in 'Mkappa_complement M U K(U :==: 1) = (M \in 'M_'P1).

Lemma FtypeJ M x : ((M :^ x)%G \in 'M_'F) = (M \in 'M_'F).

Lemma PtypeJ M x : ((M :^ x)%G \in 'M_'P) = (M \in 'M_'P).

Lemma P1typeJ M x : ((M :^ x)%G \in 'M_'P1) = (M \in 'M_'P1).

Lemma P2typeJ M x : ((M :^ x)%G \in 'M_'P2) = (M \in 'M_'P2).

This is B & G, Lemma 14.1.
This is B & G, Proposition 14.2.
Proposition Ptype_structure M K (Ms := M`_\sigma) (Kstar := 'C_Ms(K)) :
  M \in 'M_'P\kappa(M).-Hall(M) K
  [/\ (*a*) exists2 U : {group gT},
              kappa_complement M U K Ms ><| (U ><| K) = M
            & [/\ abelian U, semiprime Ms K & semiregular U K],
      (*b*) (*1.2*) K \x Kstar = 'N_M(K)
            {in 'E^1(K), X,
            (*1.1*) 'N_M(X) = 'N_M(K)
            (*2*) {in 'M('N(X)), Mstar, X \subset Mstar`_\sigma}},
      (*c*) Kstar != 1 {in 'E^1(Kstar), X, 'M('C(X)) = [set M]},
  [/\ (*d*) {in ~: M, g, Kstar :&: M :^ g = 1}
          {in M :\: 'N_M(K), g, K :&: K :^ g = 1},
      (*e*) {in \pi(Kstar), p S,
             p.-Sylow(M) S'M(S) = [set M] ~~ (S \subset Kstar)}
    & (*f*) Y, \sigma(M).-group YY :&: Kstar != 1 → Y \subset Ms]
    & (*g*) M \in 'M_'P2
            [/\ \sigma(M) =i \beta(M), prime #|K|, nilpotent Ms
              & normedTI Ms^# G M]].

This is essentially the skolemized form of 14.2(a).
Lemma kappa_compl_context M U K :
    M \in 'Mkappa_complement M U K
  [/\ \sigma(M)^'.-Hall(M) (U <*> K),
      M`_\sigma ><| (U ><| K) = M,
      semiprime M`_\sigma K,
      semiregular U K
    & K :!=: 1 → abelian U].

This is B & G, Corollary 14.3.
Corollary pi_of_cent_sigma M x x' :
    M \in 'Mx \in (M`_\sigma)^#
    x' \in ('C_M[x])^#\sigma(M)^'.-elt x'
     (*1*) \kappa(M).-elt x' 'C[x] \subset M
   (*2*) [/\ \tau2(M).-elt x', \ell_\sigma(x') == 1%N & 'M('C[x']) = [set M]].

This is B & G, Theorem 14.4. We are omitting the first half of part (a), since we have taken it as our definition of 'R[x].
Theorem FT_signalizer_context x (N := 'N[x]) (R := 'R[x]) :
    \ell_\sigma(x) == 1%N
  [/\ [/\ [transitive R, on 'M_\sigma[x] | 'JG],
          #|R| = #|'M_\sigma[x]|,
          R <| 'C[x]
        & Hall 'C[x] R]
   & #|'M_\sigma[x]| > 1 →
  [/\ 'M('C[x]) = [set N],
    (*a*) R :!=: 1,
    (*c1*) \tau2(N).-elt x,
     (*f*) N \in 'M_'F :|: 'M_'P2
    & {in 'M_\sigma[x], M,
  [/\ (*b*) R ><| 'C_(M :&: N)[x] = 'C[x],
     (*c2*) {subset \tau2(N) \sigma(M)},
      (*d*) {subset [predI \pi(M) & \sigma(N)] \beta(N)}
    & (*e*) \sigma(N)^'.-Hall(N) (M :&: N)]}]].

A useful supplement to Theorem 14.4.
Because the definition of 'N[x] uses choice, we can only prove it commutes with conjugation now that we have established that the choice is unique.
This is the remark imediately above B & G, Lemma 14.5; note the adjustment allowing for the case x' = 1.
Remark sigma_cover_decomposition x x' :
    \ell_\sigma(x) == 1%Nx' \in 'R[x]
  sigma_decomposition (x × x') = x |: [set x']^#.

This is the simplified form of remark imediately above B & G, Lemma 14.5.
Remark nt_sigma_cover_decomposition x x' :
    \ell_\sigma(x) == 1%Nx' \in 'R[x]^#
  sigma_decomposition (x × x') = [set x; x'].

Remark mem_sigma_cover_decomposition x g :
  \ell_\sigma(x) == 1%Ng \in x *: 'R[x]x \in sigma_decomposition g.

Remark ell_sigma_cover x g :
  \ell_\sigma(x) == 1%Ng \in x *: 'R[x]\ell_\sigma(g) 2.

Remark ell_sigma_support M g : M \in 'Mg \in M^~~\ell_\sigma(g) 2.

This is B & G, Lemma 14.5(a).
Lemma sigma_cover_disjoint x y :
    \ell_\sigma(x) == 1%N\ell_\sigma(y) == 1%Nx != y
  [disjoint x *: 'R[x] & y *: 'R[y]].

This is B & G, Lemma 14.5(b).
Lemma sigma_support_disjoint M1 M2 :
  M1 \in 'MM2 \in 'Mgval M2 \notin M1 :^: G[disjoint M1^~~ & M2^~~].

This is B & G, Lemma 14.5(c).
This is B & G, Lemma 14.6.
Lemma sigma_decomposition_dichotomy (g : gT) :
   g != 1 →
     [ (x | \ell_\sigma(x) == 1%N), x^-1 × g \in 'R[x]]
(+) [ (y | \ell_\sigma(y) == 1%N),
      let y' := y^-1 × g in
      [ M in 'M_\sigma[y], (y' \in ('C_M[y])^#) && \kappa(M).-elt y']].

Section PTypeEmbedding.
Implicit Types Mi Mj : {group gT}.
Implicit Type Ks : {set gT}.

This is B & G, Theorem 14.7. This theorem provides the basis for the maximal subgroup classification, the main output of the local analysis. Note that we handle differently the two separate instances of non-structural proof (by analogy) that occur in the textbook, p. 112, l. 7 and p. 113, l. 22. For the latter we simply use global induction on the size of the class support of the TI-set \hat{Z} (for this reason we have kept the assertion that this is greater than half of the size of G, even though this is not used later in the proof; we did drop the more precise lower bound). For the former we prove a preliminary lemma that summarizes the four results of the beginning of the proof that used after p. 112, l. 7 -- note that this also gets rid of a third non structural argument (on p. 112, l. 5). Also, note that the direct product decomposition of Z and the K_i, and its direct relation with the sigma-decomposition of elements of Z (p. 112, l. 13-19) is NOT materially used in the rest of the argument, though it does obviously help a human reader forge a mental picture of the situation at hand. Only the first remark, l. 13, is used to prove the alternative definition of T implicit in the remarks l. 22-23. Accordingly, we have suppressed most of these intermediate results: we have only kept the proof that Z is the direct product of the K_i^*, though we discard this result immediately (its 24-line proof just nudges the whole proof size slightyly over the 600-line bar).
Theorem Ptype_embedding M K :
    M \in 'M_'P\kappa(M).-Hall(M) K
  exists2 Mstar, Mstar \in 'M_'P gval Mstar \notin M :^: G
  & let Kstar := 'C_(M`_\sigma)(K) in
    let Z := K <*> Kstar in let Zhat := Z :\: (K :|: Kstar) in
  [/\ (*a*) {in 'E^1(K), X, 'M('C(X)) = [set Mstar]},
      (*b*) \kappa(Mstar).-Hall(Mstar) Kstar \sigma(M).-Hall(Mstar) Kstar,
      (*c*) 'C_(Mstar`_\sigma)(Kstar) = K \kappa(M) =i \tau1(M),
      (*d*) [/\ cyclic Z, M :&: Mstar = Z,
                {in K^#, x, 'C_M[x] = Z},
                {in Kstar^#, y, 'C_Mstar[y] = Z}
              & {in K^# & Kstar^#, x y, 'C[x × y] = Z}]
& [/\ (*e*) [/\ normedTI Zhat G Z, {in ~: M, g, [disjoint Zhat & M :^ g]}
              & (#|G|%:R / 2%:R < #|class_support Zhat G|%:R :> rat)%R ],
      (*f*) M \in 'M_'P2 prime #|K| Mstar \in 'M_'P2 prime #|Kstar|,
      (*g*) {in 'M_'P, H, gval H \in M :^: G :|: Mstar :^: G}
    & (*h*) M^`(1) ><| K = M]].

End PTypeEmbedding.

This is the first part of B & G, Corollary 14.8.
Corollary P1type_trans : {in 'M_'P1 &, M H, gval H \in M :^: G}.

This is the second part of B & G, Corollary 14.8.
Corollary Ptype_trans : {in 'M_'P, M,
  exists2 Mstar, Mstar \in 'M_'P gval Mstar \notin M :^: G
  & {in 'M_'P, H, gval H \in M :^: G :|: Mstar :^: G}}.

This is B & G, Corollary 14.9.
Corollary mFT_partition :
  let Pcover := [set class_support M^~~ G | M : {group gT} in 'M] in
  [/\ (*1*) 'M_'P == set0 :> {set {group gT}}partition Pcover G^#
    & (*2*) M K, M \in 'M_'P\kappa(M).-Hall(M) K
            let Ks := 'C_(M `_\sigma)(K) in let Z := K <*> Ks in
            let Zhat := Z :\: (K :|: Ks) in
            let ClZhat := class_support Zhat G in
            partition (ClZhat |: Pcover) G^# ClZhat \notin Pcover].

This is B & G, Corollary 14.10.
This is B & G, Lemma 14.11.
Lemma primes_non_Fitting_Ftype M E q Q :
    M \in 'M_'F\sigma(M)^'.-Hall(M) E
    Q \in 'E_q^1(E)~~ (Q \subset 'F(E))
  exists2 Mstar, Mstar \in 'M &
  [\/ (*1*) q \in \tau2(Mstar) 'M('C(Q)) = [set Mstar]
    | (*2*) q \in \kappa(Mstar) Mstar \in 'M_'P1 ].

This is B & G, Lemma 14.12. Note that the assumption M \in 'M_'P2 could be weakened to M \in 'M_'P, since the assumption H \in 'M('N(R)) implies H != 1, and hence U != 1.
Lemma P2type_signalizer M Mstar U K r R H :
    M \in 'M_'P2kappa_complement M U KMstar \in 'M('C(K))
    r.-Sylow(U) RH \in 'M('N(R))
  [/\ H \in 'M_'F, U \subset H`_\sigma, U <*> K = M :&: H
   & [/\ ~~ ('N_H(U) \subset M), K \subset 'F(H :&: Mstar)
       & \sigma(H)^'.-Hall(H) (H :&: Mstar)]].

This is B & G, Lemma 14.13(a). Part (b) is not needed for the Peterfalvi revision of the character theory part of the proof.