(Joint Center)Library BGsection12

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

This file covers B & G, section 12; it defines the prime sets for the complements of M`_\sigma in a maximal group M: \tau1(M) == the set of p not in \pi(M^`(1)) (thus not in \sigma(M)), such that M has p-rank 1. \tau2(M) == the set of p not in \sigma(M), such that M has p-rank 2. \tau3(M) == the set of p not in \sigma(M), but in \pi(M^`(1)), such that M has p-rank 1. We also define the following helper predicate, which encapsulates the notation conventions defined at the beginning of B & G, Section 12: sigma_complement M E E1 E2 E3 <=> E is a Hall \sigma(M)^'-subgroup of M, the Ei are Hall \tau_i(M)-subgroups of E, and E2 * E1 is a group.

Set Implicit Arguments.

Import GroupScope.
Section Definitions.

Variables (gT : finGroupType) (M : {set gT}).
Local Notation sigma' := \sigma(M)^'.

Definition tau1 := [pred p in sigma' | 'r_p(M) == 1%N & ~~ (p %| #|M^`(1)|)].
Definition tau2 := [pred p in sigma' | 'r_p(M) == 2].
Definition tau3 := [pred p in sigma' | 'r_p(M) == 1%N & p %| #|M^`(1)|].

Definition sigma_complement E E1 E2 E3 :=
  [/\ sigma'.-Hall(M) E, tau1.-Hall(E) E1, tau2.-Hall(E) E2, tau3.-Hall(E) E3
    & group_set (E2 × E1)].

End Definitions.

Notation "\tau1 ( M )" := (tau1 M)
  (at level 2, format "\tau1 ( M )") : group_scope.
Notation "\tau2 ( M )" := (tau2 M)
  (at level 2, format "\tau2 ( M )") : group_scope.
Notation "\tau3 ( M )" := (tau3 M)
  (at level 2, format "\tau3 ( M )") : group_scope.

Section Section12.

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

Section Introduction.

Variables M E : {group gT}.
Hypotheses (maxM : M \in 'M) (hallE : \sigma(M)^'.-Hall(M) E).

Lemma tau1J x : \tau1(M :^ x) =i \tau1(M).

Lemma tau2J x : \tau2(M :^ x) =i \tau2(M).

Lemma tau3J x : \tau3(M :^ x) =i \tau3(M).

Lemma tau2'1 : {subset \tau1(M) \tau2(M)^'}.

Lemma tau3'1 : {subset \tau1(M) \tau3(M)^'}.

Lemma tau3'2 : {subset \tau2(M) \tau3(M)^'}.

Lemma ex_sigma_compl : F : {group gT}, \sigma(M)^'.-Hall(M) F.

Let s'E : \sigma(M)^'.-group E := pHall_pgroup hallE.
Let sEM : E \subset M := pHall_sub hallE.

For added convenience, this lemma does NOT depend on the maxM assumption.
The preliminary remarks in the introduction of B & G, section 12.

Remark der1_sigma_compl : M^`(1) :&: E = E^`(1).

Remark partition_pi_mmax p :
  (p \in \pi(M)) =
     [|| p \in \tau1(M), p \in \tau2(M), p \in \tau3(M) | p \in \sigma(M)].

Remark partition_pi_sigma_compl p :
  (p \in \pi(E)) = [|| p \in \tau1(M), p \in \tau2(M) | p \in \tau3(M)].

Remark tau2E p : (p \in \tau2(M)) = (p \in \pi(E)) && ('r_p(E) == 2).

Remark tau3E p : (p \in \tau3(M)) = (p \in \pi(E^`(1))) && ('r_p(E) == 1%N).

Remark tau1E p :
  (p \in \tau1(M)) = [&& p \in \pi(E), p \notin \pi(E^`(1)) & 'r_p(E) == 1%N].

Generate a rank 2 elementary abelian tau2 subgroup in a given complement.
Lemma ex_tau2Elem p :
  p \in \tau2(M)exists2 A, A \in 'E_p^2(E) & A \in 'E_p^2(M).

A converse to the above Lemma: if E has an elementary abelian subgroup of order p^2, then p must be in tau2.
Lemma sigma'2Elem_tau2 p A : A \in 'E_p^2(E)p \in \tau2(M).

This is B & G, Lemma 12.1(a).
This is B & G, Lemma 12.1(g).
Lemma tau2_not_beta p :
  p \in \tau2(M)p \notin \beta(G) {subset 'E_p^2(M) 'E×_p(G)}.

End Introduction.

Implicit Arguments tau2'1 [[M] x].
Implicit Arguments tau3'1 [[M] x].
Implicit Arguments tau3'2 [[M] x].

This is the rest of B & G, Lemma 12.1 (parts b, c, d,e, and f).
Lemma sigma_compl_context M E E1 E2 E3 :
    M \in 'Msigma_complement M E E1 E2 E3
  [/\ (*b*) E3 \subset E^`(1) E3 <| E,
      (*c*) E2 :==: 1 → E1 :!=: 1,
      (*d*) cyclic E1 cyclic E3,
      (*e*) E3 ><| (E2 ><| E1) = E E3 ><| E2 ><| E1 = E
    & (*f*) 'C_E3(E) = 1].

This is B & G, Lemma 12.2(a).
Lemma prime_class_mmax_norm M p X :
     M \in 'Mp.-group X'N(X) \subset M
  (p \in \sigma(M)) || (p \in \tau2(M)).

This is B & G, Lemma 12.2(b).
Lemma mmax_norm_notJ M Mstar p X :
    M \in 'MMstar \in 'M
    p.-group XX \subset M'N(X) \subset Mstar
    [|| [&& p \in \sigma(M) & M :!=: Mstar], p \in \tau1(M) | p \in \tau3(M)]
  gval Mstar \notin M :^: G.

This is B & G, Lemma 12.3.
Lemma nonuniq_p2Elem_cent_sigma M Mstar p A A0 :
    M \in 'MMstar \in 'MMstar :!=: MA \in 'E_p^2(M)
    A0 \in 'E_p^1(A)'N(A0) \subset Mstar
 [/\ (*a*) p \notin \sigma(M)A \subset 'C(M`_\sigma :&: Mstar)
   & (*b*) p \notin \alpha(M)A \subset 'C(M`_\alpha :&: Mstar)].

This is B & G, Proposition 12.4.
Proposition p2Elem_mmax M p A :
      M \in 'MA \in 'E_p^2(M)
    (*a*) 'C(A) \subset M
  (*b*) ([ A0 in 'E_p^1(A), 'M('N(A0)) != [set M]]
           [/\ p \in \sigma(M), M`_\alpha = 1 & nilpotent M`_\sigma]).

This is B & G, Theorem 12.5(a) -- this part does not mention a specific rank 2 elementary abelian \tau_2(M) subgroup of M.

Theorem tau2_Msigma_nil M p : M \in 'Mp \in \tau2(M)nilpotent M`_\sigma.

This is B & G, Theorem 12.5 (b-f) -- the bulk of the Theorem.
Theorem tau2_context M p A (Ms := M`_\sigma) :
    M \in 'Mp \in \tau2(M)A \in 'E_p^2(M)
  [/\ (*b*) P, p.-Sylow(M) P
                abelian P
              (A \subset P'Ohm_1(P) = A ~~ ('N(P) \subset M)),
      (*c*) Ms <*> A <| M,
      (*d*) 'C_Ms(A) = 1,
      (*e*) Mstar, Mstar \in 'M(A) :\ MMs :&: Mstar = 1
    & (*f*) exists2 A1, A1 \in 'E_p^1(A) & 'C_Ms(A1) = 1].

This is B & G, Corollary 12.6 (a, b, c & f) -- i.e., the assertions that do not depend on the decomposition of the complement.
Corollary tau2_compl_context M E p A (Ms := M`_\sigma) :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
  [/\ (*a*) A <| E 'E_p^1(E) = 'E_p^1(A),
      (*b*) [/\ 'C(A) \subset E, 'N_M(A) = E & ~~ ('N(A) \subset M)],
      (*c*) X, X \in 'E_p^1(E)'C_Ms(X) != 1 → 'M('C(X)) = [set M]
    & (*f*) Mstar,
              Mstar \in 'Mgval Mstar \notin M :^: G
            Ms :&: Mstar`_\sigma = 1
          [predI \sigma(M) & \sigma(Mstar)] =i pred0].

This is B & G, Corollary 12.6 (d, e) -- the parts that apply to a particular decomposition of the complement. We included an easy consequece of part (a), that A is a subgroup of E2, as this is used implicitly later in sections 12 and 13.
Corollary tau2_regular M E E1 E2 E3 p A (Ms := M`_\sigma) :
    M \in 'Msigma_complement M E E1 E2 E3
    p \in \tau2(M)A \in 'E_p^2(E)
  [/\ (*d*) semiregular Ms E3,
      (*e*) semiregular Ms 'C_E1(A)
          & A \subset E2].

This is B & G, Theorem 12.7.
Theorem nonabelian_tau2 M E p A P0 (Ms := M`_\sigma) (A0 := 'C_A(Ms)%G) :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
    p.-group P0~~ abelian P0
 [/\ (*a*) \tau2(M) =i (p : nat_pred),
     (*b*) #|A0| = p Ms \x A0 = 'F(M),
     (*c*) X,
             X \in 'E_p^1(E) :\ A0'C_Ms(X) = 1 ~~ ('C(X) \subset M)
   & (*d*) exists2 E0 : {group gT}, A0 ><| E0 = E
   & (*e*) x, x \in Ms^#{subset \pi('C_E0[x]) \tau1(M)}].

This is B & G, Theorem 12.8(c). This part does not use the decompotision of the complement, and needs to be proved ahead because it is used with different primes in \tau_2(M) in the main argument. We also include an auxiliary identity, which is needed in another part of the proof of 12.8.
Theorem abelian_tau2_sub_Fitting M E p A S :
    M \in 'M\sigma(M)^'.-Hall(M) E
    p \in \tau2(M)A \in 'E_p^2(E)
    p.-Sylow(G) SA \subset Sabelian S
  [/\ S \subset 'N(S)^`(1),
    'N(S)^`(1) \subset 'F(E),
         'F(E) \subset 'C(S),
         'C(S) \subset E
   & 'F('N(A)) = 'F(E)].

This is B & G, Theorem 12.8(a,b,d,e) -- the bulk of the Theorem. We prove part (f) separately below, as it does not depend on a decomposition of the complement.
Theorem abelian_tau2 M E E1 E2 E3 p A S (Ms := M`_\sigma) :
    M \in 'Msigma_complement M E E1 E2 E3
    p \in \tau2(M)A \in 'E_p^2(E)
    p.-Sylow(G) SA \subset Sabelian S
  [/\ (*a*) E2 <| E abelian E2,
      (*b*) \tau2(M).-Hall(G) E2,
      (*d*) [/\ 'N(A) = 'N(S),
                      'N(S) = 'N(E2),
                     'N(E2) = 'N(E3 <*> E2)
            & 'N(E3 <*> E2) = 'N('F(E))]
    & (*e*) X, X \in 'E^1(E1)'C_Ms(X) = 1 → X \subset 'Z(E)].

This is B & G, Theorem 12.8(f).
Theorem abelian_tau2_norm_Sylow M E p A S :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
    p.-Sylow(G) SA \subset Sabelian S
   X, X \subset 'N(S)'C_S(X) <| 'N(S) [~: S, X] <| 'N(S).

This is B & G, Corollary 12.9.
Corollary tau1_act_tau2 M E p A q Q (Ms := M`_\sigma) :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
    q \in \tau1(M)Q \in 'E_q^1(E)'C_Ms(Q) = 1 → [~: A, Q] != 1 →
 let A0 := [~: A, Q]%G in let A1 := ('C_A(Q))%G in
 [/\ (*a*) [/\ A0 \in 'E_p^1(A), 'C_A(Ms) = A0 & A0 <| M],
     (*b*) gval A0 \notin A1 :^: G
   & (*c*) A1 \in 'E_p^1(A) ~~ ('C(A1) \subset M)].

This is B & G, Corollary 12.10(a).
Corollary sigma'_nil_abelian M N :
  M \in 'MN \subset M\sigma(M)^'.-group Nnilpotent Nabelian N.

This is B & G, Corollary 12.10(b), first assertion.
Corollary der_mmax_compl_abelian M E :
  M \in 'M\sigma(M)^'.-Hall(M) Eabelian E^`(1).

This is B & G, Corollary 12.10(b), second assertion. Note that we do not require the full decomposition of the complement.
Corollary tau2_compl_abelian M E E2 :
   M \in 'M\sigma(M)^'.-Hall(M) E\tau2(M).-Hall(E) E2abelian E2.

This is B & G, Corollary 12.10(c). We do not really need a full decomposition of the complement in the first part, but this reduces the number of assumptions.
Corollary tau1_cent_tau2Elem_factor M E p A :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
  [/\ E1 E2 E3, sigma_complement M E E1 E2 E3E3 × E2 \subset 'C_E(A),
      'C_E(A) <| E
    & \tau1(M).-group (E / 'C_E(A))].

This is B & G, Corollary 12.10(d).
Corollary norm_noncyclic_sigma M p P :
    M \in 'Mp \in \sigma(M)p.-group PP \subset M~~ cyclic P
  'N(P) \subset M.

This is B & G, Corollary 12.10(e).
Corollary cent1_nreg_sigma_uniq M (Ms := M`_\sigma) x :
    M \in 'Mx \in M^#\tau2(M).-elt x'C_Ms[x] != 1 →
 'M('C[x]) = [set M].

This is B & G, Lemma 12.11.
Lemma primes_norm_tau2Elem M E p A Mstar :
    M \in 'M\sigma(M)^'.-Hall(M) Ep \in \tau2(M)A \in 'E_p^2(E)
    Mstar \in 'M('N(A))
 [/\ (*a*) {subset \tau2(M) [predD \sigma(Mstar) & \beta(Mstar)]},
     (*b*) [predU \tau1(Mstar) & \tau2(Mstar)].-group (E / 'C_E(A))
   & (*c*) q, q \in \pi(E / 'C_E(A))q \in \pi('C_E(A))
           [/\ q \in \tau2(Mstar),
               exists2 P, P \in 'Syl_p(G) & P <| Mstar
             & Q, [/\ Q \in 'Syl_q(G), Q \subset Mstar & abelian Q]]].

This is a generalization of B & G, Theorem 12.12. In the B & G text, Theorem 12.12 only establishes the type F structure for groups of type I, whereas it is required for the derived groups of groups of type II (in the sense of Peterfalvi). Indeed this is exactly what is stated in Lemma 15.15(e) and then Theorem B(3). The proof of 15.15(c) cites 12.12 in the type I case (K = 1) and then loosely invokes a "short and easy argument" inside the proof of 12.12 for the K != 1 case. In fact, this involves copying roughly 25% of the proof, whereas the proof remains essentially unchanged when Theorem 12.12 is generalized to a normal Hall subgroup of E as below. Also, we simplify the argument for central tau2 Sylow subgroup S of U by by replacing the considerations on the abelian structure of S by a comparison of Mho^n-1(S) and Ohm_1(S) (with exponent S = p ^ n), as the former is needed anyway to prove regularity when S is not homocyclic.
Theorem FTtypeF_complement M (Ms := M`_\sigma) E U :
    M \in 'M\sigma(M)^'.-Hall(M) EHall E UU <| EU :!=: 1 →
  {in U^#, e, [predU \tau1(M) & \tau3(M)].-elt e'C_Ms[e] = 1}
  [/\ (*a*) A0 : {group gT},
             [/\ A0 <| U, abelian A0 & {in Ms^#, x, 'C_U[x] \subset A0}]
    & (*b*) E0 : {group gT},
             [/\ E0 \subset U, exponent E0 = exponent U
               & [Frobenius Ms <*> E0 = Ms ><| E0]]].

This is B & G, Theorem 12.13.
Theorem nonabelian_Uniqueness p P : p.-group P~~ abelian PP \in 'U.

This is B & G, Corollary 12.14. We have removed the redundant assumption p \in \sigma(M), and restricted the quantification over P to the part of the conclusion where it is mentioned. Usage note: it might be more convenient to state that P is a Sylow subgroup of M rather than M`_\sigma; check later use.
Corollary cent_der_sigma_uniq M p X (Ms := M`_\sigma) :
    M \in 'MX \in 'E_p^1(M)(p \in \beta(M)) || (X \subset Ms^`(1))
  'M('C(X)) = [set M] ( P, p.-Sylow(Ms) P'M(P) = [set M]).

This is B & G, Proposition 12.15.
Proposition sigma_subgroup_embedding M q X Mstar :
    M \in 'Mq \in \sigma(M)X \subset Mq.-group XX :!=: 1 →
    Mstar \in 'M('N(X)) :\ M
 [/\ (*a*) gval Mstar \notin M :^: G,
            S, q.-Sylow(M :&: Mstar) SX \subset S
       (*b*) 'N(S) \subset M
     (*c*) q.-Sylow(Mstar) S
    & if q \in \sigma(Mstar)
     (*d*) then
     [/\ (*1*) Mstar`_\beta × (M :&: Mstar) = Mstar,
         (*2*) {subset \tau1(Mstar) [predU \tau1(M) & \alpha(M)]}
       & (*3*) M`_\beta = M`_\alpha M`_\alpha != 1]
     (*e*) else
     [/\ (*1*) q \in \tau2(Mstar),
         (*2*) {subset [predI \pi(M) & \sigma(Mstar)] \beta(Mstar)}
       & (*3*) \sigma(Mstar)^'.-Hall(Mstar) (M :&: Mstar)]].

This is B & G, Corollary 12.16.
Corollary sigma_Jsub M Y :
    M \in 'M\sigma(M).-group YY :!=: 1 →
  [/\ x, Y :^ x \subset M`_\sigma
    & E p H,
        \sigma(M)^'.-Hall(M) Ep \in \pi(E)p \notin \beta(G)
        H \in 'M(Y)gval H \notin M :^: G
    [/\ (*a*) 'r_p('N_H(Y)) 1
      & (*b*) p \in \tau1(M)p \notin \pi(('N_H(Y))^`(1))]].

This is B & G, Lemma 12.17.
Lemma sigma_compl_embedding M E (Ms := M`_\sigma) :
    M \in 'M\sigma(M)^'.-Hall(M) E
 [/\ 'C_Ms(E) \subset Ms^`(1), [~: Ms, E] = Ms
   & g (MsMg := Ms :&: M :^ g), g \notin M
     [/\ cyclic MsMg, \beta(M)^'.-group MsMg & MsMg :&: Ms^`(1) = 1]].

This is B & G, Lemma 12.18. We corrected an omission in the text, which fails to quote Lemma 10.3 to justify the two p-rank inequalities (12.5) and (12.6), and indeed erroneously refers to 12.2(a) for (12.5). Note also that the loosely justified equalities of Ohm_1 subgroups are in fact unnecessary.
Lemma cent_Malpha_reg_tau1 M p q P Q (Ma := M`_\alpha) :
    M \in 'Mp \in \tau1(M)q \in p^'P \in 'E_p^1(M)Q :!=: 1 →
    P \subset 'N(Q)'C_Q(P) = 1 → 'M('N(Q)) != [set M]
  [/\ (*a*) Ma != 1 → q \notin \alpha(M)q.-group QQ \subset M
            'C_Ma(P) != 1 'C_Ma(Q <*> P) = 1
    & (*b*) q.-Sylow(M) Q
            [/\ \alpha(M) =i \beta(M), Ma != 1, q \notin \alpha(M),
                'C_Ma(P) != 1 & 'C_Ma(Q <*> P) = 1]].

This is B & G, Lemma 12.19. We have used lemmas 10.8(b) and 10.2(c) rather than 10.9(a) as suggested in the text; this avoids a quantifier inversion!
Lemma der_compl_cent_beta' M E :
    M \in 'M\sigma(M)^'.-Hall(M) E
  exists2 H : {group gT}, \beta(M)^'.-Hall(M`_\sigma) H & E^`(1) \subset 'C(H).

End Section12.

Implicit Arguments tau2'1 [[gT] [M] x].
Implicit Arguments tau3'1 [[gT] [M] x].
Implicit Arguments tau3'2 [[gT] [M] x].