(Joint Center)Library BGsection4

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
Require Import fintype finfun bigop ssralg finset prime binomial.
Require Import fingroup morphism automorphism perm quotient action gproduct.
Require Import gfunctor commutator zmodp cyclic center pgroup gseries nilpotent.
Require Import sylow abelian maximal extremal hall.
Require Import matrix mxalgebra mxrepresentation mxabelem.
Require Import BGsection1 BGsection2.

This file covers B & G, Section 4, i.e., the proof of structure theorems for solvable groups with a small (of rank at most 2) Fitting subgroup.

Set Implicit Arguments.

Import GroupScope.

Section Section4.

Implicit Type gT : finGroupType.
Implicit Type p : nat.

B & G, Lemma 4.1 (also, Gorenstein, 1.3.4, and Aschbacher, ex. 2.4) is covered by Lemma center_cyclic_abelian, in center.v.
B & G, Lemma 4.2 is covered by Lemmas commXg, commgX, commXXg (for 4.2(a)) and expMg_Rmul (for 4.2(b)) in commutators.v.
This is B & G, Proposition 4.3.
Proposition exponent_odd_nil23 gT (R : {group gT}) p :
   p.-group Rodd #|R|nil_class R 2 + (p > 3)
 [/\ (*a*) exponent 'Ohm_1(R) %| p
   & (*b*) R^`(1) \subset 'Ohm_1(R)
           {in R &, {morph expgn^~ p : x y / x × y}}].

Part (a) of B & G, Proposition 4.4 is covered in file maximal.v by lemmas max_SCN and SCN_max.
This is B & G, Proposition 4.4(b), or Gorenstein 7.6.5.
Proposition SCN_Sylow_cent_dprod gT (R G A : {group gT}) p :
  p.-Sylow(G) RA \in 'SCN(R)'O_p^'('C_G(A)) \x A = 'C_G(A).

This is B & G, Lemma 4.5(b), or Gorenstein, 5.4.4 and 5.5.5.
Lemma Ohm1_extremal_odd gT (R : {group gT}) p x :
    p.-group Rodd #|R|~~ cyclic Rx \in R#|R : <[x]>| = p
  ('Ohm_1(R))%G \in 'E_p^2(R).

Section OddNonCyclic.

Variables (gT : finGroupType) (p : nat) (R : {group gT}).
Hypotheses (pR : p.-group R) (oddR : odd #|R|) (ncycR : ~~ cyclic R).

This is B & G, Lemma 4.5(a), or Gorenstein 5.4.10.
This is B & G, Lemma 4.5(c).
Some "obvious" consequences of the above, which are used casually and pervasively throughout B & G.
Definition odd_pgroup_rank1_cyclic := odd_pgroup_rank1_cyclic. (* in extremal *)

Lemma odd_rank1_Zgroup gT (G : {group gT}) :
  odd #|G|Zgroup G = ('r(G) 1).

This is B & G, Proposition 4.6 (a stronger version of Lemma 4.5(a)).
Proposition odd_normal_p2Elem_exists gT p (R S : {group gT}) :
    p.-group Rodd #|R|S <| R~~ cyclic S
   E : {group gT}, [/\ E \subset S, E <| R & E \in 'E_p^2(R)].

This is B & G, Lemma 4.7, and (except for the trivial converse) Gorenstein 5.4.15 and Aschbacher 23.17.
Lemma rank2_SCN3_empty gT p (R : {group gT}) :
  p.-group Rodd #|R|('r(R) 2) = ('SCN_3(R) == set0).

This is B & G, Proposition 4.8(a).
Proposition rank2_exponent_p_p3group gT (R : {group gT}) p :
  p.-group Rrank R 2 → exponent R %| plogn p #|R| 3.

This is B & G, Proposition 4.8(b).
Proposition exponent_Ohm1_rank2 gT p (R : {group gT}) :
  p.-group R'r(R) 2 → p > 3 → exponent 'Ohm_1(R) %| p.

This is B & G, Lemma 4.9.
Lemma quotient_p2_Ohm1 gT p (R : {group gT}) :
    p.-group Rp > 3 → logn p #|'Ohm_1(R)| 2 →
   T : {group gT}, T <| Rlogn p #|'Ohm_1(R / T)| 2.

This is B & G, Lemma 4.10.
Lemma Ohm1_metacyclic_p2Elem gT p (R : {group gT}) :
    metacyclic Rp.-group Rodd #|R|~~ cyclic R
  'Ohm_1(R)%G \in 'E_p^2(R).

This is B & G, Proposition 4.11 (due to Huppert).
Proposition p2_Ohm1_metacyclic gT p (R : {group gT}) :
  p.-group Rp > 3 → logn p #|'Ohm_1(R)| 2 → metacyclic R.

This is B & G, Theorem 4.12 (also due to Huppert), for internal action.
Theorem coprime_metacyclic_cent_sdprod gT p (R A : {group gT}) :
    p.-group Rodd #|R|metacyclic Rp^'.-group AA \subset 'N(R)
    let T := [~: R, A] in let C := 'C_R(A) in
  [/\ (*a*) abelian T,
      (*b*) T ><| C = R
    & (*c*) ~~ abelian RT != 1 →
            [/\ C != 1, cyclic T, cyclic C & R^`(1) \subset T]].

This covers B & G, Lemmas 4.13 and 4.14.
Lemma pi_Aut_rank2_pgroup gT p q (R : {group gT}) :
    p.-group Rodd #|R|'r(R) 2 → q \in \pi(Aut R)q != p
  [/\ q %| (p ^ 2).-1, q < p & q %| p.+1./2 q %| p.-1./2].

B & G, Lemma 4.15 is covered by maximal/critical_extraspecial.
This is B & G, Theorem 4.16 (due to Blackburn).
Theorem rank2_coprime_comm_cprod gT p (R A : {group gT}) :
    p.-group Rodd #|R|R :!=: 1 → 'r(R) 2 →
    [~: R, A] = Rp^'.-group Aodd #|A|
  [/\ p > 3
    & [\/ abelian R
        | exists2 S : {group gT},
             [/\ ~~ abelian S, logn p #|S| = 3 & exponent S %| p]
        & C : {group gT},
             [/\ S \* C = R, cyclic C & 'Ohm_1(C) = S^`(1)]]].

This is B & G, Theorem 4.17.
Theorem der1_Aut_rank2_pgroup gT p (R : {group gT}) (A : {group {perm gT}}) :
    p.-group Rodd #|R|'r(R) 2 →
    A \subset Aut Rsolvable Aodd #|A|
  p.-group A^`(1).

This is B & G, Theorem 4.18(a).
Theorem rank2_max_pdiv gT p q (G : {group gT}) :
  solvable Godd #|G|'r_p(G) 2 → q \in \pi(G / 'O_p^'(G))q p.

This is B & G, Theorem 4.18(c,e)
Theorem rank2_der1_complement gT p (G : {group gT}) :
    solvable Godd #|G|'r_p(G) 2 →
  [/\ (*c*) p^'.-Hall(G^`(1)) 'O_p^'(G^`(1)),
     (*e1*) abelian (G / 'O_{p^',p}(G))
   & (*e2*) p^'.-group (G / 'O_{p^',p}(G))].

This is B & G, Theorem 4.18(b)
Theorem rank2_min_p_complement gT (G : {group gT}) (p := pdiv #|G|) :
  solvable Godd #|G|'r_p(G) 2 → p^'.-Hall(G) 'O_p^'(G).

This is B & G, Theorem 4.18(d)
Theorem rank2_sub_p'core_der1 gT (G A : {group gT}) p :
    solvable Godd #|G|'r_p(G) 2 → p^'.-subgroup(G^`(1)) A
  A \subset 'O_p^'(G^`(1)).

This is B & G, Corollary 4.19
Corollary rank2_der1_cent_chief gT p (G Gs U V : {group gT}) :
    odd #|G|solvable GGs <| G'r_p(Gs) 2 →
    chief_factor G V Up.-group (U / V) → U \subset Gs
  G^`(1) \subset 'C(U / V | 'Q).

This is B & G, Theorem 4.20(a)
Theorem rank2_der1_sub_Fitting gT (G : {group gT}) :
  odd #|G|solvable G'r('F(G)) 2 → G^`(1) \subset 'F(G).

This is B & G, Theorem 4.20(b)
Theorem rank2_char_Sylow_normal gT (G S T : {group gT}) :
    odd #|G|solvable G'r('F(G)) 2 →
  Sylow G ST \char ST \subset S^`(1)T <| G.

This is B & G, Theorem 4.20(c), for the last factor of the series.
Theorem rank2_min_p'core_Hall gT (G : {group gT}) (p := pdiv #|G|) :
  odd #|G|solvable G'r('F(G)) 2 → p^'.-Hall(G) 'O_p^'(G).

This is B & G, Theorem 4.20(c), for intermediate factors.
Theorem rank2_ge_pcore_Hall gT m (G : {group gT}) (pi := [pred p | p m]) :
  odd #|G|solvable G'r('F(G)) 2 → pi.-Hall(G) 'O_pi(G).

This is B & G, Theorem 4.20(c), for the first factor of the series.
Theorem rank2_max_pcore_Sylow gT (G : {group gT}) (p := max_pdiv #|G|) :
  odd #|G|solvable G'r('F(G)) 2 → p.-Sylow(G) 'O_p(G).

End Section4.