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

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 'Mp \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 :&: Hp.-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 Mp.-group PH \in 'M('N(P))
[/\ (*a*) P1, P1 \subset M :&: Hp.-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).

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) E1P \subset E1P :!=: 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.
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.

This is B & G, Theorem 13.9.
Theorem sigma_partition M Mstar :
M \in 'MMstar \in 'Mgval 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 'Msigma_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 'Msigma_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.

This is B & G, Lemma 13.13.
Lemma tau13_nonregular_sigma M E p P :
M \in 'M\sigma(M)^'.-Hall(M) E
P \in 'E_p^1(E)(p \in \tau1(M)) || (p \in \tau3(M))
'C_(M`_\sigma)(P) != 1 →
{in 'M('N(P)), Mstar, p \in \sigma(Mstar)}.

End Section13.