(Joint Center)Library BGsection7

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
Require Import finset prime fingroup morphism automorphism action quotient.
Require Import gfunctor cyclic pgroup center commutator gseries nilpotent.
Require Import sylow abelian maximal hall.
Require Import BGsection1 BGsection6.

This file covers B & G, section 7, i.e., the proof of the Thompson Transitivity Theorem, as well as some generalisations used later in the proof. This is the first section of the proof that applies to a (hypothetical) minimally simple odd group, so we also introduce at this point some infrastructure to carry over this assumption into the rest of the proof. minSimpleOddGroupType == a finGroupType that ranges exactly over the elements of a minimal counter-example to the Odd Order Theorem. G == the group of all the elements in a minSimpleOddGroupType (this is a local notation that must be reestablished for each such Type). 'M == the set of all (proper) maximal subgroups of G 'M(H) == the set of all elements of 'M that contain H 'U == the set of all H such that 'M(H) contains a single (unique) maximal subgroup of G. 'SCN_n[p] == the set of all SCN subgroups of rank at least n of all the Sylow p-subgroups of G. |/|_H(A, pi) == the set of all pi-subgroups of H that are normalised by A. |/|*(A, pi) == the set of pi-subgroups of G, normalised by A, and maximal subject to this condition. normed_constrained A == A is a nontrivial proper subgroup of G, such that for any proper subgroup X containing A, all Y in |/|_X(A, pi') lie in the pi'-core of X (here pi is the set of prime divisors of #|A|). This is Hypothesis 7.1 in B & G.

Set Implicit Arguments.

Import GroupScope.

Reserved Notation "''M'" (at level 8, format "''M'").
Reserved Notation "''M' ( H )" (at level 8, format "''M' ( H )").
Reserved Notation "''U'" (at level 8).
Reserved Notation "''SCN_' n [ p ]"
  (at level 8, n at level 2, format "''SCN_' n [ p ]").
Reserved Notation "|/|_ X ( A ; pi )"
  (at level 8, X at level 2, format "|/|_ X ( A ; pi )").
Reserved Notation "|/|* ( A ; pi )"
  (at level 8, format "|/|* ( A ; pi )").

The generic setup for the whole Odd Order Theorem proof.
Elementary properties of the minimal counter example.
Section MinSimpleOdd.

Variable gT : minSimpleOddGroupType.
Notation G := (TheMinSimpleOddGroup gT).
Implicit Types H K D M P U V X : {group gT}.
Local Notation sT := {set gT}.
Implicit Type p : nat.

Lemma mFT_odd H : odd #|H|.

Lemma mFT_simple : simple G.

Lemma mFT_nonSolvable : ~~ solvable G.

Lemma mFT_sol M : M \proper Gsolvable M.

Lemma mFT_nonAbelian : ~~ abelian G.

Lemma mFT_neq1 : G != 1.

Lemma mFT_gt1 : [1] \proper G.

Lemma mFT_quo_odd M H : odd #|M / H|.

Lemma mFT_sol_proper M : (M \proper G) = solvable M.

Lemma mFT_pgroup_proper p P : p.-group PP \proper G.

Lemma mFT_norm_proper H : H :!=: 1 → H \proper G'N(H) \proper G.

Lemma cent_mFT_trivial : 'C(G) = 1.

Lemma mFT_cent_proper H : H :!=: 1 → 'C(H) \proper G.

Lemma mFT_cent1_proper x : x != 1 → 'C[x] \proper G.

Lemma mFT_quo_sol M H : H :!=: 1 → solvable (M / H).

Maximal groups of the minimal FT counterexample, as defined at the start of B & G, section 7.
Definition minSimple_max_groups := [set M : {group gT} | maximal M G].
Local Notation "'M" := minSimple_max_groups : group_scope.

Definition minSimple_max_groups_of (H : sT) := [set M in 'M | H \subset M].
Local Notation "''M' ( H )" := (minSimple_max_groups_of H) : group_scope.

Definition minSimple_uniq_max_groups := [set U : {group gT} | #|'M(U)| == 1%N].
Local Notation "'U" := minSimple_uniq_max_groups : group_scope.

Definition minSimple_SCN_at n p := \bigcup_(P in 'Syl_p(G)) 'SCN_n(P).

Lemma mmax_exists H : H \proper G{M | M \in 'M(H)}.

Lemma any_mmax : {M : {group gT} | M \in 'M}.

Lemma mmax_proper M : M \in 'MM \proper G.

Lemma mmax_sol M : M \in 'Msolvable M.

Lemma mmax_max M H : M \in 'MH \proper GM \subset HH :=: M.

Lemma eq_mmax : {in 'M &, M H, M \subset HM :=: H}.

Lemma sub_mmax_proper M H : M \in 'MH \subset MH \proper G.

Lemma mmax_norm X M :
  M \in 'MX :!=: 1 → X \proper GM \subset 'N(X)'N(X) = M.

Lemma mmax_normal_subset A M :
  M \in 'MA <| M~~ (A \subset [1])'N(A) = M.

Lemma mmax_normal M H : M \in 'MH <| MH :!=: 1 → 'N(H) = M.

Lemma mmax_sigma_Sylow p P M :
  M \in 'Mp.-Sylow(M) P'N(P) \subset Mp.-Sylow(G) P.

Lemma mmax_neq1 M : M \in 'MM :!=: 1.

Lemma norm_mmax M : M \in 'M'N(M) = M.

Lemma mmaxJ M x : (M :^ x \in 'M)%G = (M \in 'M).

Lemma mmax_ofS H K : H \subset K'M(K) \subset 'M(H).

Lemma mmax_ofJ K x M : ((M :^ x)%G \in 'M(K :^ x)) = (M \in 'M(K)).

Lemma uniq_mmaxP U : reflect ( M, 'M(U) = [set M]) (U \in 'U).
Implicit Arguments uniq_mmaxP [U].

Lemma mem_uniq_mmax U M : 'M(U) = [set M]M \in 'M U \subset M.

Lemma eq_uniq_mmax U M H :
  'M(U) = [set M]H \in 'MU \subset HH :=: M.

Lemma def_uniq_mmax U M :
  U \in 'UM \in 'MU \subset M'M(U) = [set M].

Lemma uniq_mmax_subset1 U M :
  M \in 'MU \subset M(U \in 'U) = ('M(U) \subset [set M]).

Lemma sub_uniq_mmax U M H :
  'M(U) = [set M]U \subset HH \proper GH \subset M.

Lemma mmax_sup_id M : M \in 'M'M(M) = [set M].

Lemma mmax_uniq_id : {subset 'M 'U}.

Lemma def_uniq_mmaxJ M K x : 'M(K) = [set M]'M(K :^ x) = [set M :^ x]%G.

Lemma uniq_mmaxJ K x :((K :^ x)%G \in 'U) = (K \in 'U).

Lemma uniq_mmax_norm_sub (M U : {group gT}) :
  'M(U) = [set M]'N(U) \subset M.

Lemma uniq_mmax_neq1 (U : {group gT}) : U \in 'UU :!=: 1.

Lemma def_uniq_mmaxS M U V :
  U \subset VV \proper G'M(U) = [set M]'M(V) = [set M].

Lemma uniq_mmaxS U V : U \subset VV \proper GU \in 'UV \in 'U.

End MinSimpleOdd.

Implicit Arguments uniq_mmaxP [gT U].

Notation "''M'" := (minSimple_max_groups _) : group_scope.
Notation "''M' ( H )" := (minSimple_max_groups_of H) : group_scope.
Notation "''U'" := (minSimple_uniq_max_groups _) : group_scope.
Notation "''SCN_' n [ p ]" := (minSimple_SCN_at _ n p) : group_scope.

Section Hypothesis7_1.

Variable gT : finGroupType.
Implicit Types X Y A P Q : {group gT}.
Local Notation G := [set: gT].

Definition normed_pgroups (X A : {set gT}) pi :=
  [set Y : {group gT} | pi.-subgroup(X) Y & A \subset 'N(Y)].
Local Notation "|/|_ X ( A ; pi )" := (normed_pgroups X A pi) : group_scope.

Definition max_normed_pgroups (A : {set gT}) pi :=
  [set Y : {group gT} | [max Y | pi.-group Y & A \subset 'N(Y)]].
Local Notation "|/|* ( A ; pi )" := (max_normed_pgroups A pi) : group_scope.

This is the statement for B & G, Hypothesis 7.1.
Inductive normed_constrained (A : {set gT}) :=
  NormedConstrained (pi := \pi(A)) of A != 1 & A \proper G
  & X Y : {group gT},
    A \subset XX \proper GY \in |/|_X(A; pi^')Y \subset 'O_pi^'(X).

Variable pi : nat_pred.

Lemma max_normed_exists A X :
  pi.-group XA \subset 'N(X){Y | Y \in |/|*(A; pi) & X \subset Y}.

Lemma mem_max_normed A X : X \in |/|*(A; pi)pi.-group X A \subset 'N(X).

Lemma norm_acts_max_norm P : [acts 'N(P), on |/|*(P; pi) | 'JG].

Lemma trivg_max_norm P : 1%G \in |/|*(P; pi)|/|*(P; pi) = [set 1%G].

Lemma max_normed_uniq A P Q :
    |/|*(A; pi) = [set Q]A \subset PP \subset 'N(Q)
  |/|*(P; pi) = [set Q].

End Hypothesis7_1.

Notation "|/|_ X ( A ; pi )" := (normed_pgroups X A pi) : group_scope.
Notation "|/|* ( A ; pi )" := (max_normed_pgroups A pi) : group_scope.

Section Seven.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Local Notation grT := {group gT}.
Implicit Types H P Q R K M A B : grT.
Implicit Type p q : nat.

Section NormedConstrained.

Variables (q : nat) (A : grT).
Let pi := Eval simpl in \pi(A).
Let K := 'O_pi^'('C(A)).
Let nsKC : K <| 'C(A) := pcore_normal _ _.

Lemma cent_core_acts_max_norm : [acts K, on |/|*(A; q) | 'JG].
Let actsKmax := actsP cent_core_acts_max_norm.

Hypotheses (cstrA : normed_constrained A) (pi'q : q \notin pi).

Let hyp71 H R :
  A \subset HH \proper GR \in |/|_H(A; pi^')R \subset 'O_pi^'(H).

This is the observation between B & G, Hypothesis 7.1 and Lemma 7.1.
This is B & G, Lemma 7.1.
Lemma normed_constrained_meet_trans Q1 Q2 H :
    A \subset HH \proper GQ1 \in |/|*(A; q)Q2 \in |/|*(A; q)
    Q1 :&: H != 1 → Q2 :&: H != 1 →
  exists2 k, k \in K & Q2 :=: Q1 :^ k.

This is B & G, Theorem 7.2.
This is B & G, Theorem 7.3.
This is B & G, Theorem 7.4.
Theorem normed_trans_superset P :
    A <|<| Ppi.-group P[transitive K, on |/|*(A; q) | 'JG]
 [/\ 'C_K(P) = 'O_pi^'('C(P)),
     [transitive 'O_pi^'('C(P)), on |/|*(P; q) | 'JG],
     |/|*(P; q) \subset |/|*(A; q)
   & {in |/|*(P; q), Q, P :&: 'N(P)^`(1) \subset 'N(Q)^`(1)
                             'N(P) = 'C_K(P) × 'N_('N(P))(Q)}].

End NormedConstrained.

This is B & G, Proposition 7.5(a). As this is only used in Proposition 10.10, under the assumption A \in E*_p(G), we avoid the in_pmaxElemE detour A = [set x in 'C_G(A) | x ^+ p == 1], and just use A \in E*_p(G).
Proposition plength_1_normed_constrained p A :
    A :!=: 1 → A \in 'E×_p(G) → ( M, M \proper Gp.-length_1 M) →
  normed_constrained A.

This is B & G, Proposition 7.5(b).
Proposition SCN_normed_constrained p P A :
  p.-Sylow(G) PA \in 'SCN_2(P)normed_constrained A.

This is B & G, Theorem 7.6 (the Thompson Transitivity Theorem).
Theorem Thompson_transitivity p q A :
    A \in 'SCN_3[p]q \in p^'
  [transitive 'O_p^'('C(A)), on |/|*(A; q) | 'JG].

End Seven.