(Joint Center)Library BGsection16

(* (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 BGsection2 BGsection3 BGsection4 BGsection5.
Require Import BGsection6 BGsection7 BGsection9 BGsection10 BGsection12.
Require Import BGsection13 BGsection14 BGsection15.

This file covers B & G, section 16; it summarises all the results of the local analysis. Some of the definitions of B & G have been adapted to fit in beter with Peterfalvi, section 8, dropping unused properties and adding a few missing ones. This file also defines the following: of_typeF M U <-> M = M`_\F ><| U is of type F, in the sense of Petervalvi (8.1) rather than B & G section 14. is_typeF_complement M U U0 <-> U0 is a subgroup of U with the same exponent as U, such that M`_\F ><| U0 is a Frobenius group; this corresponds to Peterfalvi (8.1)(c). is_typeF_inertia M U U1 <-> U1 <| U is abelian and contains 'C_U[x] for all x in M`_\F^#, and thus the inertia groups of all nonprincipal irreducible characters of M`_\F; this corresponds to Peterfalvi (8.1)(b). of_typeI M U <-> M = M`_\F ><| U is of type I, in the sense of Peterfalvi (8.3); this definition is almost identical to B & G conditions (Ii) - (Iv), except that (Iiv) is dropped, as is the condition p \in \pi* in (Iv)(c). Also, the condition 'O_p^'(M) cyclic, present in both B & G and Peterfalvi, is weakened to 'O_p^'(M`_\F) cyclic, because B & G, Theorem 15.7 only proves the weaker statement, and we did not manage to improve it. This appears to be a typo in B & G that was copied over to Petrfalvi (8.3). It is probably no consequence because (8.3) is only used in (12.6) and (12.10) and neither use the assumption that 'O_p^'(M) is cyclic. For defW : W1 \x W2 = W we also define: of_typeP M U defW <-> M = M`_\F ><| U ><| W1 is of type P, in the sense of Peterfalvi (8.4) rather than B & G section 14, where (8.4)(d,e) hold for W and W2 (i.e., W2 = C_M^(1)(W1)). of_typeII_IV M U defW <-> M = M`_\F ><| U ><| W1 is of type II, III, or IV in the sense of Peterfalvi (8.6)(a). This is almost exactly the contents of B & G, (T1)-(T7), except that (T6) is dropped, and 'C_(M`_\F)(W1) \subset M^`(2) is added (PF, (8.4)(d) and B & G, Theorem C(3)). of_typeII M U defW <-> M = M`_\F ><| U ><| W1 is of type II in the sense of Peterfalvi (8.6); this differs from B & G by dropping the rank 2 clause in IIiii and replacing IIv by B(2)(3) (note that IIv is stated incorrectly: M' should be M'^#). of_typeIII M U defW <-> M = M`_\F ><| U ><| W1 is of type III in the sense of Peterfalvi (8.6). of_typeIV M U defW <-> M = M`_\F ><| U ><| W1 is of type IV in the sense of Peterfalvi (8.6). of_typeV M U defW <-> U = 1 and M = M`_\F ><| W1 is of type V in the sense of Peterfalvi (8.7); this differs from B & G (V) dropping the p \in \pi* condition in clauses (V)(b) and (V)(c). exists_typeP spec <-> spec U defW holds for some groups U, W, W1 and W2 such that defW : W1 \x W2 = W; spec will be one of (of_typeP M), (of_typeII_IV M), (of_typeII M), etc. FTtype_spec i M <-> M is of type i, for 0 < i <= 5, in the sense of the predicates above, for the appropriate complements to M`_\F and M^`(1). FTtype M == the type of M, in the sense above, when M is a maximal subgroup of G (this is an integer i between 1 and 5). M`_\s == an alternative, combinatorial definition of M`_\sigma := M`_\F if M is of type I or II, else M^`(1) 'A1(M) == the "inner Dade support" of a maximal group M, as defined in Peterfalvi (8.10). := (M`_\s)^# 'A(M) == the "Dade support" of M as defined in Peterfalvi (8.10) (this differs from B & G by excluding 1). 'A0(M) == the "outer Dade support" of M as defined in Peterfalvi (8.10) (this differs from B & G by excluding 1). 'M^G == a transversal of the conjugacy classes of 'M.

Set Implicit Arguments.

Import GroupScope.

Section GeneralDefinitions.

Variable gT : finGroupType.
Implicit Types V W X : {set gT}.

End GeneralDefinitions.

Section Definitions.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Types M U V W X : {set gT}.

Definition is_typeF_inertia M U (H := M`_\F) U1 :=
  [/\ U1 <| U, abelian U1 & {in H^#, x, 'C_U[x] \subset U1}].

Definition is_typeF_complement M U (H := M`_\F) U0 :=
  [/\ U0 \subset U, exponent U0 = exponent U & [Frobenius H <*> U0 = H ><| U0]].

Definition of_typeF M U (H := M`_\F) :=
 [/\ (*a*) [/\ H != 1, U :!=: 1 & H ><| U = M],
     (*b*) U1 : {group gT}, is_typeF_inertia M U U1
   & (*c*) U0 : {group gT}, is_typeF_complement M U U0].

Definition of_typeI M (H := M`_\F) U :=
    of_typeF M U
   [\/ (*a*) normedTI H^# G M,
         (*b*) abelian H 'r(H) = 2
       | (*c*) {in \pi(H), p, exponent U %| p.-1}
             (exists2 p, p \in \pi(H) & cyclic 'O_p^'(H))].

Section Ptypes.

Variables M U W W1 W2 : {set gT}.
Let H := M`_\F.
Let M' := M^`(1).
Implicit Type defW : W1 \x W2 = W.

Definition of_typeP defW :=
  [/\ (*a*) [/\ cyclic W1, Hall M W1, W1 != 1 & M' ><| W1 = M],
      (*b*) [/\ nilpotent U, U \subset M', W1 \subset 'N(U) & H ><| U = M'],
      (*c*) [/\ ~~ cyclic H, M^`(2) \subset 'F(M), H × 'C_M(H) = 'F(M)
              & 'F(M) \subset M'],
      (*d*) [/\ cyclic W2, W2 != 1, W2 \subset H, W2 \subset M^`(2)
              & {in W1^#, x, 'C_M'[x] = W2}]
    & (*e*) normedTI (W :\: (W1 :|: W2)) G W].

Definition of_typeII_IV defW :=
  [/\ of_typeP defW, U != 1, prime #|W1| & normedTI 'F(M)^# G M].

Definition of_typeII defW :=
  [/\ of_typeII_IV defW, abelian U, ~~ ('N(U) \subset M),
      of_typeF M' U & M'`_\F = H].

Definition of_typeIII defW :=
  [/\ of_typeII_IV defW, abelian U & 'N(U) \subset M].

Definition of_typeIV defW :=
  [/\ of_typeII_IV defW, ~~ abelian U & 'N(U) \subset M].

Definition of_typeV defW :=
  [/\ of_typeP defW U = 1
   & [\/ (*a*) normedTI H^# G M,
         (*b*) exists2 p, p \in \pi(H) & #|W1| %| p.-1 cyclic 'O_p^'(H)
      | (*c*) exists2 p, p \in \pi(H)
             & [/\ #|'O_p(H)| = (p ^ 3)%N, #|W1| %| p.+1 & cyclic 'O_p^'(H)]]].

End Ptypes.

CoInductive exists_typeP (spec : U W W1 W2, W1 \x W2 = WProp) : Prop
  := FTtypeP_Spec (U W W1 W2 : {group gT}) defW of spec U W W1 W2 defW.

Definition FTtype_spec i M :=
  match i with
  | 1%N U : {group gT}, of_typeI M U
  | 2 ⇒ exists_typeP (of_typeII M)
  | 3 ⇒ exists_typeP (of_typeIII M)
  | 4 ⇒ exists_typeP (of_typeIV M)
  | 5 ⇒ exists_typeP (of_typeV M)
  | _False
  end.

Definition FTtype M :=
  if \kappa(M)^'.-group M then 1%N else
  if M`_\sigma != M^`(1) then 2 else
  if M`_\F == M`_\sigma then 5 else
  if abelian (M`_\sigma / M`_\F) then 3 else 4.

Lemma FTtype_range M : 0 < FTtype M 5.

Definition FTcore M := if 0 < FTtype M 2 then M`_\F else M^`(1).
Fact FTcore_is_group M : group_set (FTcore M).
Canonical Structure FTcore_group M := Group (FTcore_is_group M).

Definition FTsupport1 M := (FTcore M)^#.

Let FTder M := M^`(FTtype M != 1%N).

Definition FTsupport M := \bigcup_(x in FTsupport1 M) 'C_(FTder M)[x]^#.

Definition FTsupport0 M (pi := \pi(FTder M)) :=
  FTsupport M :|: [set x in M | ~~ pi.-elt x & ~~ pi^'.-elt x].

Definition mmax_transversal U := orbit_transversal 'JG U 'M.

End Definitions.

Notation "M `_ \s" := (FTcore M) (at level 3, format "M `_ \s") : group_scope.
Notation "M `_ \s" := (FTcore_group M) : Group_scope.

Notation "''A1' ( M )" := (FTsupport1 M)
  (at level 8, format "''A1' ( M )") : group_scope.

Notation "''A' ( M )" := (FTsupport M)
  (at level 8, format "''A' ( M )") : group_scope.

Notation "''A0' ( M )" := (FTsupport0 M)
  (at level 8, format "''A0' ( M )") : group_scope.

Notation "''M^' G" := (mmax_transversal G)
  (at level 3, format "''M^' G") : group_scope.

Section Section16.

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

Structural properties of the M`_\s definition.
This section covers the characterization of the F, P, P1 and P2 types of maximal subgroups summarized at the top of p. 125. in B & G.
Section KappaClassification.

Variables M U K : {group gT}.
Hypotheses (maxM : M \in 'M) (complU : kappa_complement M U K).

Remark trivgFmax : (M \in 'M_'F) = (K :==: 1).

Remark trivgPmax : (M \in 'M_'P) = (K :!=: 1).

Remark FmaxP : reflect (K :==: 1 U :!=: 1) (M \in 'M_'F).

Remark P1maxP : reflect (K :!=: 1 U :==: 1) (M \in 'M_'P1).

Remark P2maxP : reflect (K :!=: 1 U :!=: 1) (M \in 'M_'P2).

End KappaClassification.

This section covers the combinatorial statements of B & G, Lemma 16.1. It needs to appear before summary theorems A-E because we are following Peterfalvi in anticipating the classification in the definition of the kernel sets A1(M), A(M) and A0(M). The actual correspondence between the combinatorial classification and the mathematical description, i.e., the of_typeXX predicates, will be given later.
Section FTtypeClassification.

Variable M : {group gT}.
Hypothesis maxM : M \in 'M.

Lemma kappa_witness :
   UK : {group gT} × {group gT}, kappa_complement M UK.1 UK.2.

This is B & G, Lemma 16.1(a).
Lemma FTtype_Fmax : (M \in 'M_'F) = (FTtype M == 1%N).

Lemma FTtype_Pmax : (M \in 'M_'P) = (FTtype M != 1%N).

This is B & G, Lemma 16.1(b).
This covers the P1 part of B & G, Lemma 16.1 (c) and (d).
Other relations between the 'core' groups.
This is B & G, Lemma 16.1(f).
Lemma Fcore_eq_FTcore : reflect (M`_\F = M`_\s) (FTtype M \in pred3 1%N 2 5).

This is the second part of B & G, Lemma 16.1(c).
Internal automorphism.
Lemma FTtypeJ M x : FTtype (M :^ x) = FTtype M.

Lemma FTcoreJ M x : (M :^ x)`_\s = M`_\s :^ x.

Lemma FTsupp1J M x : 'A1(M :^ x) = 'A1(M) :^ x.

Lemma FTsuppJ M x : 'A(M :^ x) = 'A(M) :^ x.

Lemma FTsupp0J M x : 'A0(M :^ x) = 'A0(M) :^ x.

Inclusion/normality of class function supports.
Support inclusions that depend on the maximality of M.

Variable M : {group gT}.
Hypothesis maxM : M \in 'M.

Lemma FTsupp1_sub : 'A1(M) \subset 'A(M).

Lemma FTsupp1_sub0 : 'A1(M) \subset 'A0(M).

Lemma FTsupp1_neq0 : 'A1(M) != set0.

Lemma FTsupp_neq0 : 'A(M) != set0.

Lemma FTsupp0_neq0 : 'A0(M) != set0.

Lemma Fcore_sub_FTsupp1 : M`_\F^# \subset 'A1(M).

Lemma Fcore_sub_FTsupp : M`_\F^# \subset 'A(M).

Lemma Fcore_sub_FTsupp0 : M`_\F^# \subset 'A0(M).

Lemma Fitting_sub_FTsupp : 'F(M)^# \subset 'A(M).

Lemma Fitting_sub_FTsupp0 : 'F(M)^# \subset 'A0(M).

Lemma FTsupp_eq1 : (2 < FTtype M)%N'A(M) = 'A1(M).

End MmaxFTsupp.

Section SingleGroupSummaries.

Variables M U K : {group gT}.
Hypotheses (maxM : M \in 'M) (complU : kappa_complement M U K).

Let Kstar := 'C_(M`_\sigma)(K).

Theorem BGsummaryA :
 [/\ (*1*) [/\ M`_\sigma <| M, \sigma(M).-Hall(M) M`_\sigma &
               \sigma(M).-Hall(G) M`_\sigma],
     (*2*) \kappa(M).-Hall(M) K cyclic K,
     (*3*) [/\ U \in [complements to M`_\sigma <*> K in M],
               K \subset 'N(U),
               M`_\sigma <*> U <| M,
               U <| U <*> K
             & M`_\sigma × U × K = M],
     (*4*) {in K^#, k, 'C_U[k] = 1}
  &
 [/\ (*5*) Kstar != 1 {in K^#, k, K \x Kstar = 'C_M[k]},
     (*6*) [/\ M`_\F != 1, M`_\F \subset M`_\sigma, M`_\sigma \subset M^`(1),
               M^`(1) \proper M & nilpotent (M^`(1) / M`_\F)],
     (*7*) [/\ M^`(2) \subset 'F(M), M`_\F × 'C_M(M`_\F) = 'F(M)
             & K :!=: 1 → 'F(M) \subset M^`(1)]
   & (*8*) M`_\F != M`_\sigma
           [/\ U :=: 1, normedTI 'F(M)^# G M & prime #|K| ]]].

This is a variant of B & G, Lemma 16.1(e) that better fits the Peterfalvi definitions.
Lemma sdprod_FTder : M`_\sigma ><| U = M^`(FTtype M != 1%N).

Theorem BGsummaryB :
 [/\ (*1*) p S, p.-Sylow(U) Sabelian S 'r(S) 2,
     (*2*) abelian <<U :&: 'A(M)>>,
     (*3*) U0 : {group gT},
           [/\ U0 \subset U, exponent U0 = exponent U & [disjoint U0 & 'A(M)]]
& (*4*) ( X, X \subset UX :!=: 1 → 'C_(M`_\sigma)(X) != 1 →
            'M('C(X)) = [set M])
   (*5*) ('A(M) != 'A1(M)normedTI ('A(M) :\: 'A1(M)) G M)].

Let Z := K <*> Kstar.
Let Zhat := Z :\: (K :|: Kstar).

We strengthened the uniqueness condition in part (4) to 'M_\sigma(K) = [set Mstar].
Theorem BGsummaryC : K :!=: 1 →
 [/\
  [/\ (*1*) abelian U ~~ ('N(U) \subset M),
      (*2*) [/\ cyclic Kstar, Kstar != 1, Kstar \subset M`_\F & ~~ cyclic M`_\F]
    & (*3*) M`_\sigma ><| U = M^`(1) Kstar \subset M^`(2)],
   Mstar,
  [/\ (*4*) [/\ Mstar \in 'M_'P, 'C_(Mstar`_\sigma)(Kstar) = K,
                \kappa(Mstar).-Hall(Mstar) Kstar
              & 'M_\sigma(K) = [set Mstar]], (* uniqueness *)
      (*5*) {in 'E^1(Kstar), X, 'M('C(X)) = [set M]}
          {in 'E^1(K), Y, 'M('C(Y)) = [set Mstar]},
      (*6*) [/\ M :&: Mstar = Z, K \x Kstar = Z & cyclic Z]
    & (*7*) (M \in 'M_'P2 Mstar \in 'M_'P2)
          {in 'M_'P, H, gval H \in M :^: G :|: Mstar :^: G}]
& [/\ (*8*) normedTI Zhat G Z,
      (*9*) let B := 'A0(M) :\: 'A(M) in
            B = class_support Zhat M normedTI B G M,
     (*10*) U :!=: 1 →
            [/\ prime #|K|, normedTI 'F(M)^# G M & M`_\sigma \subset 'F(M)]
   & (*11*) U :==: 1 → prime #|Kstar| ]].

End SingleGroupSummaries.

Theorem BGsummaryD M : M \in 'M
 [/\ (*1*) {in M`_\sigma &, x y, y \in x ^: Gy \in x ^: M},
     (*2*) g (Ms := M`_\sigma), g \notin M
           Ms:&: M :^ g = Ms :&: Ms :^ g cyclic (Ms :&: M :^ g),
     (*3*) {in M`_\sigma^#, x,
            [/\ Hall 'C[x] 'C_M[x], 'R[x] ><| 'C_M[x] = 'C[x]
              & let MGx := [set Mg in M :^: G | x \in Mg] in
                [transitive 'R[x], on MGx | 'Js] #|'R[x]| = #|MGx| ]}
   & (*4*) {in M`_\sigma^#, x (N := 'N[x]), ~~ ('C[x] \subset M)
           [/\ 'M('C[x]) = [set N] N`_\F = N`_\sigma,
               x \in 'A(N) :\: 'A1(N) N \in 'M_'F :|: 'M_'P2,
               \sigma(N)^'.-Hall(N) (M :&: N)
             & N \in 'M_'P2
               [/\ M \in 'M_'F,
                   exists2 E, [Frobenius M = M`_\sigma ><| gval E] & cyclic E
                 & ~~ normedTI (M`_\F)^# G M]]}].

Lemma mmax_transversalP :
  [/\ 'M^G \subset 'M, is_transversal 'M^G (orbit 'JG G @: 'M) 'M,
      {in 'M^G &, injective (fun MM :^: G)}
    & {in 'M, M, x, (M :^ x)%G \in 'M^G}].

We are conforming to the statement of B & G, but we defer the introduction of 'M^G to Peterfalvi (8.17), which requires several other changes.
Theorem BGsummaryE :
  [/\ (*1*) M, M \in 'M
            #|class_support M^~~ G| = (#|M`_\sigma|.-1 × #|G : M|)%N,
      (*2*) {in \pi(G), p,
             exists2 M : {group gT}, M \in 'M & p \in \sigma(M)}
          {in 'M &, M H,
             gval H \notin M :^: G[predI \sigma(M) & \sigma(H)] =i pred0}
    & (*3*) let PG := [set class_support M^~~ G | M : {group gT} in 'M] in
            [/\ partition PG (cover PG),
                'M_'P = set0 :> {set {group gT}}cover PG = G^#
              & M K, M \in 'M_'P\kappa(M).-Hall(M) K
                let Kstar := 'C_(M`_\sigma)(K) in
                let Zhat := (K <*> Kstar) :\: (K :|: Kstar) in
                partition [set class_support Zhat G; cover PG] G^#]].

Let typePfacts M (H := M`_\F) U W1 W2 W (defW : W1 \x W2 = W) :
     M \in 'Mof_typeP M U defW
  [/\ M \in 'M_'P, \kappa(M).-Hall(M) W1, 'C_H(W1) = W2,
     (M \in 'M_'P1) = (U :==: 1) || ('N(U) \subset M)
    & let Ms := M`_\sigma in
      Ms = M^`(1)(H == Ms) = (U :==: 1) abelian (Ms / H) = abelian U].

This is B & G, Lemma 16.1.
Lemma FTtypeP i M : M \in 'Mreflect (FTtype_spec i M) (FTtype M == i).

This is B & G, Theorem I. Note that the first assertion is not used in the Perterfalvi revision of the character theory part of the proof.
Theorem BGsummaryI :
  [/\ H x a, Hall G Hnilpotent Hx \in Hx ^ a \in H
      exists2 y, y \in 'N(H) & x ^ a = x ^ y
    & {in 'M, M, FTtype M == 1%N}
     ST : {group gT} × {group gT}, let (S, T) := ST in
      [/\ S \in 'M T \in 'M,
           Wi : {group gT} × {group gT}, let (W1, W2) := Wi in
          let W := W1 <*> W2 in let V := W :\: (W1 :|: W2) in
         (*a*) [/\ cyclic W, normedTI V G W & W1 :!=: 1 W2 :!=: 1]
         (*b*) [/\ S^`(1) ><| W1 = S, T^`(1) ><| W2 = T & S :&: T = W],
     (*c*) {in 'M, M, FTtype M != 1%N
             x, S :^ x = M T :^ x = M},
     (*d*) FTtype S == 2 FTtype T == 2
   & (*e*) 1 < FTtype S 5 1 < FTtype T 5]].

Lemma FTsupp0_type1 M : FTtype M == 1%N'A0(M) = 'A(M).

Lemma FTsupp0_typeP M (H := M`_\F) U W1 W2 W (defW : W1 \x W2 = W) :
    M \in 'Mof_typeP M U defW
  let V := W :\: (W1 :|: W2) in 'A0(M) :\: 'A(M) = class_support V M.

This is the part of B & G, Theorem II that is relevant to the proof of Peterfalvi (8.7). We drop the considerations on the set of supporting groups, in particular (Tii)(a), but do include additional information on D namely the fact that D is included in 'A1(M), not just 'A(M).
Theorem BGsummaryII M (X : {set gT}) :
    M \in 'MX \in pred2 'A(M) 'A0(M)
    let D := [set x in X | ~~ ('C[x] \subset M)] in
 [/\ D \subset 'A1(M), (* was 'A(M) in B & G *)
     (*i*) {in X, x a, x ^ a \in Xexists2 y, y \in M & x ^ a = x ^ y}
  & {in D, x (L := 'N[x]),
 [/\ (*ii*) 'M('C[x]) = [set L], FTtype L \in pred2 1%N 2,
     [/\ (*b*) L`_\F ><| (M :&: L) = L,
         (*c*) {in X, y, coprime #|L`_\F| #|'C_M[y]| },
         (*d*) x \in 'A(L) :\: 'A1(L)
       & (*e*) 'C_(L`_\F)[x] ><| 'C_M[x] = 'C[x]]
& (*iii*) FTtype L == 2 →
             exists2 E, [Frobenius M = M`_\F ><| gval E] & cyclic E]}].

End Section16.