(Joint Center)Library BGsection6

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

This file covers most of B & G section 6. Theorem 6.4 is not proved, since it is not needed for the revised proof of the odd order theorem.

Set Implicit Arguments.

Import GroupScope.

Section Six.

Implicit Type gT : finGroupType.
Implicit Type p : nat.

Section OneType.

Variable gT : finGroupType.
Implicit Types G H K S U : {group gT}.

This is B & G, Theorem A.4(b) and 6.1, or Gorenstein 6.5.2, the main Hall- Higman style p-stability result used in the proof of the Odd Order Theorem
Auxiliary results from AppendixAB, necessary to exploit the results below.
The two parts of B & G, Theorem 6.2 are established in BGappendixAB.
This is the main statement of B & G, Theorem 6.2. It is not used in the actual proof.
This is the second part (special case) of B & G, Theorem 6.2.
Theorem Puig_center_normal p G S :
  odd #|G|solvable Gp.-Sylow(G) S'O_p^'(G) = 1 → 'Z('L(S)) <| G.

This is B & G, Lemma 6.3(a).
Lemma coprime_der1_sdprod K H G :
    K ><| H = Gcoprime #|K| #|H|solvable KK \subset G^`(1)
  [~: K, H] = K 'C_K(H) \subset K^`(1).

This is B & G, Lemma 6.3(b). It is apparently not used later.
Lemma prime_nil_der1_factor G :
    nilpotent G^`(1)prime #|G / G^`(1)|
  Hall G G^`(1) ( H, G^`(1) ><| H = GG^`(1) = [~: G, H]).

Section PprodSubCoprime.

Variables K U H G : {group gT}.
Hypotheses (defG : K × U = G) (nsKG : K <| G).
Hypotheses (sHU : H \subset U) (coKH : coprime #|K| #|H|).
Let nKG : G \subset 'N(K).
Let sKG : K \subset G.
Let sUG : U \subset G.
Let nKU : U \subset 'N(K).
Let nKH : H \subset 'N(K).

This is B & G, Lemma 6.5(a); note that we do not assume solvability.
Lemma pprod_focal_coprime : H :&: G^`(1) = H :&: U^`(1).

Hypothesis solG : solvable G.

This is B & G, Lemma 6.5(c).
Lemma pprod_trans_coprime g :
    g \in GH :^ g \subset U
  exists2 c, c \in 'C_K(H) & exists2 u, u \in U & g = c × u.

This is B & G, Lemma 6.5(b).
Lemma pprod_norm_coprime_prod : 'C_K(H) × 'N_U(H) = 'N_G(H).

End PprodSubCoprime.

Section Plength1Prod.

Variables (p : nat) (G S : {group gT}).
Hypotheses (sylS : p.-Sylow(G) S) (pl1G : p.-length_1 G).
Let K := 'O_p^'(G).
Let sSG : S \subset G.
Let nsKG : K <| G.
Let sKG : K \subset G.
Let nKG : G \subset 'N(K).
Let nKS : S \subset 'N(K).
Let coKS : coprime #|K| #|S|.
Let sSN : S \subset 'N_G(S).

Let sylGbp : p.-Sylow(G / K) 'O_p(G / K).

This is B & G, Lemma 6.6(a1); note that we do not assume solvability.
This is B & G, Lemma 6.6(a2); note that we do not assume solvability.
Lemma plength1_Frattini : K × 'N_G(S) = G.
Local Notation defG := plength1_Frattini.

This is B & G, Lemma 6.6(b); note that we do not assume solvability.
This is B & G, Lemma 6.6(c).
Lemma plength1_Sylow_trans (Y : {set gT}) g :
    Y \subset Sg \in GY :^ g \subset S
  exists2 c, c \in 'C_G(Y) & exists2 u, u \in 'N_G(S) & g = c × u.

This is B & G, Lemma 6.6(d).
Lemma plength1_Sylow_Jsub (Q : {group gT}) :
    Q \subset Gp.-group Q
  exists2 x, x \in 'C_G(Q :&: S) & Q :^ x \subset S.

End Plength1Prod.

End OneType.

This is B & G, Theorem 6.7
Theorem plength1_norm_pmaxElem gT p (G E L : {group gT}) :
    E \in 'E×_p(G)odd psolvable Gp.-length_1 G
    L \subset GE \subset 'N(L)p^'.-group L
  L \subset 'O_p^'(G).

End Six.