path: root/mathcomp/odd_order/BGsection5.v

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp
Require Import fintype finset prime fingroup morphism perm automorphism action.
From mathcomp
Require Import quotient cyclic gfunctor pgroup gproduct center commutator.
From mathcomp
Require Import gseries nilpotent sylow abelian maximal hall.
From mathcomp
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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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.
Proof.
move=> injf sHG; rewrite /narrow injm_p_rank //; congr (_ ==> _).
apply/set0Pn/set0Pn=> [] [E /setIP[Ep2E maxE]].
  exists (invm injf @* E)%G; rewrite -[H](group_inj (morphim_invm injf _)) //.
  have sEfG: E \subset f @* G. 
    by rewrite (subset_trans _ (morphimS _ sHG)) //; case/pnElemP: Ep2E.
  by rewrite inE injm_pnElem ?injm_pmaxElem ?injm_invm ?morphimS // Ep2E.
have sEG: E \subset G by rewrite (subset_trans _ sHG) //; case/pnElemP: Ep2E.
by exists (f @* E)%G; rewrite inE injm_pnElem ?injm_pmaxElem // Ep2E.
Qed.

Lemma isog_narrow G R : G \isog R -> p.-narrow G = p.-narrow R.
Proof. by case/isogP=> f injf <-; rewrite injm_narrow. Qed.

(* 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.
Proof. by apply: isog_narrow (isog_symr (conj_isog R x)). Qed.

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 -> exists E, E \in 'E_p^2(R) :&: 'E*_p(R).
Proof. by move=> nnP; apply: set0Pn; apply: implyP rR. Qed.

Let ntR : R :!=: 1. Proof. by case: eqP rR => // ->; rewrite p_rank1. Qed.
Let p_pr : prime p. Proof. by case: (pgroup_pdiv pR ntR). Qed.
Let p_gt1 : p > 1. Proof. exact: prime_gt1. Qed.

(* This is B & G, Lemma 5.1(a). *)
Lemma rank3_SCN3 : exists B, B \in 'SCN_3(R).
Proof.
by apply/set0Pn; rewrite -(rank2_SCN3_empty pR oddR) leqNgt (rank_pgroup pR) rR.
Qed.

(* 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.
Proof.
move=> Ep2E /andP[sER nER]; have [_ abelE dimE] := pnElemP Ep2E.
have [B Ep3B nBR]: exists2 B, B \in 'E_p^3(R) & R \subset 'N(B).
  have [C] := rank3_SCN3; case/setIdP=> SCN_C rC.
  have [nsCR cCC] := andP (maxgroupp (SCN_max SCN_C)).
  have [sCR _] := andP nsCR; have pC: p.-group C := pgroupS sCR pR.
  have{pC cCC} abelC1: p.-abelem 'Ohm_1(C) := Ohm1_abelem pC cCC.
  have dimC1: 3 <= logn p #|'Ohm_1(C)| by rewrite -rank_abelem // rank_Ohm1.
  have nsC1R: 'Ohm_1(C) <| R := gFnormal_trans _ nsCR.
  have [B [sBC1 nsBR oB]] := normal_pgroup pR nsC1R dimC1.
  have [sBR nBR] := andP nsBR; exists B => //; apply/pnElemP.
  by rewrite oB pfactorK // (abelemS sBC1).
have [sBR abelB dimB] := pnElemP Ep3B; have [pB cBB _] := and3P abelB.
have [oB oE] := (card_pnElem Ep3B, card_pnElem Ep2E).
pose Bs := (E <*> 'C_B(E))%G; have sCB: 'C_B(E) \subset B := subsetIl B _.
have sBsR: Bs \subset R by rewrite join_subG sER subIset ?sBR.
suffices Bs_gt2: 2 < logn p #|Bs|.
  have nBsR: Bs <| R by rewrite /normal sBsR // normsY ?normsI ?norms_cent.
  have abelBs: p.-abelem Bs.
    by rewrite (cprod_abelem p (cprodEY _)) ?subsetIr // abelE (abelemS sCB).
  have [C maxC sBsC] : {H | [max H | H <| R & abelian H ] & Bs \subset H}.
    by apply: maxgroup_exists; rewrite nBsR (abelem_abelian abelBs).
  exists C; last by rewrite (subset_trans _ sBsC) ?joing_subl.
  by rewrite inE (max_SCN pR) ?(leq_trans Bs_gt2) // -rank_abelem ?rankS.
apply: contraFT (ltnn 2); rewrite -leqNgt => Bs_le2.
have{Bs_le2} sCE: 'C_B(E) \subset E.
  rewrite (sameP joing_idPl eqP) eq_sym eqEcard joing_subl /=.
  by rewrite (card_pgroup (pgroupS sBsR pR)) oE leq_exp2l.
have dimCBE: 2 <= logn p #|'C_B(E)|.
  rewrite -ltnS -dimB -addn1 -leq_subLR -logn_div ?divgS ?cardSg //.
  by rewrite logn_quotient_cent_abelem ?dimE ?(subset_trans sBR nER).
have defE: 'C_B(E) = E.
  apply/eqP; rewrite eqEcard sCE oE /=.
  by rewrite (card_pgroup (pgroupS sCB pB)) leq_exp2l.
by rewrite -dimB -dimE -defE lognSg // subsetIidl sub_abelian_cent // -defE.
Qed.

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

Let ntZ : Z != 1.
Proof. by rewrite Ohm1_eq1 (center_nil_eq1 (pgroup_nil pR)). Qed.

Let sZR : Z \subset R. Proof. by rewrite !gFsub_trans. Qed.

Let abelZ : p.-abelem (Z). 
Proof. by rewrite (Ohm1_abelem (pgroupS _ pR)) ?center_sub ?center_abelian. Qed.

Let pZ : p.-group Z. Proof. exact: abelem_pgroup abelZ. Qed.

Let defCRZ : 'C_R(Z) = R.
Proof. by apply/setIidPl; rewrite centsC gFsub_trans ?subsetIr. Qed.

Let sWR : W \subset R. Proof. exact/gFsub_trans/gFsub. Qed.
Let nWR : R \subset 'N(W). Proof. exact/gFnorm_trans/gFnorm. Qed.

(* 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 ].
Proof.
case/setIP=> Ep2E maxE; have defCRE1 := Ohm1_cent_max maxE pR.
have [[sER abelE dimE] oE] := (pnElemP Ep2E, card_pnElem Ep2E).
have [[sZR_R nZR_R] [pE _ eE]] := (andP (center_normal R), and3P abelE).
have{nZR_R} nZR: R \subset 'N(Z) := gFnorm_trans _ nZR_R.
have{sZR_R} [pZR pW] := (pgroupS sZR_R pR, pgroupS sWR pR).
have sZE: Z \subset E by rewrite -defCRE1 OhmS ?setIS // centS.
have rCRE : 'r_p('C_R(E)) = 2 by rewrite -p_rank_Ohm1 defCRE1 p_rank_abelem.
have oZ: #|Z| = p.
  apply/prime_nt_dvdP; rewrite -?trivg_card1 // (card_pgroup pZ) /= -/Z.
  rewrite (@dvdn_exp2l _ _ 1) // -ltnS -dimE properG_ltn_log //= -/Z.
  by case/eqVproper: sZE rR => // defZ; rewrite -defCRZ defZ rCRE ltnn.
have ncycR: ~~ cyclic R by rewrite (odd_pgroup_rank1_cyclic pR) // -(subnKC rR).
have [ncycW eW] := Ohm1_odd_ucn2 pR oddR ncycR; rewrite -/W in ncycW eW.
have sWRZ: [~: W, R] \subset Z.
  rewrite [Z](OhmE 1 pZR) sub_gen //= -ucn1 subsetI.
  rewrite (subset_trans _ (ucn_comm 1 _)) ?commSg ?Ohm_sub //.
  by move: nWR eW; rewrite -commg_subl -sub_LdivT; apply: subset_trans.
have sZW: Z \subset W by rewrite OhmS /= -?ucn1 ?ucn_subS //.
have ltZW: Z \proper W.
  by rewrite properEneq; case: eqP ncycW => // <-; rewrite prime_cyclic ?oZ.
have sWRE := subset_trans sWRZ sZE.
have nEW: W \subset 'N(E) by rewrite -commg_subr (subset_trans _ sWRE) ?commgSS.
have defZ: 'C_W(E) = Z.
  have sCE: 'C_W(E) \subset E.
    rewrite -{2}defCRE1 (OhmE 1 (pgroupS (subsetIl R _) pR)) sub_gen //.
    by rewrite subsetI setSI // subIset // sub_LdivT eW.
  have [defC | ltCE] := eqVproper sCE.
    have sEW: E \subset W by rewrite -defC subsetIl.
    have nsER: E <| R.
      by rewrite /normal sER -commg_subl (subset_trans (commSg R sEW)).
    have [B scn3B sEB] := normal_p2Elem_SCN3 Ep2E nsER.
    have [scnB dimB] := setIdP scn3B; have [_ scBR] := SCN_P scnB.
    rewrite ltnNge -rank_Ohm1 -dimE -rank_abelem ?rankS // in dimB.
    by rewrite -scBR -defCRE1 OhmS // setIS ?centS.
  apply/eqP; rewrite eq_sym eqEcard oZ (card_pgroup (pgroupS sCE pE)) /= -/W.
  rewrite subsetI sZW (centsS sER); last by rewrite centsC -subsetIidl defCRZ.
  by rewrite (leq_exp2l _ 1) // -ltnS -dimE properG_ltn_log.
have dimW: logn p #|W| = 2.
  apply/eqP; rewrite -(Lagrange sZW) lognM ?cardG_gt0 // oZ (pfactorK 1) //=.
  rewrite -/Z eqSS eqn_leq -{1}defZ logn_quotient_cent_abelem ?dimE // -/W.
  by rewrite -divgS // logn_div ?cardSg // subn_gt0 properG_ltn_log.
have abelW: p.-abelem W.
  by rewrite (abelem_Ohm1 (pgroupS _ pR)) ?(p2group_abelian pW) ?dimW ?ucn_sub.
have charT: T \char R by rewrite subcent_char ?char_refl ?gFchar_trans.
rewrite 2!inE sWR abelW dimW; do 2?split => //.
  by apply: contra (proper_subn ltZW); rewrite -defZ !subsetI subxx sER centsC.
apply/prime_nt_dvdP=> //.
  rewrite indexg_eq1 subsetIidl centsC; apply: contraFN (ltnn 1) => cRW.
  by rewrite -dimW -(setIidPl (centsS sER cRW)) defZ oZ (pfactorK 1).
rewrite -(part_pnat_id (pnat_dvd (dvdn_indexg _ _) pR)) p_part.
by rewrite (@dvdn_exp2l p _ 1) ?logn_quotient_cent_abelem ?dimW.
Qed.

(* 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)].
Proof.
move=> nnR oS sSR rS; have pS : p.-group S := pgroupS sSR pR.
have [E maxEp2E] := narrow_pmaxElem nnR; have [Ep2E maxE] := setIP maxEp2E.
have [not_sET [oZ Ep2W] [charT maxT]] := Ohm1_ucn_p2maxElem maxEp2E.
have cZS : S \subset 'C(Z) by rewrite (subset_trans sSR) // -defCRZ subsetIr.
have nZS : S \subset 'N(Z) by rewrite cents_norm.
have cSS : abelian S by rewrite cyclic_abelian ?prime_cyclic // oS.
pose SZ := (S <*> [group of Z])%G; have sSSZ: S \subset SZ := joing_subl _ _.
have sSZ_R: SZ \subset R by rewrite join_subG sSR sZR.
have abelSZ : p.-abelem SZ.
  by rewrite /= joingC (cprod_abelem p (cprodEY cZS)) abelZ prime_abelem.
have tiSZ: S :&: Z = 1.
  rewrite prime_TIg ?oS //= -/Z; apply: contraL rR => sZS.
  by rewrite -leqNgt (leq_trans _ rS) ?p_rankS // -{1}defCRZ setIS ?centS.
have{tiSZ} oSZ: #|SZ| = (p ^ 2)%N by rewrite /= norm_joinEl ?TI_cardMg ?oS ?oZ.
have Ep2SZ: SZ \in 'E_p^2(R) by rewrite pnElemE // !inE sSZ_R abelSZ oSZ eqxx.
have{oSZ Ep2SZ abelSZ sSZ_R} maxSZ: SZ \in 'E_p^2(R) :&: 'E*_p(R).
  rewrite inE Ep2SZ; apply/pmaxElemP; rewrite inE sSZ_R abelSZ.
  split=> // H /setIdP[sHR abelH] sSZH.
  have [[_ _ dimSZ] [cHH pH _]] := (pnElemP Ep2SZ, and3P abelH).
  have sSH: S \subset H := subset_trans sSSZ sSZH.
  have{sSH} sH_CRS: H \subset 'C_R(S) by rewrite subsetI sHR (centsS sSH).
  have{sH_CRS}: 'r_p(H) <= 2 by rewrite (leq_trans _ rS) ?p_rankS.
  apply: contraTeq; rewrite eq_sym eqEproper sSZH negbK => lSZH.
  by rewrite -ltnNge p_rank_abelem // -dimSZ properG_ltn_log.
have sZT: Z \subset T.
  by rewrite subsetI sZR (centsS sWR) // centsC -defCRZ subsetIr.
have{SZ sSSZ maxSZ} not_sST: ~~ (S \subset T).
  have: ~~ (SZ \subset T) by case/Ohm1_ucn_p2maxElem: maxSZ.
  by rewrite join_subG sZT andbT.
have tiST: S :&: T :=: 1 by rewrite prime_TIg ?oS. 
have defST: S * T = R.
  apply/eqP; rewrite eqEcard TI_cardMg ?mul_subG ?subsetIl //=.
  by rewrite  mulnC oS -maxT Lagrange ?subsetIl.
have cRRb: abelian (R / T) by rewrite -defST quotientMidr quotient_abelian.
have sR'T: R^`(1) \subset T by rewrite der1_min ?char_norm. 
have TI_SR': S :&: R^`(1) :=: 1.
  by rewrite prime_TIg ?oS // (contra _ not_sST) // => /subset_trans->.
have defCRS : S \x 'C_T(S) = 'C_R(S).
  rewrite (dprodE _ _) ?subsetIr //= -/T; last by rewrite setIA tiST setI1g.
  rewrite -{1}(center_idP cSS) subcent_TImulg ?defST //.
  by rewrite subsetI normG (subset_trans sSR) ?char_norm.
have sCTSR: 'C_T(S) \subset R by rewrite subIset ?subsetIl.
split; rewrite ?(odd_pgroup_rank1_cyclic (pgroupS _ pR) (oddSg _ oddR)) //= -/T.
rewrite -ltnS (leq_trans _ rS) //= -(p_rank_dprod p defCRS) -add1n leq_add2r.
by rewrite -rank_pgroup // rank_gt0 -cardG_gt1 oS.
Qed.

(* 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 (exists S, [/\ gval S \subset R, #|S| = p & 'r_p('C_R(S)) <= 2])
          (p.-narrow R).
Proof.
rewrite /narrow rR; apply: (iffP (set0Pn _)) => [[E maxEp2E]|[S [sSR oS rCRS]]].
  have [Ep2E maxE] := setIP maxEp2E.
  have{maxEp2E} [_ [oZ _] _] := Ohm1_ucn_p2maxElem maxEp2E.
  have [sER abelE dimE] := pnElemP Ep2E; have oE := card_pnElem Ep2E.
  have sZE: Z \subset E by rewrite -(Ohm1_cent_max maxE pR) OhmS ?setIS ?centS.
  have [S defE] := abelem_split_dprod abelE sZE; exists S.
  have{defE} [[_ defZS _ _] oZS] := (dprodP defE, dprod_card defE).
  split; first by rewrite (subset_trans _ sER) // -defZS mulG_subr.
    by apply/eqP; rewrite -(eqn_pmul2l (ltnW p_gt1)) -{1}oZ oZS oE.
  rewrite -dimE -p_rank_abelem // -(Ohm1_cent_max maxE pR) p_rank_Ohm1.
  by rewrite -defZS /= centM setIA defCRZ.
have abelS := prime_abelem p_pr oS.
have cSZ: Z \subset 'C(S) by rewrite (centsS sSR) // centsC -defCRZ subsetIr.
have sSZR: S <*> Z \subset R by rewrite join_subG sSR.
have defSZ: S \x Z = S <*> Z.
  rewrite dprodEY ?prime_TIg ?oS //= -/Z; apply: contraL rR => sSZ.
  by rewrite -leqNgt (leq_trans _ rCRS) ?p_rankS // -{1}defCRZ setIS ?centS.
have abelSZ: p.-abelem (S <*> Z) by rewrite (dprod_abelem p defSZ) abelS.
have [pSZ cSZSZ _] := and3P abelSZ.
have dimSZ: logn p #|S <*> Z| = 2.
  apply/eqP; rewrite -p_rank_abelem // eqn_leq (leq_trans (p_rankS _ _) rCRS).
    rewrite -(p_rank_dprod p defSZ) p_rank_abelem // oS (pfactorK 1) // ltnS.
    by rewrite -rank_pgroup // rank_gt0.
  by rewrite subsetI sSZR sub_abelian_cent ?joing_subl.
exists [group of S <*> Z]; rewrite 3!inE sSZR abelSZ dimSZ /=.
apply/pmaxElemP; rewrite inE sSZR; split=> // E; case/pElemP=> sER abelE sSZE.
apply: contraTeq rCRS; rewrite eq_sym -ltnNge -dimSZ => neqSZE.
have [[pE cEE _] sSE] := (and3P abelE, subset_trans (joing_subl S Z) sSZE).
rewrite (leq_trans (properG_ltn_log pE _)) ?properEneq ?neqSZE //.
by rewrite -p_rank_abelem ?p_rankS // subsetI sER sub_abelian_cent.
Qed.

(* 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). *)
Lemma narrow_structureP : reflect (narrow_structure p R) (p.-narrow R).
Proof.
apply: (iffP idP) => [nnR | [S C sSR sCR oS cycC defSC]].
  have [S [sSR oS rCRS]] := narrow_centP nnR.
  have [cycC _ _ defCRS] := narrow_cent_dprod nnR oS sSR rCRS.
  by exists S [group of 'C_T(S)]; rewrite //= -setIA subsetIl.
apply/narrow_centP; exists S; split=> //.
have cycS: cyclic S by rewrite prime_cyclic ?oS.
rewrite -(p_rank_dprod p defSC) -!(rank_pgroup (pgroupS _ pR)) // -addn1.
rewrite leq_add -?abelian_rank1_cyclic ?cyclic_abelian //.
Qed.

End Rank3.

(* 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) -> forall x, x \in A -> p^'.-elt x -> #[x] %| p.-1].
Proof.
move=> nnR solA AutA oddA; have nilR := pgroup_nil pR.
have [rR | rR] := leqP 'r(R) 2.
  have pA' := der1_Aut_rank2_pgroup pR oddR rR AutA solA oddA.
  have sA'Ap: A^`(1) \subset 'O_p(A) by rewrite pcore_max ?der_normal.
  have cAbAb: abelian (A / 'O_p(A)) by rewrite sub_der1_abelian.
  split; rewrite // -(nilpotent_pcoreC p (abelian_nil cAbAb)).
  by rewrite trivg_pcore_quotient dprod1g pcore_pgroup.
have ntR: R :!=: 1 by rewrite -rank_gt0 2?ltnW.
rewrite (rank_pgroup pR) in rR.
have [H [charH sHRZ] _ eH pCH] := critical_odd pR oddR ntR.
have{ntR} [[p_pr _ _] sHR] := (pgroup_pdiv pR ntR, char_sub charH).
have ntH: H :!=: 1 by rewrite trivg_exponent eH -prime_coprime ?coprimen1.
have{nnR} [S C sSR sCR oS cycC defSC] := narrow_structureP rR nnR.
have [_ mulSC cSC tiSC] := dprodP defSC.
have abelS: p.-abelem S := prime_abelem p_pr oS; have [pS cSS _] := and3P abelS.
have cycS: cyclic S by rewrite prime_cyclic ?oS.
have tiHS: H :&: S = 1.
  have rCRS: 'r_p('C_R(S)) <= 2.
    rewrite -(p_rank_dprod p defSC) -addn1 -!rank_pgroup ?(pgroupS _ pR) //.
    by rewrite leq_add -?abelian_rank1_cyclic ?cyclic_abelian.
  rewrite setIC prime_TIg ?oS //; apply: contraL (rCRS) => sSH; rewrite -ltnNge.
  have cZHS: S \subset 'C('Z(H)) by rewrite centsC (centsS sSH) ?subsetIr.
  pose U := S <*> 'Z(H).
  have sUH: U \subset H by rewrite join_subG sSH subsetIl.
  have cUU: abelian U  by rewrite abelianY cSS center_abelian centsC.
  have abelU: p.-abelem U by rewrite abelemE // cUU -eH exponentS.
  have sUR: U \subset R := subset_trans sUH sHR.
  have rU: 'r_p(U) <= 'r_p('C_R(S)).
    by rewrite p_rankS //= subsetI sUR (centsS (joing_subl S 'Z(H))).
  have nsUR: U <| R.
    rewrite /normal sUR -commg_subl (subset_trans (commSg _ sUH)) //= -/U.
    by rewrite (subset_trans sHRZ) // joing_subr.
  have{rU}:= leq_trans rU rCRS; rewrite leq_eqVlt => /predU1P[] rU. 
    have Ep2U: [group of U] \in 'E_p^2(R).
      by rewrite !inE /= sUR abelU -(p_rank_abelem abelU) rU.
    have [F scn3F sUF] := normal_p2Elem_SCN3 rR Ep2U nsUR.
    have [scnF rF] := setIdP scn3F; have [_ scF] := SCN_P scnF. 
    rewrite (leq_trans rF) // -scF -rank_pgroup ?(pgroupS (subsetIl _ _)) //. 
    by rewrite rankS ?setIS ?centS // (subset_trans _ sUF) ?joing_subl.
  have defU: S :=: U.
    apply/eqP; rewrite eqEcard oS joing_subl (card_pgroup (pgroupS sUR pR)).
    by rewrite -p_rank_abelem // (leq_exp2l _ 1) // prime_gt1.
  have ntS: S :!=: 1 by rewrite -cardG_gt1 oS prime_gt1.
  have sSZ: S \subset 'Z(R) by rewrite prime_meetG ?oS ?meet_center_nil // defU.
  by rewrite (setIidPl _) // centsC (subset_trans sSZ) ?subsetIr.
have{tiHS eH} oCHS: #|'C_H(S)| = p.
  have ntCHS: 'C_H(S) != 1.
    have: H :&: 'Z(R) != 1 by rewrite meet_center_nil ?char_normal.
    by apply: subG1_contra; rewrite setIS // (centsS sSR) ?subsetIr.
  have cycCHS: cyclic 'C_H(S).
    have tiS_CHS: S :&: 'C_H(S) = 1 by rewrite setICA setIA tiHS setI1g.
    rewrite (isog_cyclic (quotient_isog _ tiS_CHS)) ?subIset ?cent_sub ?orbT //.
    rewrite (cyclicS _ (quotient_cyclic S cycC)) //= -(quotientMidl S C).
    by rewrite mulSC quotientS // setSI // char_sub.
  have abelCHS: p.-abelem 'C_H(S).
    by rewrite abelemE ?cyclic_abelian // -eH exponentS ?subsetIl.
  rewrite -(Ohm1_id abelCHS).
  by rewrite (Ohm1_cyclic_pgroup_prime _ (abelem_pgroup abelCHS)).
pose B := A^`(1) <*> [set a ^+ p.-1 | a in A].
have sBA: B \subset A.
  rewrite join_subG (der_sub 1 A) /=.
  by apply/subsetP=> _ /imsetP[a Aa ->]; rewrite groupX.
have AutB: B \subset Aut R := subset_trans sBA AutA.
suffices pB (X : {group {perm gT}}): X \subset B -> p^'.-group X -> X :=: 1.
  have cAbAb: abelian (A / 'O_p(A)).
    rewrite sub_der1_abelian // pcore_max ?der_normal //.
    apply/pgroupP=> q q_pr; apply: contraLR => p'q; rewrite -p'natE //.
    have [X sylX] := Sylow_exists q A^`(1); have [sXA' qX _] := and3P sylX.
    rewrite -partn_eq1 ?cardG_gt0 // -(card_Hall sylX).
    by rewrite (pB X) ?cards1 ?(pi_pgroup qX) ?(subset_trans sXA') ?joing_subl.
  rewrite cAbAb -(nilpotent_pcoreC p (abelian_nil cAbAb)) trivg_pcore_quotient.
  rewrite dprod1g pcore_pgroup; split=> //_ a Aa p'a. 
  rewrite order_dvdn -cycle_eq1 [<[_]>]pB ?(pgroupS (cycleX _ _) p'a) //.
  by rewrite genS // sub1set inE orbC (mem_imset (expgn^~ _)).
move=> sXB p'X; have AutX := subset_trans sXB AutB.
pose toX := ([Aut R] \ AutX)%gact; pose CX := 'C_(H | toX)(X).
suffices sHCX: H \subset CX.
  rewrite -(setIid X) coprime_TIg ?(pnat_coprime (pgroupS _ pCH)) //.
  by rewrite subsetIidl gacent_ract setIid gacentC in sHCX.
elim: _.+1 {1 2 4 6}H (charH) (subxx H) (ltnSn #|H|) => // n IHn L charL sLH.
rewrite ltnS => leLn; have sLR := char_sub charL; pose K := [~: L, R].
wlog ntL: / L :!=: 1 by case: eqP => [-> | _ -> //]; rewrite sub1G.
have charK: K \char R by rewrite charR ?char_refl.
have ltKL: K \proper L.
  have nLR: R \subset 'N_R(L) by rewrite subsetIidl char_norm.
  exact: nil_comm_properl nilR sLR ntL nLR.
have [sKL sKR] := (proper_sub ltKL, char_sub charK).
have [sKH pK] := (subset_trans sKL sLH, pgroupS sKR pR : p.-group K).
have nsKH: K <| H := normalS sKH sHR (char_normal charK).
have sKCX: K \subset CX by rewrite IHn ?(leq_trans (proper_card ltKL)) ?leLn.
have pL := pgroupS sLR pR; have nKL: L \subset 'N(K) := commg_norml _ _.
have{pS cSS} oLb: #|L / K| = p.
  have [v defS] := cyclicP cycS; rewrite defS cycle_subG in sSR.
  have ntLb: L / K != 1 by rewrite -subG1 quotient_sub1 ?proper_subn.
  have [_ p_dv_Lb _] := pgroup_pdiv (quotient_pgroup _ pL) ntLb.
  apply/eqP; rewrite eqn_leq {p_dv_Lb}(dvdn_leq _ p_dv_Lb) // andbT.
  rewrite -divg_normal ?(normalS sKL sLH nsKH) // leq_divLR ?cardSg //= -/K.
  rewrite -(card_lcoset K v) -(LagrangeI L 'C(S)) -indexgI /= -oCHS /K commGC.
  rewrite {2}defS cent_cycle index_cent1 leq_mul ?subset_leq_card ?setSI //.
  by apply/subsetP=> vx; case/imsetP=> x Lx ->; rewrite mem_lcoset mem_commg.
have cycLb: cyclic (L / K) by rewrite prime_cyclic ?oLb.
rewrite -(quotientSGK _ sKCX) // quotientGI // subsetI quotientS //= -/K.
have actsXK: [acts X, on K | toX] by rewrite acts_ract subxx acts_char.
rewrite ext_coprime_quotient_cent ?(pnat_coprime pK p'X) ?(pgroup_sol pK) //.
have actsAL : {acts A, on group L | [Aut R]} by apply: gacts_char.
have sAD: A \subset qact_dom <[actsAL]> [~: L, R].
  by rewrite qact_domE // acts_actby subxx (setIidPr sKL) acts_char.
suffices cLbX: X \subset 'C(L / K | <[actsAL]> / _).
  rewrite gacentE ?qact_domE // subsetI quotientS //=.
  apply/subsetP=> Ku LbKu; rewrite inE; apply/subsetP=> x Xx; rewrite inE.
  have [Dx cLx] := setIdP (subsetP cLbX x Xx); have [Ax _] := setIdP Dx.
  rewrite inE in cLx; have:= subsetP cLx Ku LbKu; rewrite inE /=.
  have [u Nu Lu ->] := morphimP LbKu.
  by rewrite !{1}qactE // ?actbyE // qact_domE ?(subsetP actsXK).
rewrite (subset_trans sXB) // astab_range -ker_actperm gen_subG.
rewrite -sub_morphim_pre; last by rewrite -gen_subG ?(subset_trans sBA).
rewrite morphimU subUset morphim_der // (sameP trivgP derG1P).
rewrite (abelianS _ (Aut_cyclic_abelian cycLb)); last first.
  exact: subset_trans (morphim_sub _ _) (im_actperm_Aut _).
apply/subsetP=> _ /morphimP[_ _ /imsetP[x Ax ->] ->].
have Dx := subsetP sAD x Ax; rewrite inE morphX //= -order_dvdn.
apply: dvdn_trans (order_dvdG (actperm_Aut _ Dx)) _.
by rewrite card_Aut_cyclic // oLb (@totient_pfactor p 1) ?muln1.
Qed.

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 G -> p.-Sylow(G) S -> p.-narrow S ->
    (2 < 'r(S)) ==> p.-length_1 G -> 
  [/\ (*a*) p^'.-Hall(G^`(1)) 'O_p^'(G^`(1))
    & (*c*) forall q, q \in \pi(G / 'O_p^'(G)) -> q <= p].
Proof.
move=> oddG solG sylS nnS; case: (leqP 'r(S) 2) => /= rS pl1G.
  have rG: 'r_p(G) <= 2 by rewrite -(rank_Sylow sylS).
  split=> [|q]; first by have [-> _ _] := rank2_der1_complement solG oddG rG.
  exact: rank2_max_pdiv solG oddG rG.
rewrite /pHall pcore_sub pcore_pgroup pnatNK /=.
rewrite -(pcore_setI_normal p^' (der_normal 1 G)) // setIC indexgI /=.
wlog Gp'1: gT G S oddG nnS solG sylS rS pl1G / 'O_p^'(G) = 1.
  set K := 'O_p^'(G); have [_ nKG] := andP (pcore_normal _ G : K <| G).
  move/(_ _ (G / K) (S / K))%G; rewrite quotient_sol ?quotient_odd //.
  have [[sSG pS _] p'K] := (and3P sylS, pcore_pgroup _ G : p^'.-group K).
  have [nKS nKG'] := (subset_trans sSG nKG, subset_trans (der_sub 1 G) nKG).
  have tiKS: K :&: S = 1 := coprime_TIg (p'nat_coprime p'K pS).
  have isoS := isog_symr (quotient_isog nKS tiKS).
  rewrite (isog_narrow p isoS) {isoS}(isog_rank isoS) quotient_pHall //.
  rewrite plength1_quo // trivg_pcore_quotient indexg1 /= -quotient_der //.
  by rewrite card_quotient //= -/K -(card_isog (quotient1_isog _)); apply.
rewrite Gp'1 indexg1 -(card_isog (quotient1_isog _)) -pgroupE.
have [sSG pS _] := and3P sylS; have oddS: odd #|S| := oddSg sSG oddG.
have ntS: S :!=: 1 by rewrite -rank_gt0 (leq_trans _ rS).
have [p_pr _ _] := pgroup_pdiv pS ntS; have p_gt1 := prime_gt1 p_pr.
have{pl1G} defS: 'O_p(G) = S.
  by rewrite (eq_Hall_pcore _ sylS) -?plength1_pcore_Sylow.
have nSG: G \subset 'N(S) by rewrite -defS gFnorm.
pose fA := restrm nSG (conj_aut S); pose A := fA @* G.
have AutA: A \subset Aut S by rewrite [A]im_restrm Aut_conj_aut.
have [solA oddA]: solvable A /\ odd #|A| by rewrite morphim_sol ?morphim_odd.
have [/= _ cAbAb p'A_dv_p1] := Aut_narrow pS oddS nnS solA AutA oddA.
have{defS} pKfA: p.-group ('ker fA).
  rewrite (pgroupS _ pS) //= ker_restrm ker_conj_aut.
  by rewrite -defS -Fitting_eq_pcore ?cent_sub_Fitting.
split=> [|q].
  rewrite -(pmorphim_pgroup pKfA) ?der_sub // morphim_der //.
  by rewrite (pgroupS (der1_min _ cAbAb)) ?pcore_pgroup ?gFnorm.
rewrite mem_primes => /and3P[q_pr _ /Cauchy[] // x Gx ox].
rewrite leq_eqVlt -implyNb; apply/implyP=> p'q; rewrite -(ltn_predK p_gt1) ltnS.
have ofAx: #[fA x] = q.
  apply/prime_nt_dvdP=> //; last by rewrite -ox morph_order.
  rewrite order_eq1; apply: contraNneq p'q => fAx1.
  by apply: (pgroupP pKfA); rewrite // -ox order_dvdG //; apply/kerP.
have p'fAx: p^'.-elt (fA x) by rewrite /p_elt ofAx pnatE.
by rewrite -ofAx dvdn_leq ?p'A_dv_p1 ?mem_morphim // -(subnKC p_gt1).
Qed.

End Five.