(Joint Center)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.

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) HH <| Mnilpotent HH \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 fM \subset Df @* M`_\F = (f @* M)`_\F.

Lemma isom_Fcore M R : isom M R fM \subset Disom M`_\F R`_\F f.

Lemma isog_Fcore M R : M \isog RM`_\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 'MM`_\F \subset M`_\sigma.

Lemma Fcore_eq_Msigma M :
  M \in 'Mreflect (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 'Mkappa_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 UX :!=: 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) KM`_\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 'Mpi.-Hall(M`_\sigma) HH :!=: 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 'Mpi.-Hall(M`_\sigma) Hx \in Hx ^ 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 HHall G Hexists2 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)].

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

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 'Mg \notin MX :!=: 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.
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_'P2kappa_complement M U KMstar \in 'M('C(K))
    r.-Sylow(U) RH \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.
Theorem nonFtype_signalizer_base M x :
   M \in 'Mx \in M`_\sigma^#
   ~~ ('C[x] \subset M)'N[x] \notin 'M_'F
 [/\ (*a*) M \in 'M_'F, 'N[x] \in 'M_'P2
   & (*b*) exists2 E : {group gT}, \sigma(M)^'.-Hall(M) E
         & cyclic (gval E) [Frobenius M = M`_\sigma ><| E]].

End Section15.