Library mathcomp.solvable.maximal
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import div fintype finfun bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism quotient.
From mathcomp Require Import action commutator gproduct gfunctor ssralg.
From mathcomp Require Import finalg zmodp cyclic pgroup center gseries.
From mathcomp Require Import nilpotent sylow abelian finmodule.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import div fintype finfun bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism quotient.
From mathcomp Require Import action commutator gproduct gfunctor ssralg.
From mathcomp Require Import finalg zmodp cyclic pgroup center gseries.
From mathcomp Require Import nilpotent sylow abelian finmodule.
This file establishes basic properties of several important classes of
maximal subgroups: maximal, max and min normal, simple, characteristically
simple subgroups, the Frattini and Fitting subgroups, the Thompson
critical subgroup, special and extra-special groups, and self-centralising
normal (SCN) subgroups. In detail, we define:
charsimple G == G is characteristically simple (it has no nontrivial
characteristic subgroups, and is nontrivial)
'Phi(G) == the Frattini subgroup of G, i.e., the intersection of
all its maximal proper subgroups.
'F(G) == the Fitting subgroup of G, i.e., the largest normal
nilpotent subgroup of G (defined as the (direct)
product of all the p-cores of G).
critical C G == C is a critical subgroup of G: C is characteristic
(but not functorial) in G, the center of C contains
both its Frattini subgroup and the commutator [G, C],
and is equal to the centraliser of C in G. The
Thompson_critical theorem provides critical subgroups
for p-groups; we also show that in this case the
centraliser of C in Aut G is a p-group as well.
special G == G is a special group: its center, Frattini, and
derived sugroups coincide (we follow Aschbacher in
not considering nontrivial elementary abelian groups
as special); we show that a p-group factors under
coprime action into special groups (Aschbacher 24.7).
extraspecial G == G is a special group whose center has prime order
(hence G is non-abelian).
'SCN(G) == the set of self-centralising normal abelian subgroups
of G (the A <| G such that 'C_G(A) = A).
'SCN_n(G) == the subset of 'SCN(G) containing all groups with rank
at least n (i.e., A \in 'SCN(G) and 'm(A) >= n).
Set Implicit Arguments.
Import GroupScope.
Section Defs.
Variable gT : finGroupType.
Implicit Types (A B D : {set gT}) (G : {group gT}).
Definition charsimple A := [min A of G | G :!=: 1 & G \char A].
Definition Frattini A := \bigcap_(G : {group gT} | maximal_eq G A) G.
Canonical Frattini_group A : {group gT} := Eval hnf in [group of Frattini A].
Definition Fitting A := \big[dprod/1]_(p <- primes #|A|) 'O_p(A).
Lemma Fitting_group_set G : group_set (Fitting G).
Canonical Fitting_group G := group (Fitting_group_set G).
Definition critical A B :=
[/\ A \char B,
Frattini A \subset 'Z(A),
[~: B, A] \subset 'Z(A)
& 'C_B(A) = 'Z(A)].
Definition special A := Frattini A = 'Z(A) ∧ A^`(1) = 'Z(A).
Definition extraspecial A := special A ∧ prime #|'Z(A)|.
Definition SCN B := [set A : {group gT} | A <| B & 'C_B(A) == A].
Definition SCN_at n B := [set A in SCN B | n ≤ 'r(A)].
End Defs.
Notation "''Phi' ( A )" := (Frattini A)
(at level 8, format "''Phi' ( A )") : group_scope.
Notation "''Phi' ( G )" := (Frattini_group G) : Group_scope.
Notation "''F' ( G )" := (Fitting G)
(at level 8, format "''F' ( G )") : group_scope.
Notation "''F' ( G )" := (Fitting_group G) : Group_scope.
Notation "''SCN' ( B )" := (SCN B)
(at level 8, format "''SCN' ( B )") : group_scope.
Notation "''SCN_' n ( B )" := (SCN_at n B)
(at level 8, n at level 2, format "''SCN_' n ( B )") : group_scope.
Section PMax.
Variables (gT : finGroupType) (p : nat) (P M : {group gT}).
Hypothesis pP : p.-group P.
Lemma p_maximal_normal : maximal M P → M <| P.
Lemma p_maximal_index : maximal M P → #|P : M| = p.
Lemma p_index_maximal : M \subset P → prime #|P : M| → maximal M P.
End PMax.
Section Frattini.
Variables gT : finGroupType.
Implicit Type G M : {group gT}.
Lemma Phi_sub G : 'Phi(G) \subset G.
Lemma Phi_sub_max G M : maximal M G → 'Phi(G) \subset M.
Lemma Phi_proper G : G :!=: 1 → 'Phi(G) \proper G.
Lemma Phi_nongen G X : 'Phi(G) <*> X = G → <<X>> = G.
Lemma Frattini_continuous (rT : finGroupType) G (f : {morphism G >-> rT}) :
f @* 'Phi(G) \subset 'Phi(f @* G).
End Frattini.
Canonical Frattini_igFun := [igFun by Phi_sub & Frattini_continuous].
Canonical Frattini_gFun := [gFun by Frattini_continuous].
Section Frattini0.
Variable gT : finGroupType.
Implicit Types (rT : finGroupType) (D G : {group gT}).
Lemma Phi_char G : 'Phi(G) \char G.
Lemma Phi_normal G : 'Phi(G) <| G.
Lemma injm_Phi rT D G (f : {morphism D >-> rT}) :
'injm f → G \subset D → f @* 'Phi(G) = 'Phi(f @* G).
Lemma isog_Phi rT G (H : {group rT}) : G \isog H → 'Phi(G) \isog 'Phi(H).
Lemma PhiJ G x : 'Phi(G :^ x) = 'Phi(G) :^ x.
End Frattini0.
Section Frattini2.
Variables gT : finGroupType.
Implicit Type G : {group gT}.
Lemma Phi_quotient_id G : 'Phi (G / 'Phi(G)) = 1.
Lemma Phi_quotient_cyclic G : cyclic (G / 'Phi(G)) → cyclic G.
Variables (p : nat) (P : {group gT}).
Lemma trivg_Phi : p.-group P → ('Phi(P) == 1) = p.-abelem P.
End Frattini2.
Section Frattini3.
Variables (gT : finGroupType) (p : nat) (P : {group gT}).
Hypothesis pP : p.-group P.
Lemma Phi_quotient_abelem : p.-abelem (P / 'Phi(P)).
Lemma Phi_joing : 'Phi(P) = P^`(1) <*> 'Mho^1(P).
Lemma Phi_Mho : abelian P → 'Phi(P) = 'Mho^1(P).
End Frattini3.
Section Frattini4.
Variables (p : nat) (gT : finGroupType).
Implicit Types (rT : finGroupType) (P G H K D : {group gT}).
Lemma PhiS G H : p.-group H → G \subset H → 'Phi(G) \subset 'Phi(H).
Lemma morphim_Phi rT P D (f : {morphism D >-> rT}) :
p.-group P → P \subset D → f @* 'Phi(P) = 'Phi(f @* P).
Lemma quotient_Phi P H :
p.-group P → P \subset 'N(H) → 'Phi(P) / H = 'Phi(P / H).
This is Aschbacher (23.2)
Lemma Phi_min G H :
p.-group G → G \subset 'N(H) → p.-abelem (G / H) → 'Phi(G) \subset H.
Lemma Phi_cprod G H K :
p.-group G → H \* K = G → 'Phi(H) \* 'Phi(K) = 'Phi(G).
Lemma Phi_mulg H K :
p.-group H → p.-group K → K \subset 'C(H) →
'Phi(H × K) = 'Phi(H) × 'Phi(K).
Lemma charsimpleP G :
reflect (G :!=: 1 ∧ ∀ K, K :!=: 1 → K \char G → K :=: G)
(charsimple G).
End Frattini4.
Section Fitting.
Variable gT : finGroupType.
Implicit Types (p : nat) (G H : {group gT}).
Lemma Fitting_normal G : 'F(G) <| G.
Lemma Fitting_sub G : 'F(G) \subset G.
Lemma Fitting_nil G : nilpotent 'F(G).
Lemma Fitting_max G H : H <| G → nilpotent H → H \subset 'F(G).
Lemma pcore_Fitting pi G : 'O_pi('F(G)) \subset 'O_pi(G).
Lemma p_core_Fitting p G : 'O_p('F(G)) = 'O_p(G).
Lemma nilpotent_Fitting G : nilpotent G → 'F(G) = G.
Lemma Fitting_eq_pcore p G : 'O_p^'(G) = 1 → 'F(G) = 'O_p(G).
Lemma FittingEgen G :
'F(G) = <<\bigcup_(p < #|G|.+1 | (p : nat) \in \pi(G)) 'O_p(G)>>.
End Fitting.
Section FittingFun.
Implicit Types gT rT : finGroupType.
Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting).
Lemma FittingS gT (G H : {group gT}) : H \subset G → H :&: 'F(G) \subset 'F(H).
Lemma FittingJ gT (G : {group gT}) x : 'F(G :^ x) = 'F(G) :^ x.
End FittingFun.
Canonical Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting].
Canonical Fitting_gFun := [gFun by morphim_Fitting].
Canonical Fitting_pgFun := [pgFun by morphim_Fitting].
Section IsoFitting.
Variables (gT rT : finGroupType) (G D : {group gT}) (f : {morphism D >-> rT}).
Lemma Fitting_char : 'F(G) \char G.
Lemma injm_Fitting : 'injm f → G \subset D → f @* 'F(G) = 'F(f @* G).
Lemma isog_Fitting (H : {group rT}) : G \isog H → 'F(G) \isog 'F(H).
End IsoFitting.
Section CharSimple.
Variable gT : finGroupType.
Implicit Types (rT : finGroupType) (G H K L : {group gT}) (p : nat).
Lemma minnormal_charsimple G H : minnormal H G → charsimple H.
Lemma maxnormal_charsimple G H L :
G <| L → maxnormal H G L → charsimple (G / H).
Lemma abelem_split_dprod rT p (A B : {group rT}) :
p.-abelem A → B \subset A → ∃ C : {group rT}, B \x C = A.
Lemma p_abelem_split1 rT p (A : {group rT}) x :
p.-abelem A → x \in A →
∃ B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].
Lemma abelem_charsimple p G : p.-abelem G → G :!=: 1 → charsimple G.
Lemma charsimple_dprod G : charsimple G →
∃ H : {group gT}, [/\ H \subset G, simple H
& exists2 I : {set {perm gT}}, I \subset Aut G
& \big[dprod/1]_(f in I) f @: H = G].
Lemma simple_sol_prime G : solvable G → simple G → prime #|G|.
Lemma charsimple_solvable G : charsimple G → solvable G → is_abelem G.
Lemma minnormal_solvable L G H :
minnormal H L → H \subset G → solvable G →
[/\ L \subset 'N(H), H :!=: 1 & is_abelem H].
Lemma solvable_norm_abelem L G :
solvable G → G <| L → G :!=: 1 →
∃ H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].
Lemma trivg_Fitting G : solvable G → ('F(G) == 1) = (G :==: 1).
Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)).
End CharSimple.
Section SolvablePrimeFactor.
Variables (gT : finGroupType) (G : {group gT}).
Lemma index_maxnormal_sol_prime (H : {group gT}) :
solvable G → maxnormal H G G → prime #|G : H|.
Lemma sol_prime_factor_exists :
solvable G → G :!=: 1 → {H : {group gT} | H <| G & prime #|G : H| }.
End SolvablePrimeFactor.
Section Special.
Variables (gT : finGroupType) (p : nat) (A G : {group gT}).
p.-group G → G \subset 'N(H) → p.-abelem (G / H) → 'Phi(G) \subset H.
Lemma Phi_cprod G H K :
p.-group G → H \* K = G → 'Phi(H) \* 'Phi(K) = 'Phi(G).
Lemma Phi_mulg H K :
p.-group H → p.-group K → K \subset 'C(H) →
'Phi(H × K) = 'Phi(H) × 'Phi(K).
Lemma charsimpleP G :
reflect (G :!=: 1 ∧ ∀ K, K :!=: 1 → K \char G → K :=: G)
(charsimple G).
End Frattini4.
Section Fitting.
Variable gT : finGroupType.
Implicit Types (p : nat) (G H : {group gT}).
Lemma Fitting_normal G : 'F(G) <| G.
Lemma Fitting_sub G : 'F(G) \subset G.
Lemma Fitting_nil G : nilpotent 'F(G).
Lemma Fitting_max G H : H <| G → nilpotent H → H \subset 'F(G).
Lemma pcore_Fitting pi G : 'O_pi('F(G)) \subset 'O_pi(G).
Lemma p_core_Fitting p G : 'O_p('F(G)) = 'O_p(G).
Lemma nilpotent_Fitting G : nilpotent G → 'F(G) = G.
Lemma Fitting_eq_pcore p G : 'O_p^'(G) = 1 → 'F(G) = 'O_p(G).
Lemma FittingEgen G :
'F(G) = <<\bigcup_(p < #|G|.+1 | (p : nat) \in \pi(G)) 'O_p(G)>>.
End Fitting.
Section FittingFun.
Implicit Types gT rT : finGroupType.
Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting).
Lemma FittingS gT (G H : {group gT}) : H \subset G → H :&: 'F(G) \subset 'F(H).
Lemma FittingJ gT (G : {group gT}) x : 'F(G :^ x) = 'F(G) :^ x.
End FittingFun.
Canonical Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting].
Canonical Fitting_gFun := [gFun by morphim_Fitting].
Canonical Fitting_pgFun := [pgFun by morphim_Fitting].
Section IsoFitting.
Variables (gT rT : finGroupType) (G D : {group gT}) (f : {morphism D >-> rT}).
Lemma Fitting_char : 'F(G) \char G.
Lemma injm_Fitting : 'injm f → G \subset D → f @* 'F(G) = 'F(f @* G).
Lemma isog_Fitting (H : {group rT}) : G \isog H → 'F(G) \isog 'F(H).
End IsoFitting.
Section CharSimple.
Variable gT : finGroupType.
Implicit Types (rT : finGroupType) (G H K L : {group gT}) (p : nat).
Lemma minnormal_charsimple G H : minnormal H G → charsimple H.
Lemma maxnormal_charsimple G H L :
G <| L → maxnormal H G L → charsimple (G / H).
Lemma abelem_split_dprod rT p (A B : {group rT}) :
p.-abelem A → B \subset A → ∃ C : {group rT}, B \x C = A.
Lemma p_abelem_split1 rT p (A : {group rT}) x :
p.-abelem A → x \in A →
∃ B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].
Lemma abelem_charsimple p G : p.-abelem G → G :!=: 1 → charsimple G.
Lemma charsimple_dprod G : charsimple G →
∃ H : {group gT}, [/\ H \subset G, simple H
& exists2 I : {set {perm gT}}, I \subset Aut G
& \big[dprod/1]_(f in I) f @: H = G].
Lemma simple_sol_prime G : solvable G → simple G → prime #|G|.
Lemma charsimple_solvable G : charsimple G → solvable G → is_abelem G.
Lemma minnormal_solvable L G H :
minnormal H L → H \subset G → solvable G →
[/\ L \subset 'N(H), H :!=: 1 & is_abelem H].
Lemma solvable_norm_abelem L G :
solvable G → G <| L → G :!=: 1 →
∃ H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].
Lemma trivg_Fitting G : solvable G → ('F(G) == 1) = (G :==: 1).
Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)).
End CharSimple.
Section SolvablePrimeFactor.
Variables (gT : finGroupType) (G : {group gT}).
Lemma index_maxnormal_sol_prime (H : {group gT}) :
solvable G → maxnormal H G G → prime #|G : H|.
Lemma sol_prime_factor_exists :
solvable G → G :!=: 1 → {H : {group gT} | H <| G & prime #|G : H| }.
End SolvablePrimeFactor.
Section Special.
Variables (gT : finGroupType) (p : nat) (A G : {group gT}).
This is Aschbacher (23.7)
Lemma center_special_abelem : p.-group G → special G → p.-abelem 'Z(G).
Lemma exponent_special : p.-group G → special G → exponent G %| p ^ 2.
Lemma exponent_special : p.-group G → special G → exponent G %| p ^ 2.
Aschbacher 24.7 (replaces Gorenstein 5.3.7)
Theorem abelian_charsimple_special :
p.-group G → coprime #|G| #|A| → [~: G, A] = G →
\bigcup_(H : {group gT} | (H \char G) && abelian H) H \subset 'C(A) →
special G ∧ 'C_G(A) = 'Z(G).
End Special.
Section Extraspecial.
Variables (p : nat) (gT rT : finGroupType).
Implicit Types D E F G H K M R S T U : {group gT}.
Section Basic.
Variable S : {group gT}.
Hypotheses (pS : p.-group S) (esS : extraspecial S).
Let pZ : p.-group 'Z(S) := pgroupS (center_sub S) pS.
Lemma extraspecial_prime : prime p.
Lemma card_center_extraspecial : #|'Z(S)| = p.
Lemma min_card_extraspecial : #|S| ≥ p ^ 3.
End Basic.
Lemma card_p3group_extraspecial E :
prime p → #|E| = (p ^ 3)%N → #|'Z(E)| = p → extraspecial E.
Lemma p3group_extraspecial G :
p.-group G → ~~ abelian G → logn p #|G| ≤ 3 → extraspecial G.
Lemma extraspecial_nonabelian G : extraspecial G → ~~ abelian G.
Lemma exponent_2extraspecial G : 2.-group G → extraspecial G → exponent G = 4.
Lemma injm_special D G (f : {morphism D >-> rT}) :
'injm f → G \subset D → special G → special (f @* G).
Lemma injm_extraspecial D G (f : {morphism D >-> rT}) :
'injm f → G \subset D → extraspecial G → extraspecial (f @* G).
Lemma isog_special G (R : {group rT}) :
G \isog R → special G → special R.
Lemma isog_extraspecial G (R : {group rT}) :
G \isog R → extraspecial G → extraspecial R.
Lemma cprod_extraspecial G H K :
p.-group G → H \* K = G → H :&: K = 'Z(H) →
extraspecial H → extraspecial K → extraspecial G.
p.-group G → coprime #|G| #|A| → [~: G, A] = G →
\bigcup_(H : {group gT} | (H \char G) && abelian H) H \subset 'C(A) →
special G ∧ 'C_G(A) = 'Z(G).
End Special.
Section Extraspecial.
Variables (p : nat) (gT rT : finGroupType).
Implicit Types D E F G H K M R S T U : {group gT}.
Section Basic.
Variable S : {group gT}.
Hypotheses (pS : p.-group S) (esS : extraspecial S).
Let pZ : p.-group 'Z(S) := pgroupS (center_sub S) pS.
Lemma extraspecial_prime : prime p.
Lemma card_center_extraspecial : #|'Z(S)| = p.
Lemma min_card_extraspecial : #|S| ≥ p ^ 3.
End Basic.
Lemma card_p3group_extraspecial E :
prime p → #|E| = (p ^ 3)%N → #|'Z(E)| = p → extraspecial E.
Lemma p3group_extraspecial G :
p.-group G → ~~ abelian G → logn p #|G| ≤ 3 → extraspecial G.
Lemma extraspecial_nonabelian G : extraspecial G → ~~ abelian G.
Lemma exponent_2extraspecial G : 2.-group G → extraspecial G → exponent G = 4.
Lemma injm_special D G (f : {morphism D >-> rT}) :
'injm f → G \subset D → special G → special (f @* G).
Lemma injm_extraspecial D G (f : {morphism D >-> rT}) :
'injm f → G \subset D → extraspecial G → extraspecial (f @* G).
Lemma isog_special G (R : {group rT}) :
G \isog R → special G → special R.
Lemma isog_extraspecial G (R : {group rT}) :
G \isog R → extraspecial G → extraspecial R.
Lemma cprod_extraspecial G H K :
p.-group G → H \* K = G → H :&: K = 'Z(H) →
extraspecial H → extraspecial K → extraspecial G.
Lemmas bundling Aschbacher (23.10) with (19.1), (19.2), (19.12) and (20.8)
Section ExtraspecialFormspace.
Variable G : {group gT}.
Hypotheses (pG : p.-group G) (esG : extraspecial G).
Let p_pr := extraspecial_prime pG esG.
Let oZ := card_center_extraspecial pG esG.
Let p_gt1 := prime_gt1 p_pr.
Let p_gt0 := prime_gt0 p_pr.
Variable G : {group gT}.
Hypotheses (pG : p.-group G) (esG : extraspecial G).
Let p_pr := extraspecial_prime pG esG.
Let oZ := card_center_extraspecial pG esG.
Let p_gt1 := prime_gt1 p_pr.
Let p_gt0 := prime_gt0 p_pr.
This encasulates Aschbacher (23.10)(1).
This is the tranposition of the hyperplane dimension theorem (Aschbacher
(19.1)) to subgroups of an extraspecial group.
This is the tranposition of the orthogonal subspace dimension theorem
(Aschbacher (19.2)) to subgroups of an extraspecial group.
This is the tranposition of the proof that a singular vector is contained
in a hyperbolic plane (Aschbacher (19.12)) to subgroups of an extraspecial
group.
Lemma split1_extraspecial x :
x \in G :\: 'Z(G) →
{E : {group gT} & {R : {group gT} |
[/\ #|E| = (p ^ 3)%N ∧ #|R| = #|G| %/ p ^ 2,
E \* R = G ∧ E :&: R = 'Z(E),
'Z(E) = 'Z(G) ∧ 'Z(R) = 'Z(G),
extraspecial E ∧ x \in E
& if abelian R then R :=: 'Z(G) else extraspecial R]}}.
x \in G :\: 'Z(G) →
{E : {group gT} & {R : {group gT} |
[/\ #|E| = (p ^ 3)%N ∧ #|R| = #|G| %/ p ^ 2,
E \* R = G ∧ E :&: R = 'Z(E),
'Z(E) = 'Z(G) ∧ 'Z(R) = 'Z(G),
extraspecial E ∧ x \in E
& if abelian R then R :=: 'Z(G) else extraspecial R]}}.
This is the tranposition of the proof that the dimension of any maximal
totally singular subspace is equal to the Witt index (Aschbacher (20.8)),
to subgroups of an extraspecial group (in a slightly more general form,
since we allow for p != 2).
Note that Aschbacher derives this from the Witt lemma, which we avoid.
This is B & G, Theorem 4.15, as done in Aschbacher (23.8)
Lemma critical_extraspecial R S :
p.-group R → S \subset R → extraspecial S → [~: S, R] \subset S^`(1) →
S \* 'C_R(S) = R.
p.-group R → S \subset R → extraspecial S → [~: S, R] \subset S^`(1) →
S \* 'C_R(S) = R.
This is part of Aschbacher (23.13) and (23.14).
Theorem extraspecial_structure S : p.-group S → extraspecial S →
{Es | all (fun E ⇒ (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es
& \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.
Section StructureCorollaries.
Variable S : {group gT}.
Hypotheses (pS : p.-group S) (esS : extraspecial S).
Let p_pr := extraspecial_prime pS esS.
Let oZ := card_center_extraspecial pS esS.
{Es | all (fun E ⇒ (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es
& \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.
Section StructureCorollaries.
Variable S : {group gT}.
Hypotheses (pS : p.-group S) (esS : extraspecial S).
Let p_pr := extraspecial_prime pS esS.
Let oZ := card_center_extraspecial pS esS.
This is Aschbacher (23.10)(2).
Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}.
Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z(S) \isog Aut 'Z(S).
Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z(S) \isog Aut 'Z(S).
These are the parts of Aschbacher (23.12) and exercise 8.5 that are later
used in Aschbacher (34.9), which itself replaces the informal discussion
quoted from Gorenstein in the proof of B & G, Theorem 2.5.
Lemma center_aut_extraspecial k : coprime k p →
exists2 f, f \in Aut S & ∀ z, z \in 'Z(S) → f z = (z ^+ k)%g.
End StructureCorollaries.
End Extraspecial.
Section SCN.
Variables (gT : finGroupType) (p : nat) (G : {group gT}).
Implicit Types A Z H : {group gT}.
Lemma SCN_P A : reflect (A <| G ∧ 'C_G(A) = A) (A \in 'SCN(G)).
Lemma SCN_abelian A : A \in 'SCN(G) → abelian A.
Lemma exponent_Ohm1_class2 H :
odd p → p.-group H → nil_class H ≤ 2 → exponent 'Ohm_1(H) %| p.
exists2 f, f \in Aut S & ∀ z, z \in 'Z(S) → f z = (z ^+ k)%g.
End StructureCorollaries.
End Extraspecial.
Section SCN.
Variables (gT : finGroupType) (p : nat) (G : {group gT}).
Implicit Types A Z H : {group gT}.
Lemma SCN_P A : reflect (A <| G ∧ 'C_G(A) = A) (A \in 'SCN(G)).
Lemma SCN_abelian A : A \in 'SCN(G) → abelian A.
Lemma exponent_Ohm1_class2 H :
odd p → p.-group H → nil_class H ≤ 2 → exponent 'Ohm_1(H) %| p.
SCN_max and max_SCN cover Aschbacher 23.15(1)
Lemma SCN_max A : A \in 'SCN(G) → [max A | A <| G & abelian A].
Lemma max_SCN A :
p.-group G → [max A | A <| G & abelian A] → A \in 'SCN(G).
Lemma max_SCN A :
p.-group G → [max A | A <| G & abelian A] → A \in 'SCN(G).
The two other assertions of Aschbacher 23.15 state properties of the
normal series 1 <| Z = 'Ohm_1(A) <| A with A \in 'SCN(G).
Section SCNseries.
Variables A : {group gT}.
Hypothesis SCN_A : A \in 'SCN(G).
Let Z := 'Ohm_1(A).
Let cAA := SCN_abelian SCN_A.
Let sZA: Z \subset A := Ohm_sub 1 A.
Let nZA : A \subset 'N(Z) := sub_abelian_norm cAA sZA.
This is Aschbacher 23.15(2).
This is Aschbacher 23.15(3); note that this proof does not depend on the
maximality of A.
Lemma Ohm1_stab_Ohm1_SCN_series :
odd p → p.-group G → 'Ohm_1('C_G(Z)) \subset 'C_G(A / Z | 'Q).
End SCNseries.
odd p → p.-group G → 'Ohm_1('C_G(Z)) \subset 'C_G(A / Z | 'Q).
End SCNseries.
This is Aschbacher 23.16.
Lemma Ohm1_cent_max_normal_abelem Z :
odd p → p.-group G → [max Z | Z <| G & p.-abelem Z] → 'Ohm_1('C_G(Z)) = Z.
Lemma critical_class2 H : critical H G → nil_class H ≤ 2.
odd p → p.-group G → [max Z | Z <| G & p.-abelem Z] → 'Ohm_1('C_G(Z)) = Z.
Lemma critical_class2 H : critical H G → nil_class H ≤ 2.
This proof of the Thompson critical lemma is adapted from Aschbacher 23.6