# Library BGsection15

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

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

Require Import path bigop finset prime fingroup morphism perm automorphism.

Require Import quotient action gproduct gfunctor pgroup cyclic commutator.

Require Import center gseries nilpotent sylow abelian maximal hall frobenius.

Require Import BGsection1 BGsection2 BGsection3 BGsection4 BGsection5.

Require Import BGsection6 BGsection7 BGsection9 BGsection10 BGsection12.

Require Import BGsection13 BGsection14.

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

Require Import path bigop finset prime fingroup morphism perm automorphism.

Require Import quotient action gproduct gfunctor pgroup cyclic commutator.

Require Import center gseries nilpotent sylow abelian maximal hall frobenius.

Require Import BGsection1 BGsection2 BGsection3 BGsection4 BGsection5.

Require Import BGsection6 BGsection7 BGsection9 BGsection10 BGsection12.

Require Import BGsection13 BGsection14.

This file covers B & G, section 15; it fills in the picture of maximal
subgroups that was sketched out in section14, providing an intrinsic
characterization of M`_\sigma and establishing the TI property for the
"kernels" of maximal groups. We introduce only one new definition:
M`_\F == the (direct) product of all the normal Sylow subgroups of M;
equivalently, the largest normal nilpotent Hall subgroup of M
We will refer to M`_\F as the Fitting core or F-core of M.

Set Implicit Arguments.

Import GroupScope.

Section Definitions.

Variables (gT : finGroupType) (M : {set gT}).

Definition Fitting_core :=

<<\bigcup_(P : {group gT} | Sylow M P && (P <| M)) P>>.

Canonical Structure Fitting_core_group := [group of Fitting_core].

End Definitions.

Notation "M `_ \F" := (Fitting_core M)

(at level 3, format "M `_ \F") : group_scope.

Notation "M `_ \F" := (Fitting_core_group M) : Group_scope.

Section FittingCore.

Variable (gT : finGroupType) (M : {group gT}).

Implicit Types H P : {group gT}.

Implicit Type p : nat.

Lemma Fcore_normal : M`_\F <| M.

Hint Resolve Fcore_normal.

Lemma Fcore_sub : M`_\F \subset M.

Lemma Fcore_sub_Fitting : M`_\F \subset 'F(M).

Lemma Fcore_nil : nilpotent M`_\F.

Lemma Fcore_max pi H :

pi.-Hall(M) H → H <| M → nilpotent H → H \subset M`_\F.

Lemma Fcore_dprod : \big[dprod/1]_(P | Sylow M (gval P) && (P <| M)) P = M`_\F.

Lemma Fcore_pcore_Sylow p : p \in \pi(M`_\F) → p.-Sylow(M) 'O_p(M).

Lemma p_core_Fcore p : p \in \pi(M`_\F) → 'O_p(M`_\F) = 'O_p(M).

Lemma Fcore_Hall : \pi(M`_\F).-Hall(M) M`_\F.

Lemma pcore_Fcore pi : {subset pi ≤ \pi(M`_\F)} → 'O_pi(M`_\F) = 'O_pi(M).

Lemma Fcore_pcore_Hall pi : {subset pi ≤ \pi(M`_\F)} → pi.-Hall(M) 'O_pi(M).

End FittingCore.

Lemma morphim_Fcore : GFunctor.pcontinuous Fitting_core.

Canonical Structure Fcore_igFun := [igFun by Fcore_sub & morphim_Fcore].

Canonical Structure Fcore_gFun := [gFun by morphim_Fcore].

Canonical Structure Fcore_pgFun := [pgFun by morphim_Fcore].

Section MoreFittingCore.

Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).

Implicit Types (M H : {group gT}) (R : {group rT}).

Lemma Fcore_char M : M`_\F \char M.

Lemma FcoreJ M x : (M :^ x)`_\F = M`_\F :^ x.

Lemma injm_Fcore M : 'injm f → M \subset D → f @* M`_\F = (f @* M)`_\F.

Lemma isom_Fcore M R : isom M R f → M \subset D → isom M`_\F R`_\F f.

Lemma isog_Fcore M R : M \isog R → M`_\F \isog R`_\F.

End MoreFittingCore.

Section Section15.

Variable gT : minSimpleOddGroupType.

Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Types p q q_star r : nat.

Implicit Types x y z : gT.

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

Lemma Fcore_sub_Msigma M : M \in 'M → M`_\F \subset M`_\sigma.

Lemma Fcore_eq_Msigma M :

M \in 'M → reflect (M`_\F = M`_\sigma) (nilpotent M`_\sigma).

This is B & G, Lemma 15.1.
We have made all semidirect products explicits, and omitted the assertion
M`_\sigma \subset M^`(1), which is exactly covered by Msigma_der1.
Some refactoring is definitely needed here, to avoid the mindless cut
and paste of a large fragment of the proof of Lemma 12.12.

Lemma kappa_structure M U K (Ms := M`_\sigma) :

M \in 'M → kappa_complement M U K →

[/\ (*a*) [/\ (Ms ><| U) ><| K = M, cyclic K & abelian (M^`(1) / Ms)],

(*b*) K :!=: 1 → Ms ><| U = M^`(1) ∧ abelian U,

(*c*) ∀ X, X \subset U → X :!=: 1 → 'C_Ms(X) != 1 →

[/\ 'M('C(X)) = [set M], cyclic X & \tau2(M).-group X],

(*d*) abelian <<\bigcup_(x in Ms^#) 'C_U[x]>>

& (*e*) U :!=: 1 → ∃ U0,

[/\ gval U0 \subset U, exponent (gval U0) = exponent U

& [Frobenius Ms <*> U0 = Ms ><| U0]]].

M \in 'M → kappa_complement M U K →

[/\ (*a*) [/\ (Ms ><| U) ><| K = M, cyclic K & abelian (M^`(1) / Ms)],

(*b*) K :!=: 1 → Ms ><| U = M^`(1) ∧ abelian U,

(*c*) ∀ X, X \subset U → X :!=: 1 → 'C_Ms(X) != 1 →

[/\ 'M('C(X)) = [set M], cyclic X & \tau2(M).-group X],

(*d*) abelian <<\bigcup_(x in Ms^#) 'C_U[x]>>

& (*e*) U :!=: 1 → ∃ U0,

[/\ gval U0 \subset U, exponent (gval U0) = exponent U

& [Frobenius Ms <*> U0 = Ms ><| U0]]].

This is B & G, Theorem 15.2.
It is this theorem that implies that the non-functorial definition of
M`_\sigma used in B & G is equivalent to the original definition in FT
(also used in Peterfalvi).
Proof notes: this proof contained two non-structural arguments: taking D
to be K-invariant, and reusing the nilpotent Frobenius kernel argument for
Q1 (bottom of p. 118). We handled the first with a "without loss", but for
the second we had to spell out explicitly the assumptions and conclusions
of the nilpotent kernel argument that were spread throughout the last
paragraph p. 118.
We also had to make a few additions to the argument at the top of p. 119;
while the statement of the Theorem states that F(M) = C_M(Qbar), the text
only shows that F(M) = C_Msigma(Qbar), and we need to show that K acts
regularly on Qbar to complete the proof; this follows from the values of
orders of K, Kstar and Qbar. In addition we need to show much earlier
that K acts faithfully on Q, to show that C_M(Q) is included in Ms, and
this requires a use of 14.2(e) not mentioned in the text; in addition, the
reference to coprime action (Proposition 1.5) on p. 119 l. 1 is somewhat
misleading, since we actually need to use the coprime stabilizer Lemma 1.9
to show that C_D(Qbar) = C_D(Q) = 1 (unless we splice in the proof of that
lemma).

Theorem Fcore_structure M (Ms := M`_\sigma) :

M \in 'M →

[/\ M`_\F != 1, M`_\F \subset Ms, Ms \subset M^`(1) & M^`(1) \proper M]

∧ (∀ K D : {group gT},

\kappa(M).-Hall(M) K → M`_\F != M`_\sigma →

let p := #|K| in let Ks := 'C_Ms(K) in

let q := #|Ks| in let Q := 'O_q(M) in

let Q0 := 'C_Q(D) in let Qbar := Q / Q0 in

q^'.-Hall(M`_\sigma) D →

[/\ (*a*) [/\ M \in 'M_'P1, Ms ><| K = M & Ms = M ^`(1)],

(*b*) [/\ prime p, prime q, q \in \pi(M`_\F) & q \in \beta(M)],

[/\ (*c*) q.-Sylow(M) Q,

(*d*) nilpotent D

& (*e*) Q0 <| M],

(*f*) [/\ minnormal Qbar (M / Q0), q.-abelem Qbar & #|Qbar| = (q ^ p)%N]

& (*g*) [/\ Ms^`(1) = M^`(2),

M^`(2) \subset 'F(M),

[/\ Q <*> 'C_M(Q) = 'F(M),

'C_M(Qbar | 'Q) = 'F(M)

& 'C_Ms (Ks / Q0 | 'Q) = 'F(M)]

& 'F(M) \proper Ms]]).

M \in 'M →

[/\ M`_\F != 1, M`_\F \subset Ms, Ms \subset M^`(1) & M^`(1) \proper M]

∧ (∀ K D : {group gT},

\kappa(M).-Hall(M) K → M`_\F != M`_\sigma →

let p := #|K| in let Ks := 'C_Ms(K) in

let q := #|Ks| in let Q := 'O_q(M) in

let Q0 := 'C_Q(D) in let Qbar := Q / Q0 in

q^'.-Hall(M`_\sigma) D →

[/\ (*a*) [/\ M \in 'M_'P1, Ms ><| K = M & Ms = M ^`(1)],

(*b*) [/\ prime p, prime q, q \in \pi(M`_\F) & q \in \beta(M)],

[/\ (*c*) q.-Sylow(M) Q,

(*d*) nilpotent D

& (*e*) Q0 <| M],

(*f*) [/\ minnormal Qbar (M / Q0), q.-abelem Qbar & #|Qbar| = (q ^ p)%N]

& (*g*) [/\ Ms^`(1) = M^`(2),

M^`(2) \subset 'F(M),

[/\ Q <*> 'C_M(Q) = 'F(M),

'C_M(Qbar | 'Q) = 'F(M)

& 'C_Ms (Ks / Q0 | 'Q) = 'F(M)]

& 'F(M) \proper Ms]]).

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

Corollary cent_Hall_sigma_sdprod M H pi :

M \in 'M → pi.-Hall(M`_\sigma) H → H :!=: 1 →

∃ X, [/\ gval X \subset M, cyclic X, \tau2(M).-group X

& 'C_(M`_\sigma)(H) ><| X = 'C_M(H)].

M \in 'M → pi.-Hall(M`_\sigma) H → H :!=: 1 →

∃ X, [/\ gval X \subset M, cyclic X, \tau2(M).-group X

& 'C_(M`_\sigma)(H) ><| X = 'C_M(H)].

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

Corollary sigma_Hall_tame M H pi x a :

M \in 'M → pi.-Hall(M`_\sigma) H → x \in H → x ^ a \in H →

exists2 b, b \in 'N_M(H) & x ^ a = x ^ b.

M \in 'M → pi.-Hall(M`_\sigma) H → x \in H → x ^ a \in H →

exists2 b, b \in 'N_M(H) & x ^ a = x ^ b.

This is B & G, Corollary 15.4.
This result does not appear to be needed for the actual proof.

Corollary nilpotent_Hall_sigma H :

nilpotent H → Hall G H → exists2 M, M \in 'M & H \subset M`_\sigma.

nilpotent H → Hall G H → exists2 M, M \in 'M & H \subset M`_\sigma.

This is B & G, Corollary 15.5.
We have changed the condition K != 1 to the equivalent M \in 'M_'P, as
avoids a spurrious quantification on K.
The text is quite misleading here, since Corollary 15.3(a) is needed for
bith the nilpotent and the non-nilpotent case -- indeed, it is not really
needed in the non-nilpotent case!

Corollary Fitting_structure M (H := M`_\F) (Y := 'O_\sigma(M)^'('F(M))) :

M \in 'M →

[/\ (*a*) cyclic Y ∧ \tau2(M).-group Y,

(*b*) [/\ M^`(2) \subset 'F(M),

H \* 'C_M(H) = 'F(M)

& 'F(M`_\sigma) \x Y = 'F(M)],

(*c*) H \subset M^`(1) ∧ nilpotent (M^`(1) / H)

& (*d*) M \in 'M_'P → 'F(M) \subset M^`(1)].

M \in 'M →

[/\ (*a*) cyclic Y ∧ \tau2(M).-group Y,

(*b*) [/\ M^`(2) \subset 'F(M),

H \* 'C_M(H) = 'F(M)

& 'F(M`_\sigma) \x Y = 'F(M)],

(*c*) H \subset M^`(1) ∧ nilpotent (M^`(1) / H)

& (*d*) M \in 'M_'P → 'F(M) \subset M^`(1)].

This is B & G, Corollary 15.6.
Note that the proof of the F-core noncyclicity given in the text only
applies to the nilpotent case, and we need to use a different assertion of
15.2 if Msigma is not nilpotent.

Corollary Ptype_cyclics M K (Ks := 'C_(M`_\sigma)(K)) :

M \in 'M_'P → \kappa(M).-Hall(M) K →

[/\ Ks != 1, cyclic Ks, Ks \subset M^`(2), Ks \subset M`_\F

& ~~ cyclic M`_\F].

M \in 'M_'P → \kappa(M).-Hall(M) K →

[/\ Ks != 1, cyclic Ks, Ks \subset M^`(2), Ks \subset M`_\F

& ~~ cyclic M`_\F].

This is B & G, Theorem 15.7.
We had to change the statement of the Theorem, because the first equality
of part (c) does not appear to be valid: if M is of type F, we know very
little of the action E1 on the Sylow subgroups of E2, and so E2 might have
a Sylow subgroup that meets F(M) but is also centralised by E1 and hence
intesects M' trivially; luckily, only the inclusion M' \subset F(M) seems
to be needed in the sequel.
We have also restricted the quantification on the Ei to part (c), and
factored and simplified some of the assertions of parts (e2) and (e3); it
appears they could perhaps be simplified futher, since the assertions on
Op(H) and Op'(H) do not appear to be used in the Peterfalvi revision of
the character theory part of the proof.
Proof notes: we had to correct/complete several arguments of the B & G
text. The use of 12.6(d) for parts (c) and (d), p. 120, l. 5 from the
bottom, is inapropriate as tau2 could be empty. The assertion X1 != Z0 on
l. 5, p. 121 needs to be strengthened to ~~ (X1 \subset Z0) in order to
prove that #|Z0| is prime -- only then are the assertions equivalent. The
use of Lemma 10.13(b), l. 7, p. 121, requires that B be maximal in G, not
only in P as is stated l. 6; proving the stronger assertion requires using
Corollary 15.3(b), which the text does not mention. The regularity
property stated l. 11-13 is too weak to be used in the type P1 case -- the
regularity assumption need to be restricted to a subgroup of prime order.
Finally, the cyclicity of Z(H) is not actually needed in the proof.

Theorem nonTI_Fitting_structure M g (H := (M`_\F)%G) :

let X := ('F(M) :&: 'F(M) :^ g)%G in

M \in 'M → g \notin M → X :!=: 1 →

[/\ (*a*) M \in 'M_'F :|: 'M_'P1 ∧ H :=: M`_\sigma,

(*b*) X \subset H ∧ cyclic X,

(*c*) M^`(1) \subset 'F(M) ∧ M`_\sigma \x 'O_\sigma(M)^'('F(M)) = 'F(M),

(*d*) ∀ E E1 E2 E3, sigma_complement M E E1 E2 E3 →

[/\ E3 :=: 1, E2 <| E, E / E2 \isog E1 & cyclic (E / E2)]

& (*e*) (*1*) [/\ M \in 'M_'F, abelian H & 'r(H) = 2]

∨ let p := #|X| in [/\ prime p, ~~ abelian 'O_p(H), cyclic 'O_p^'(H)

& (*2*) {in \pi(H), ∀ q, exponent (M / H) %| q.-1}

∨ (*3*) [/\ #|'O_p(H)| = (p ^ 3)%N, M \in 'M_'P1 & #|M / H| %| p.+1]

]].

let X := ('F(M) :&: 'F(M) :^ g)%G in

M \in 'M → g \notin M → X :!=: 1 →

[/\ (*a*) M \in 'M_'F :|: 'M_'P1 ∧ H :=: M`_\sigma,

(*b*) X \subset H ∧ cyclic X,

(*c*) M^`(1) \subset 'F(M) ∧ M`_\sigma \x 'O_\sigma(M)^'('F(M)) = 'F(M),

(*d*) ∀ E E1 E2 E3, sigma_complement M E E1 E2 E3 →

[/\ E3 :=: 1, E2 <| E, E / E2 \isog E1 & cyclic (E / E2)]

& (*e*) (*1*) [/\ M \in 'M_'F, abelian H & 'r(H) = 2]

∨ let p := #|X| in [/\ prime p, ~~ abelian 'O_p(H), cyclic 'O_p^'(H)

& (*2*) {in \pi(H), ∀ q, exponent (M / H) %| q.-1}

∨ (*3*) [/\ #|'O_p(H)| = (p ^ 3)%N, M \in 'M_'P1 & #|M / H| %| p.+1]

]].

A subset of the above, that does not require the non-TI witness.

Lemma nonTI_Fitting_facts M :

M \in 'M → ~~ normedTI 'F(M)^# G M →

[/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)].

M \in 'M → ~~ normedTI 'F(M)^# G M →

[/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)].

This is B & G, Theorem 15.8, due to Feit and Thompson (1991).
We handle the non-structural step on l. 5, p. 122 by choosing A not to be
a q-group, if possible, so that when it turns out to be we know q is the
only prime in tau2(H). Since this uniqueness does not appear to be used
later we could also eliminate this complication.
We also avoid the circularity in proving that A is a q-group and that Q
is non-abelian by deriving that Q is in U from 14.2(e) rather than 12.13.

Theorem tau2_P2type_signalizer M Mstar U K r R H (q := #|K|) :

M \in 'M_'P2 → kappa_complement M U K → Mstar \in 'M('C(K)) →

r.-Sylow(U) R → H \in 'M('N(R)) → ~~ \tau2(H)^'.-group H →

[/\ prime q, \tau2(H) =i (q : nat_pred) & \tau2(M)^'.-group M].

M \in 'M_'P2 → kappa_complement M U K → Mstar \in 'M('C(K)) →

r.-Sylow(U) R → H \in 'M('N(R)) → ~~ \tau2(H)^'.-group H →

[/\ prime q, \tau2(H) =i (q : nat_pred) & \tau2(M)^'.-group M].

This is B & G, Theorem 15.9, parts (a) and (b), due to D. Sibley and Feit
and Thompson, respectively.
We have dropped part (c) because it is not used later, and localizing the
quantification on r would complicate the proof needlessly.