# Library BGsection11

(* (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.
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
Require Import BGsection7 BGsection10.

This file covers B & G, section 11; it has only one definition: exceptional_FTmaximal p M A0 A <=> p, M and A0 satisfy the conditions of Hypothesis 11.1 in B & G, i.e., M is an "exceptional" maximal subgroup in the terminology of B & G. In addition, A is elementary abelian p-subgroup of M of rank 2, that contains A0. The existence of A is guaranteed by Lemma 10.5, but as in the only two lemmas that make use of the results in this section (Lemma 12.3 and Theorem 12.5) A is known, we elected to make the dependency on A explicit.

Set Implicit Arguments.

Import GroupScope.

Section Section11.

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

Implicit Types p q r : nat.
Implicit Types A E H K M N P Q R S T U V W X Y : {group gT}.

Variables (p : nat) (M A0 A P : {group gT}).

This definition corresponsd to Hypothesis 11.1, where the condition on A has been made explicit.
Definition exceptional_FTmaximal :=
[/\ p \in \sigma(M)^', A \in 'E_p^2(M), A0 \in 'E_p^1(A) & 'N(A0) \subset M].

Hypotheses (maxM : M \in 'M) (excM : exceptional_FTmaximal).
Hypotheses (sylP : p.-Sylow(M) P) (sAP : A \subset P).

Splitting the excM hypothesis.
Let sM'p : p \in \sigma(M)^'.
Let Ep2A : A \in 'E_p^2(M).
Let Ep1A0 : A0 \in 'E_p^1(A).
Let sNA0_M : 'N(A0) \subset M.

Arithmetics of p.
Let p_pr : prime p := pnElem_prime Ep2A.
Let p_gt1 : p > 1 := prime_gt1 p_pr.
Let p_gt0 : p > 0 := prime_gt0 p_pr.

Group orders.
Let oA : #|A| = (p ^ 2)%N := card_pnElem Ep2A.
Let oA0 : #|A0| = p := card_pnElem Ep1A0.

Structure of A.
Various set inclusions.
Alternative E_p^1 memberships for A0; the first is the one used to state Hypothesis 11.1 in B & G, the second is the form expected by Lemma 10.5. Note that #|A0| = p (oA0 above) would wokr just as well.
This does not depend on exceptionalM, and could move to Section 10.
First preliminary remark of Section 11; only depends on sM'p and sylP.
Second preliminary remark of Section 11; only depends on sM'p, Ep1A0_M, and sNA0_M.
Third preliminary remark of Section 11.
This is B & G, Lemma 11.1.
Lemma exceptional_TIsigmaJ g q Q1 Q2 :
g \notin MA \subset M :^ g
q.-Sylow(M_\sigma) Q1A \subset 'N(Q1)
q.-Sylow(M_\sigma :^ g) Q2A \subset 'N(Q2)
(*a*) Q1 :&: Q2 = 1
(*b*) ( X, X \in 'E_p^1(A)'C_Q1(X) = 1 'C_Q2(X) = 1).

This is B & G, Corollary 11.2.
Corollary exceptional_TI_MsigmaJ g :
g \notin MA \subset M :^ g
(*a*) M_\sigma :&: M :^ g = 1
(*b*) M_\sigma :&: 'C(A0 :^ g) = 1.

This is B & G, Theorem 11.3.
This is B & G, Corollary 11.4.
Corollary exceptional_sigma_uniq H :
H \in 'M(A)H_\sigma :&: M _\sigma != 1 → H :=: M.

This is B & G, Theorem 11.5.
This is B & G, Corollary 11.6.
Corollary exceptional_structure (Ms := M`_\sigma) :
[/\ (*a*) A :=: 'Ohm_1(P),
(*b*) 'C_Ms(A) = 1
& (*c*) exists2 A1, A1 \in 'E_p^1(A) & exists2 A2, A2 \in 'E_p^1(A) &
[/\ A1 :!=: A2, 'C_Ms(A1) = 1 & 'C_Ms(A2) = 1]].

This is B & G, Theorem 11.7 (the main result on exceptional subgroups).