(Joint Center)Library BGsection10

(* (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.
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
Require Import BGsection7 BGsection9.

This file covers B & G, section 10, including with the definitions: \alpha(M) == the primes p such that M has p-rank at least 3. \beta(M) == the primes p in \alpha(M) such that Sylow p-subgroups of M are not narrow (see BGsection5), i.e., such that M contains no maximal elementary abelian subgroups of rank 2. In a minimal counter-example G, \beta(M) is the intersection of \alpha(M) and \beta(G). Note that B & G refers to primes in \beta(G) as ``ideal'' primes, somewhat inconsistently. \sigma(M) == the primes p such that there exists a p-Sylow subgroup P of M whose normaliser (in the minimal counter-example) is contained in M. M`_\alpha == the \alpha(M)-core of M. M`_\beta == the \beta(M)-core of M. M`_\sigma == the \sigma(M)-core of M.

Set Implicit Arguments.

Import GroupScope.

Reserved Notation "\alpha ( M )" (at level 2, format "\alpha ( M )").
Reserved Notation "\beta ( M )" (at level 2, format "\beta ( M )").
Reserved Notation "\sigma ( M )" (at level 2, format "\sigma ( M )").

Reserved Notation "M `_ \alpha" (at level 3, format "M `_ \alpha").
Reserved Notation "M `_ \beta" (at level 3, format "M `_ \beta").
Reserved Notation "M `_ \sigma" (at level 3, format "M `_ \sigma").

Section Def.

Variable gT : finGroupType.
Implicit Type p : nat.

Variable M : {set gT}.

Definition alpha := [pred p | 2 < 'r_p(M)].
Definition alpha_core := 'O_alpha(M).
Canonical Structure alpha_core_group := Eval hnf in [group of alpha_core].

Definition beta :=
  [pred p | [ (P : {group gT} | p.-Sylow(M) P), ~~ p.-narrow P]].
Definition beta_core := 'O_beta(M).
Canonical Structure beta_core_group := Eval hnf in [group of beta_core].

Definition sigma :=
  [pred p | [ (P : {group gT} | p.-Sylow(M) P), 'N(P) \subset M]].
Definition sigma_core := 'O_sigma(M).
Canonical Structure sigma_core_group := Eval hnf in [group of sigma_core].

End Def.

Notation "\alpha ( M )" := (alpha M) : group_scope.
Notation "M `_ \alpha" := (alpha_core M) : group_scope.
Notation "M `_ \alpha" := (alpha_core_group M) : Group_scope.

Notation "\beta ( M )" := (beta M) : group_scope.
Notation "M `_ \beta" := (beta_core M) : group_scope.
Notation "M `_ \beta" := (beta_core_group M) : Group_scope.

Notation "\sigma ( M )" := (sigma M) : group_scope.
Notation "M `_ \sigma" := (sigma_core M) : group_scope.
Notation "M `_ \sigma" := (sigma_core_group M) : Group_scope.

Section CoreTheory.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Type x : gT.
Implicit Type P : {group gT}.

Section GenericCores.

Variables H K : {group gT}.

Lemma sigmaJ x : \sigma(H :^ x) =i \sigma(H).

Lemma MsigmaJ x : (H :^ x)`_\sigma = H`_\sigma :^ x.

Lemma alphaJ x : \alpha(H :^ x) =i \alpha(H).

Lemma MalphaJ x : (H :^ x)`_\alpha = H`_\alpha :^ x.

Lemma betaJ x : \beta(H :^ x) =i \beta(H).

Lemma MbetaJ x : (H :^ x)`_\beta = H`_\beta :^ x.

End GenericCores.

This remark appears at the start (p. 70) of B & G, Section 10, just after the definition of ideal, which we do not include, since it is redundant with the notation p \in \beta(G) that is used later.
Remark not_narrow_ideal p P : p.-Sylow(G) P~~ p.-narrow Pp \in \beta(G).

Section MaxCores.

Variables M : {group gT}.
Hypothesis maxM : M \in 'M.

This is the first inclusion in the remark following the preliminary definitions in B & G, p. 70.
This is the first part of the remark just above B & G, Theorem 10.1.
Remark norm_sigma_Sylow p P :
  p \in \sigma(M)p.-Sylow(M) P'N(P) \subset M.

This is the second part of the remark just above B & G, Theorem 10.1.
Remark sigma_Sylow_G p P : p \in \sigma(M)p.-Sylow(M) Pp.-Sylow(G) P.

Lemma sigma_Sylow_neq1 p P : p \in \sigma(M)p.-Sylow(M) PP :!=: 1.

Lemma sigma_sub_pi : {subset \sigma(M) \pi(M)}.

Lemma predI_sigma_alpha : [predI \sigma(M) & \alpha(G)] =i \alpha(M).

Lemma predI_sigma_beta : [predI \sigma(M) & \beta(G)] =i \beta(M).

End MaxCores.

End CoreTheory.

Section Ten.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Type p : nat.
Implicit Type A E H K M N P Q R S V W X Y : {group gT}.

This is B & G, Theorem 10.1(d); note that we do not assume M is maximal.
Theorem sigma_Sylow_trans M p X g :
  p \in \sigma(M)p.-Sylow(M) XX :^ g \subset Mg \in M.

This is B & G, Theorem 10.1 (a, b, c). Part (e) of Theorem 10.1 is obviously stated incorrectly, and this is difficult to correct because it is not used in the rest of the proof.
Theorem sigma_group_trans M p X :
     M \in 'Mp \in \sigma(M)p.-group X
  [/\ (*a*) g, X \subset MX :^ g \subset M
            exists2 c, c \in 'C(X) & exists2 m, m \in M & g = c × m,
      (*b*) [transitive 'C(X), on [set Mg in M :^: G | X \subset Mg] | 'Js ]
    & (*c*) X \subset M'C(X) × 'N_M(X) = 'N(X)].

Section OneMaximal.

Variable M : {group gT}.
Hypothesis maxM : M \in 'M.

Let ltMG := mmax_proper maxM.
Let solM := mmax_sol maxM.

Let aMa : \alpha(M).-group (M`_\alpha).
Let nsMaM : M`_\alpha <| M.
Let sMaMs : M`_\alpha \subset M`_\sigma.

Let F := 'F(M / M`_\alpha).
Let nsFMa : F <| M / M`_\alpha.

Let alpha'F : \alpha(M)^'.-group F.

Let Malpha_quo_sub_Fitting : M^`(1) / M`_\alpha \subset F.

Let sigma_Hall_sub_der1 H : \sigma(M).-Hall(M) HH \subset M^`(1).

This is B & G, Theorem 10.2(a1).
This is B & G, Theorem 10.2(b1).
This is B & G, Theorem 10.2(b2).
This is B & G, Theorem 10.2(a2).
This is B & G, Theorem 10.2(c).
This is B & G, Theorem 10.2(d1).
This is B & G, Theorem 10.2(d2).
This is B & G, Theorem 10.2(e).
Theorem Msigma_neq1 : M`_\sigma :!=: 1.

This is B & G, Lemma 10.3.
Theorem cent_alpha'_uniq X :
     X \subset M\alpha(M)^'.-group X'r('C_(M`_\alpha)(X)) 2 →
  'C_M(X)%G \in 'U.

Variable p : nat.

This is B & G, Lemma 10.4(a). We omit the redundant assumption p \in \pi(M).
Lemma der1_quo_sigma' : p %| #|M / M^`(1)|p \in \sigma(M)^'.

Hypothesis s'p : p \in \sigma(M)^'.

This is B & G, Lemma 10.4(b). We do not need the assumption M`_\alpha != 1; the assumption p \in \pi(M) is restated as P != 1.
This is B & G, Lemma 10.4(c), part 1. The redundant assumption p \in \pi(M) is omitted.
This is B & G, Lemma 10.4(c), part 2 The redundant assumption p \in \pi(M) is omitted.
Lemma sigma'_rank2_beta' : 'r_p(M) = 2 → p \notin \beta(G).

This is B & G, Lemma 10.5, part 1; the condition on X has been weakened, because the proof of Lemma 12.2(a) requires the stronger result.
This is B & G, Lemma 10.5, part 2. We omit the second claim of B & G 10.5 as it is an immediate consequence of sigma'_rank2_beta' (i.e., 10.4(c)).
Lemma sigma'1Elem_sub_p2Elem X :
    X \in 'E_p^1(G)'N(X) \subset M
  exists2 A, A \in 'E_p^2(G) & X \subset A.

End OneMaximal.

This is B & G, Theorem 10.6.
Theorem mFT_proper_plength1 p H : H \proper Gp.-length_1 H.

Section OneSylow.

Variables (p : nat) (P : {group gT}).
Hypothesis sylP_G: p.-Sylow(G) P.
Let pP : p.-group P := pHall_pgroup sylP_G.

This is an B & G, Corollary 10.7(a), second part (which does not depend on a particular complement).
This is B & G, Corollary 10.7(a), first part.
Corollary mFT_Sylow_sdprod_commg V : P ><| V = 'N(P)[~: P, V] = P.

This is B & G, Corollary 10.7(b).
Corollary mFT_rank2_Sylow_cprod :
    'r(P) < 3 → ~~ abelian P
  exists2 S, [/\ ~~ abelian (gval S), logn p #|S| = 3 & exponent S %| p]
  & exists2 C, cyclic (gval C) & S \* C = P 'Ohm_1(C) = 'Z(S).

This is B & G, Corollary 10.7(c).
Corollary mFT_sub_Sylow_trans : Q x,
  Q \subset PQ :^ x \subset Pexists2 y, y \in 'N(P) & Q :^ x = Q :^ y.

This is B & G, Corollary 10.7(d).
This is B & G, Corollary 10.7(e).
This is B & G, Lemma 10.8(c).
Lemma beta_max_pdiv p :
    p \notin \beta(M)
  [/\ p^'.-Hall(M^`(1)) 'O_p^'(M^`(1)),
      p^'.-Hall(M`_\sigma) 'O_p^'(M`_\sigma)
    & q, q \in \pi(M / 'O_p^'(M))q p].

This is B & G, Lemma 10.8(a), first part.
Lemma Mbeta_Hall : \beta(M).-Hall(M) M`_\beta.

This is B & G, Lemma 10.8(a), second part.
Lemma Mbeta_Hall_G : \beta(M).-Hall(G) M`_\beta.

This is an equivalent form of B & G, Lemma 10.8(b), which is used directly later in the proof (e.g., Corollary 10.9a below, and Lemma 12.11), and is proved as an intermediate step of the proof of of 12.8(b).
Lemma Mbeta_quo_nil : nilpotent (M^`(1) / M`_\beta).

This is B & G, Lemma 10.8(b), generalized to arbitrary beta'-subgroups of M^`(1) (which includes Hall beta'-subgroups of M^`(1) and M`_\beta).
This is B & G, Corollary 10.9(a).
Corollary beta'_cent_Sylow p q X :
     p \notin \beta(M)q \notin \beta(M)q.-group X
     (p != q) && (X \subset M^`(1)) || (p < q) && (X \subset M)
  [/\ (*a1*) exists2 P, p.-Sylow(M`_\sigma) (gval P) & X \subset 'C(P),
      (*a2*) p \in \alpha(M)'C_M(X)%G \in 'U
    & (*a3*) q.-Sylow(M^`(1)) X
          exists2 P, p.-Sylow(M^`(1)) (gval P) & P \subset 'N_M(X)^`(1)].

This is B & G, Corollary 10.9(b).
Corollary nonuniq_norm_Sylow_pprod p H S :
    H \in 'MH :!=: Mp.-Sylow(G) S'N(S) \subset H :&: M
  M`_\beta × (H :&: M) = M \alpha(M) =i \beta(M).

This is B & G, Proposition 10.10.
Proposition max_normed_2Elem_signaliser p q (A Q : {group gT}) :
    p != qA \in 'E_p^2(G) :&: 'E×_p(G)Q \in |/|*(A; q)
    q %| #|'C(A)|
  exists2 P : {group gT}, p.-Sylow(G) P A \subset P
          & [/\ (*a*) 'O_p^'('C(P)) × ('N(P) :&: 'N(Q)) = 'N(P),
                (*b*) P \subset 'N(Q)^`(1)
              & (*c*) q.-narrow QP \subset 'C(Q)].

Notation for Proposition 11, which is the last to appear in this segment.
Local Notation sigma' := \sigma(gval M)^'.

This is B & G, Proposition 10.11(a).
Proposition sigma'_not_uniq K : K \subset Msigma'.-group KK \notin 'U.

This is B & G, Proposition 10.11(b).
This is B & G, Proposition 10.11(c).
This is B & G, Proposition 10.11(d).
Proposition commG_sigma'_1Elem_cyclic p K P (K0 := [~: K, P]) :
    K \subset Msigma'.-group Kp \in sigma'P \in 'E_p^1('N_M(K))
    'C_(M`_\sigma)(P) = 1 → p^'.-group Kabelian K
  [/\ K0 \subset 'C(M`_\sigma), cyclic K0 & K0 <| M].

End AnotherMaximal.

This is B & G, Lemma 10.12.
Lemma sigma_disjoint M H :
    M \in 'MH \in 'Mgval H \notin M :^: G
  [/\ (*a*) M`_\alpha :&: H`_\sigma = 1,
            [predI \alpha(M) & \sigma(H)] =i pred0
    & (*b*) nilpotent M`_\sigma
            M`_\sigma :&: H`_\sigma = 1
          [predI \sigma(M) & \sigma(H)] =i pred0].

This is B & G, Lemma 10.13.
Lemma basic_p2maxElem_structure p A P :
    A \in 'E_p^2(G) :&: 'E×_p(G)p.-group PA \subset P~~ abelian P
  let Z0 := ('Ohm_1('Z(P)))%G in
  [/\ (*a*) Z0 \in 'E_p^1(A),
      (*b*) Y : {group gT},
            [/\ cyclic Y, Z0 \subset Y
              & A0, A0 \in 'E_p^1(A) :\ Z0A0 \x Y = 'C_P(A)]
    & (*c*) [transitive 'N_P(A), on 'E_p^1(A) :\ Z0| 'JG]].

This is B & G, Proposition 10.14(a).
Proposition beta_not_narrow p : p \in \beta(G)
      [disjoint 'E_p^2(G) & 'E×_p(G)]
   ( P, p.-Sylow(G) P[disjoint 'E_p^2(P) & 'E×_p(P)]).

This is B & G, Proposition 10.14(b).
Proposition beta_noncyclic_uniq p R :
  p \in \beta(G)p.-group R'r(R) > 1 → R \in 'U.

This is B & G, Proposition 10.14(c).
Proposition beta_subnorm_uniq p P X :
  p \in \beta(G)p.-Sylow(G) PX \subset P'N_P(X)%G \in 'U.

This is B & G, Proposition 10.14(d).
Proposition beta_norm_sub_mmax M Y :
  M \in 'M\beta(M).-subgroup(M) YY :!=: 1 → 'N(Y) \subset M.

End Ten.