# Library BGsection13

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div path fintype.

Require Import bigop finset prime fingroup morphism perm automorphism quotient.

Require Import action gproduct gfunctor pgroup cyclic center commutator.

Require Import gseries nilpotent sylow abelian maximal hall frobenius.

Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.

Require Import BGsection7 BGsection9 BGsection10 BGsection12.

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div path fintype.

Require Import bigop finset prime fingroup morphism perm automorphism quotient.

Require Import action gproduct gfunctor pgroup cyclic center commutator.

Require Import gseries nilpotent sylow abelian maximal hall frobenius.

Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.

Require Import BGsection7 BGsection9 BGsection10 BGsection12.

This file covers B & G, section 13; the title subject of the section,
prime and regular actions, was defined in the frobenius.v file.

Set Implicit Arguments.

Import GroupScope.

Section Section13.

Variable gT : minSimpleOddGroupType.

Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Types p q q_star r : nat.

Implicit Types A E H K L M Mstar N P Q Qstar R S T U V W X Y Z : {group gT}.

Section OneComplement.

Variables M E : {group gT}.

Hypotheses (maxM : M \in 'M) (hallE : \sigma(M)^'.-Hall(M) E).

Let sEM : E \subset M := pHall_sub hallE.

Let sM'E : \sigma(M)^'.-group E := pHall_pgroup hallE.

This is B & G, Lemma 13.1.

Lemma Msigma_setI_mmax_central p H :

H \in 'M → p \in \pi(E) → p \in \pi(H) → p \notin \tau1(H) →

[~: M`_\sigma :&: H, M :&: H] != 1 → gval H \notin M :^: G →

[/\ (*a*) ∀ P, P \subset M :&: H → p.-group P →

P \subset 'C(M`_\sigma :&: H),

(*b*) p \notin \tau2(H)

& (*c*) p \in \tau1(M) → p \in \beta(G)].

H \in 'M → p \in \pi(E) → p \in \pi(H) → p \notin \tau1(H) →

[~: M`_\sigma :&: H, M :&: H] != 1 → gval H \notin M :^: G →

[/\ (*a*) ∀ P, P \subset M :&: H → p.-group P →

P \subset 'C(M`_\sigma :&: H),

(*b*) p \notin \tau2(H)

& (*c*) p \in \tau1(M) → p \in \beta(G)].

This is B & G, Corollary 13.2.

Corollary cent_norm_tau13_mmax p P H :

(p \in \tau1(M)) || (p \in \tau3(M)) →

P \subset M → p.-group P → H \in 'M('N(P)) →

[/\ (*a*) ∀ P1, P1 \subset M :&: H → p.-group P1 →

P1 \subset 'C(M`_\sigma :&: H),

(*b*) ∀ X, X \subset E :&: H → \tau1(H)^'.-group X →

X \subset 'C(M`_\sigma :&: H)

& (*c*) [~: M`_\sigma :&: H, M :&: H] != 1 →

p \in \sigma(H) ∧ (p \in \tau1(M) → p \in \beta(H))].

(p \in \tau1(M)) || (p \in \tau3(M)) →

P \subset M → p.-group P → H \in 'M('N(P)) →

[/\ (*a*) ∀ P1, P1 \subset M :&: H → p.-group P1 →

P1 \subset 'C(M`_\sigma :&: H),

(*b*) ∀ X, X \subset E :&: H → \tau1(H)^'.-group X →

X \subset 'C(M`_\sigma :&: H)

& (*c*) [~: M`_\sigma :&: H, M :&: H] != 1 →

p \in \sigma(H) ∧ (p \in \tau1(M) → p \in \beta(H))].

This is B & G, Corollary 13.3(a).

This is B & G, Corollary 13.3(b).

This is B & G, Theorem 13.4.
Note how the non-structural steps in the proof (top of p. 99, where it is
deduced that C_M_alpha(P) <= C_M_alpha(R) from q \notin \alpha, and then
C_M_alpha(P) = C_M_alpha(R) from r \in tau_1(M) !!), are handled cleanly
on lines 5-12 of the proof by a conditional expression for the former, and
a without loss tactic for the latter.
Also note that the references to 10.12 and 12.2 are garbled (some are
missing, and some are exchanged!).

Theorem cent_tau1Elem_Msigma p r P R (Ms := M`_\sigma) :

p \in \tau1(M) → P \in 'E_p^1(E) → R \in 'E_r^1('C_E(P)) →

'C_Ms(P) \subset 'C_Ms(R).

p \in \tau1(M) → P \in 'E_p^1(E) → R \in 'E_r^1('C_E(P)) →

'C_Ms(P) \subset 'C_Ms(R).

This is B & G, Theorem 13.5.

This is B & G, Lemma 13.6.
The wording at the top of the proof is misleading: it should say: by
Corollary 12.14, it suffices to show that we can't have both q \in beta(M)
and X \notsubset M_sigma^(1). Also, the reference to 12.13 should be 12.19
or 10.9 (we've used 12.19 here).

Lemma cent_cent_Msigma_tau1_uniq E1 P q X (Ms := M`_\sigma) :

\tau1(M).-Hall(E) E1 → P \subset E1 → P :!=: 1 →

X \in 'E_q^1('C_Ms(P)) →

'M('C(X)) = [set M] ∧ (∀ S, q.-Sylow(Ms) S → 'M(S) = [set M]).

End OneComplement.

\tau1(M).-Hall(E) E1 → P \subset E1 → P :!=: 1 →

X \in 'E_q^1('C_Ms(P)) →

'M('C(X)) = [set M] ∧ (∀ S, q.-Sylow(Ms) S → 'M(S) = [set M]).

End OneComplement.

This is B & G, Lemma 13.7.
We've had to plug a gap in this proof: on p. 100, l. 6-7 it is asserted
the conclusion (E1 * E3 acts in a prime manner on M_sigma) follows from
the fact that E1 and E3 have coprime orders and act in a prime manner with
the same set of fixed points. This seems to imply the following argument:
For any x \in M_sigma,
C_(E1 * E3) [x] = C_E1[x] * C_E3[x] is either E1 * E3 or 1,
i.e., E1 * E3 acts in a prime manner on M_sigma.
This is improper because the distributivity of centralisers over coprime
products only hold under normality conditions that do not hold in this
instance. The correct argument, which involves using the prime action
assumption a second time, only relies on the fact that E1 and E3 are Hall
subgroups of the group E1 * E3. The fact that E3 <| E (Lemma 12.1(a)),
implicitly needed to justify that E1 * E3 is a group, can also be used to
simplify the argument, and we do so.

Lemma tau13_primact_Msigma M E E1 E2 E3 :

M \in 'M → sigma_complement M E E1 E2 E3 → ¬ semiregular E3 E1 →

semiprime M`_\sigma (E3 <*> E1).

M \in 'M → sigma_complement M E E1 E2 E3 → ¬ semiregular E3 E1 →

semiprime M`_\sigma (E3 <*> E1).

This is B & G, Lemma 13.8.
We had to plug a significant hole in the proof text: in the sixth
paragraph of the proof, it is asserted that because M = N_M(Q)M_alpha and
r is in pi(C_M(P)), P centralises some non-trivial r-subgroup of N_M(Q).
This does not seem to follow directly, even taking into account that r is
not in alpha(M): while it is true that N_M(Q) contains a Sylow r-subgroup
of M, this subgroup does not need to contain an r-group centralized by P.
We can only establish the required result by making use of the fact that M
has a normal p-complement K (because p is in tau_1(M)), as then N_K(Q)
will contain a p-invariant Sylow r-subgroup S of K and M (coprime action)
and then any r-subgroup of M centralised by P will be in K, and hence
conjugate in C_K(P) to a subgroup of S (coprime action again).

Lemma tau1_mmaxI_asymmetry M Mstar p P q Q q_star Qstar :

(*1*) [/\ M \in 'M, Mstar \in 'M & gval Mstar \notin M :^: G] →

(*2*) [/\ p \in \tau1(M), p \in \tau1(Mstar) & P \in 'E_p^1(M :&: Mstar)] →

(*3*) [/\ q.-Sylow(M :&: Mstar) Q, q_star.-Sylow(M :&: Mstar) Qstar,

P \subset 'N(Q) & P \subset 'N(Qstar)] →

(*4*) 'C_Q(P) = 1 ∧ 'C_Qstar(P) = 1 →

(*5*) 'N(Q) \subset Mstar ∧ 'N(Qstar) \subset M →

False.

(*1*) [/\ M \in 'M, Mstar \in 'M & gval Mstar \notin M :^: G] →

(*2*) [/\ p \in \tau1(M), p \in \tau1(Mstar) & P \in 'E_p^1(M :&: Mstar)] →

(*3*) [/\ q.-Sylow(M :&: Mstar) Q, q_star.-Sylow(M :&: Mstar) Qstar,

P \subset 'N(Q) & P \subset 'N(Qstar)] →

(*4*) 'C_Q(P) = 1 ∧ 'C_Qstar(P) = 1 →

(*5*) 'N(Q) \subset Mstar ∧ 'N(Qstar) \subset M →

False.

This is B & G, Theorem 13.9.

Theorem sigma_partition M Mstar :

M \in 'M → Mstar \in 'M → gval Mstar \notin M :^: G →

[predI \sigma(M) & \sigma(Mstar)] =i pred0.

M \in 'M → Mstar \in 'M → gval Mstar \notin M :^: G →

[predI \sigma(M) & \sigma(Mstar)] =i pred0.

This is B & G, Theorem 13.10.

Theorem tau13_regular M E E1 E2 E3 p P :

M \in 'M → sigma_complement M E E1 E2 E3 →

P \in 'E_p^1(E1) → ~~ (P \subset 'C(E3)) →

[/\ (*a*) semiregular E3 E1,

(*b*) semiregular M`_\sigma E3

& (*c*) 'C_(M`_\sigma)(P) != 1].

M \in 'M → sigma_complement M E E1 E2 E3 →

P \in 'E_p^1(E1) → ~~ (P \subset 'C(E3)) →

[/\ (*a*) semiregular E3 E1,

(*b*) semiregular M`_\sigma E3

& (*c*) 'C_(M`_\sigma)(P) != 1].

This is B & G, Corollary 13.11.

Corollary tau13_nonregular M E E1 E2 E3 :

M \in 'M → sigma_complement M E E1 E2 E3 → ¬ semiregular M`_\sigma E3 →

[/\ (*a*) E1 :!=: 1,

(*b*) E3 ><| E1 = E,

(*c*) semiprime M`_\sigma E

& (*d*) ∀ X, X \in 'E^1(E) → X <| E].

M \in 'M → sigma_complement M E E1 E2 E3 → ¬ semiregular M`_\sigma E3 →

[/\ (*a*) E1 :!=: 1,

(*b*) E3 ><| E1 = E,

(*c*) semiprime M`_\sigma E

& (*d*) ∀ X, X \in 'E^1(E) → X <| E].

This is B & G, Lemma 13.12.

Lemma tau12_regular M E p q P A :

M \in 'M → \sigma(M)^'.-Hall(M) E →

p \in \tau1(M) → P \in 'E_p^1(E) → q \in \tau2(M) → A \in 'E_q^2(E) →

'C_A(P) != 1 →

'C_(M`_\sigma)(P) = 1.

M \in 'M → \sigma(M)^'.-Hall(M) E →

p \in \tau1(M) → P \in 'E_p^1(E) → q \in \tau2(M) → A \in 'E_q^2(E) →

'C_A(P) != 1 →

'C_(M`_\sigma)(P) = 1.

This is B & G, Lemma 13.13.