(Joint Center)Library BGsection8

(* (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 automorphism action gproduct gfunctor.
Require Import center commutator pgroup gseries nilpotent sylow abelian maximal.
Require Import BGsection1 BGsection5 BGsection6 BGsection7.

This file covers B & G, section 8, i.e., the proof of two special cases of the Uniqueness Theorem, for maximal groups with Fitting subgroups of rank at least 3.

Set Implicit Arguments.

Import GroupScope.

Section Eight.

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

Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)
  (at level 8, q at level 2, format "K ` p") : group_scope.
Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)%G : Group_scope.

This is B & G, Theorem 8.1(a).
Theorem non_pcore_Fitting_Uniqueness p M A0 :
    M \in 'M~~ p.-group ('F(M)) → A0 \in 'E×_p('F(M))'r_p(A0) 3 →
  'C_('F(M))(A0)%G \in 'U.

This is B & G, Theorem 8.1(b).
Theorem SCN_Fitting_Uniqueness p M P A :
    M \in 'Mp.-group ('F(M)) → p.-Sylow(M) P
    'r_p('F(M)) 3 → A \in 'SCN_3(P)
  [/\ p.-Sylow(G) P, A \subset 'F(M) & A \in 'U].

This summarizes the two branches of B & G, Theorem 8.1.
Theorem Fitting_Uniqueness M : M \in 'M'r('F(M)) 3 → 'F(M)%G \in 'U.

End Eight.