(Joint Center)Library BGsection9

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

This file covers B & G, section 9, i.e., the proof the Uniqueness Theorem, along with the several variants and auxiliary results. Note that this is the only file to import BGsection8.

Set Implicit Arguments.

Import GroupScope.

Section Nine.

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

This is B & G, Theorem 9.1(b).
Theorem noncyclic_normed_sub_Uniqueness p M B :
    M \in 'MB \in 'E_p(M)~~ cyclic B
    \bigcup_(K in |/|_G(B; p^')) K \subset M
  B \in 'U.

This is B & G, Theorem 9.1(a).
Theorem noncyclic_cent1_sub_Uniqueness p M B :
    M \in 'MB \in 'E_p(M)~~ cyclic B
    \bigcup_(b in B^#) 'C[b] \subset M
  B \in 'U.

This is B & G, Corollary 9.2.
Corollary cent_uniq_Uniqueness K L :
  L \in 'UK \subset 'C(L)'r(K) 2 → K \in 'U.

This is B & G, Corollary 9.3.
Corollary any_cent_rank3_Uniquness p A B :
    abelian Ap.-group A'r(A) 3 → A \in 'U
    p.-group B~~ cyclic B'r_p('C(B)) 3 →
  B \in 'U.

This is B & G, Lemma 9.4.
Lemma any_rank3_Fitting_Uniqueness p M P :
  M \in 'M'r_p('F(M)) 3 → p.-group P'r(P) 3 → P \in 'U.

This is B & G, Lemma 9.5.
Lemma SCN_3_Uniqueness p A : A \in 'SCN_3[p]A \in 'U.

This is B & G, Theorem 9.6, first assertion; note that B & G omit the (necessary!) condition K \proper G.
Theorem rank3_Uniqueness K : K \proper G'r(K) 3 → K \in 'U.

This is B & G, Theorem 9.6, second assertion
Theorem cent_rank3_Uniqueness K : 'r(K) 2 → 'r('C(K)) 3 → K \in 'U.

This is B & G, Theorem 9.6, final observation
Theorem nonmaxElem2_Uniqueness p A : A \in 'E_p^2(G) :\: 'E×_p(G)A \in 'U.

End Nine.