# Library BGsection5

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

This file covers Section 5 of B & G, except for some technical results that are not actually used in the proof of the Odd Order Theorem, namely part (c) of Theorem 5.5, parts (b), (d) and (e) of Theorem 5.5, and all of Theorem 5.7. We also make the following change: in B & G, narrow p-groups of rank at least 3 are defined by the structure of the centralisers of their prime subgroups, then characterized by their rank 2 elementary abelian subgroups in Theorem 5.3. We exchange the two, because the latter condition is easier to check, and is the only one used later in the proof.
p.-narrow G == G has a maximal elementary abelian p-subgroup of p-rank at most 2. := ('r_p(G) > 2) ==> ('E_p^2(G) :&: 'E*_p(G) != set0)
narrow_structure p G <-> G has a subgroup S of order p whose centraliser is the direct product of S and a cyclic group C, i.e., S \x C = 'C_G(S). This is the condition used in the definition of "narrow" in B & G, p. 2. Theorem 5.3 states that for odd p this definition is equivalent to ours, and this property is not used outside of Section 5.

Set Implicit Arguments.

Import GroupScope.

Reserved Notation "p .-narrow" (at level 2, format "p .-narrow").

Section Definitions.

Variables (gT : finGroupType) (p : nat) (A : {set gT}).

Definition narrow := ('r_p(A) > 2) ==> ('E_p^2(A) :&: 'E×_p(A) != set0).

Inductive narrow_structure : Prop :=
NarrowStructure (S C : {group gT}) of
S \subset A & C \subset A & #|S| = p & cyclic C & S \x C = 'C_A(S).

End Definitions.

Notation "p .-narrow" := (narrow p) : group_scope.

Section IsoDef.

Variables (gT rT : finGroupType) (p : nat).
Implicit Types G H : {group gT}.
Implicit Type R : {group rT}.

Lemma injm_narrow G H (f : {morphism G >-> rT}) :
'injm fH \subset Gp.-narrow (f @* H) = p.-narrow H.

Lemma isog_narrow G R : G \isog Rp.-narrow G = p.-narrow R.

No isomorphism theorems for narrow_structure, which is not used outside of this file.

End IsoDef.

Section Five.

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

Section OneGroup.

Variables (gT : finGroupType) (p : nat) (R : {group gT}).
Implicit Types B E S : {group gT}.

Lemma narrowJ x : p.-narrow (R :^ x) = p.-narrow R.

Hypotheses (pR : p.-group R) (oddR : odd #|R|).

Section Rank3.

Hypothesis rR : 2 < 'r_p(R).

This lemma uses only the rR hypothesis.
Lemma narrow_pmaxElem : p.-narrow R E, E \in 'E_p^2(R) :&: 'E×_p(R).

Let ntR : R :!=: 1.
Let p_pr : prime p.
Let p_gt1 : p > 1.

This is B & G, Lemma 5.1(a).
Lemma rank3_SCN3 : B, B \in 'SCN_3(R).

This is B & G, Lemma 5.1(b).
Lemma normal_p2Elem_SCN3 E :
E \in 'E_p^2(R)E <| Rexists2 B, B \in 'SCN_3(R) & E \subset B.

Let Z := 'Ohm_1('Z(R)).
Let W := 'Ohm_1('Z_2(R)).
Let T := 'C_R(W).

Let ntZ : Z != 1.

Let sZR : Z \subset R.

Let abelZ : p.-abelem (Z).

Let pZ : p.-group Z.

Let defCRZ : 'C_R(Z) = R.

Let sWR : W \subset R.

Let nWR : R \subset 'N(W).

This is B & G, Lemma 5.2.
Lemma Ohm1_ucn_p2maxElem E :
E \in 'E_p^2(R) :&: 'E×_p(R)
[/\ (*a*) ~~ (E \subset T),
(*b*) #|Z| = p [group of W] \in 'E_p^2(R)
& (*c*) T \char R #|R : T| = p ].

This is B & G, Theorem 5.3(d); we omit parts (a)-(c) as they are mostly redundant with Lemma 5.2, given our definition of "narrow".
This is B & G, Corollary 5.4. Given our definition of narrow, this is used directly in the proof of the main part of Theorem 5.3.
This is the main statement of B & G, Theorem 5.3, stating the equivalence of the structural and rank characterizations of the "narrow" property. Due to our definition of "narrow", the equivalence is the converse of that in B & G (we define narrow in terms of maximal elementary abelian subgroups).
This is B & G, Theoren 5.5 (a) and (b). Part (c), which is not used in the proof of the Odd Order Theorem, is omitted.
Theorem Aut_narrow (A : {group {perm gT}}) :
p.-narrow Rsolvable AA \subset Aut Rodd #|A|
[/\ (*a*) p^'.-group (A / 'O_p(A)), abelian (A / 'O_p(A))
& (*b*) 2 < 'r(R) x, x \in Ap^'.-elt x#[x] %| p.-1].

End OneGroup.

This is B & G, Theorem 5.6, parts (a) and (c). We do not prove parts (b), (d) and (e), as they are not used in the proof of the Odd Order Theorem.
Theorem narrow_der1_complement_max_pdiv gT p (G S : {group gT}) :
odd #|G|solvable Gp.-Sylow(G) Sp.-narrow S
(2 < 'r(S)) ==> p.-length_1 G
[/\ (*a*) p^'.-Hall(G^(1)) 'O_p^'(G^(1))
& (*c*) q, q \in \pi(G / 'O_p^'(G))q p].

End Five.