# 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.

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 f → H \subset G → p.-narrow (f @* H) = p.-narrow H.

Lemma isog_narrow G R : G \isog R → p.-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.

Let ntR : R :!=: 1.

Let p_pr : prime p.

Let p_gt1 : p > 1.

This is B & G, Lemma 5.1(a).

This is B & G, Lemma 5.1(b).

Lemma normal_p2Elem_SCN3 E :

E \in 'E_p^2(R) → E <| R → exists2 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).

E \in 'E_p^2(R) → E <| R → exists2 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 ].

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".

Theorem narrow_cent_dprod S :

p.-narrow R → #|S| = p → S \subset R → 'r_p('C_R(S)) ≤ 2 →

[/\ cyclic 'C_T(S), S :&: R^`(1) = 1, S :&: T = 1 & S \x 'C_T(S) = 'C_R(S)].

p.-narrow R → #|S| = p → S \subset R → 'r_p('C_R(S)) ≤ 2 →

[/\ cyclic 'C_T(S), S :&: R^`(1) = 1, S :&: T = 1 & S \x 'C_T(S) = 'C_R(S)].

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.

Corollary narrow_centP :

reflect (∃ S, [/\ gval S \subset R, #|S| = p & 'r_p('C_R(S)) ≤ 2])

(p.-narrow R).

reflect (∃ S, [/\ gval S \subset R, #|S| = p & 'r_p('C_R(S)) ≤ 2])

(p.-narrow R).

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 R → solvable A → A \subset Aut R → odd #|A| →

[/\ (*a*) p^'.-group (A / 'O_p(A)), abelian (A / 'O_p(A))

& (*b*) 2 < 'r(R) → ∀ x, x \in A → p^'.-elt x → #[x] %| p.-1].

End OneGroup.

p.-narrow R → solvable A → A \subset Aut R → odd #|A| →

[/\ (*a*) p^'.-group (A / 'O_p(A)), abelian (A / 'O_p(A))

& (*b*) 2 < 'r(R) → ∀ x, x \in A → p^'.-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.