Library mathcomp.solvable.extremal
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file contains the definition and properties of extremal p-groups;
+ it covers and is mostly based on the beginning of Aschbacher, section 23,
+ as well as several exercises of this section.
+ We define canonical representatives for the group classes that cover the
+ extremal p-groups (non-abelian p-groups with a cyclic maximal subgroup):
+ 'Mod_m == the modular group of order m, for m = p ^ n, p prime and n >= 3.
+ 'D_m == the dihedral group of order m, for m = 2n >= 4.
+ 'Q_m == the generalized quaternion group of order m, for m = 2 ^ n >= 8.
+ 'SD_m == the semi-dihedral group of order m, for m = 2 ^ n >= 16.
+ In each case the notation is defined in the %type, %g and %G scopes, where
+ it denotes a finGroupType, a full gset and the full group for that type.
+ However each notation is only meaningful under the given conditions, in
+ 'D_m is only an extremal group for m = 2 ^ n >= 8, and 'D_8 = 'Mod_8 (they
+ are, in fact, beta-convertible).
+ We also define
+ extremal_generators G p n (x, y) <-> G has order p ^ n, x in G has order
+ p ^ n.-1, and y is in G \ < [x]>: thus < [x]> has index p in G,
+ so if p is prime, < [x]> is maximal in G, G is generated by x
+ and y, and G is extremal or abelian.
+ extremal_class G == the class of extremal groups G belongs to: one of
+ ModularGroup, Dihedral, Quaternion, SemiDihedral or NotExtremal.
+ extremal2 G <=> extremal_class G is one of Dihedral, Quaternion, or
+ SemiDihedral; this allows 'D_4 and 'D_8, but excludes 'Mod(2^n)
+ for n > 3.
+ modular_group_generators p n (x, y) <-> y has order p and acts on x via
+ x ^ y = x ^+ (p ^ n.-2).+1. This is the complement to
+ extremal_generators G p n (x, y) for modular groups.
+ We provide cardinality, presentation, generator and structure theorems for
+ each class of extremal group. The extremal_generators predicate is used to
+ supply structure theorems with all the required data about G; this is
+ completed by an isomorphism assumption (e.g., G \isog 'D(2 ^ n)), and
+ sometimes other properties (e.g., # [y] == 2 in the semidihedral case). The
+ generators assumption can be deduced generically from the isomorphism
+ assumption, or it can be proved manually for a specific choice of x and y.
+ The extremal_class function is used to formulate synthetic theorems that
+ cover several classes of extremal groups (e.g., Aschbacher ex. 8.3).
+
+
+
+
+Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+Import GroupScope GRing.Theory.
+ +
+Reserved Notation "''Mod_' m" (at level 8, m at level 2, format "''Mod_' m").
+Reserved Notation "''D_' m" (at level 8, m at level 2, format "''D_' m").
+Reserved Notation "''SD_' m" (at level 8, m at level 2, format "''SD_' m").
+Reserved Notation "''Q_' m" (at level 8, m at level 2, format "''Q_' m").
+ +
+Module Extremal.
+ +
+Section Construction.
+ +
+Variables q p e : nat.
+
+
++Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+Import GroupScope GRing.Theory.
+ +
+Reserved Notation "''Mod_' m" (at level 8, m at level 2, format "''Mod_' m").
+Reserved Notation "''D_' m" (at level 8, m at level 2, format "''D_' m").
+Reserved Notation "''SD_' m" (at level 8, m at level 2, format "''SD_' m").
+Reserved Notation "''Q_' m" (at level 8, m at level 2, format "''Q_' m").
+ +
+Module Extremal.
+ +
+Section Construction.
+ +
+Variables q p e : nat.
+
+ Construct the semi-direct product of 'Z_q by 'Z_p with 1%R ^ 1%R = e%R,
+ if possible, i.e., if p, q > 1 and there is s \in Aut 'Z_p such that
+ # [s] %| p and s 1%R = 1%R ^+ e.
+
+
+
+
+Let a : 'Z_p := Zp1.
+Let b : 'Z_q := Zp1.
+ +
+Definition aut_of :=
+ odflt 1 [pick s in Aut B | p > 1 & (#[s] %| p) && (s b == b ^+ e)].
+ +
+Lemma aut_dvdn : #[aut_of] %| #[a].
+ +
+Definition act_morphism := eltm_morphism aut_dvdn.
+ +
+Definition base_act := ([Aut B] \o act_morphism)%gact.
+ +
+Lemma act_dom : <[a]> \subset act_dom base_act.
+ +
+Definition gact := (base_act \ act_dom)%gact.
+Fact gtype_key : unit.
+Definition gtype := locked_with gtype_key (sdprod_groupType gact).
+ +
+Hypotheses (p_gt1 : p > 1) (q_gt1 : q > 1).
+ +
+Lemma card : #|[set: gtype]| = (p × q)%N.
+ +
+Lemma Grp : (∃ s, [/\ s \in Aut B, #[s] %| p & s b = b ^+ e]) →
+ [set: gtype] \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ e)).
+ +
+End Construction.
+ +
+End Extremal.
+ +
+Section SpecializeExtremals.
+ +
+Import Extremal.
+ +
+Variable m : nat.
+Let p := pdiv m.
+Let q := m %/ p.
+ +
+Definition modular_gtype := gtype q p (q %/ p).+1.
+Definition dihedral_gtype := gtype q 2 q.-1.
+Definition semidihedral_gtype := gtype q 2 (q %/ p).-1.
+Definition quaternion_kernel :=
+ <<[set u | u ^+ 2 == 1] :\: [set u ^+ 2 | u in [set: gtype q 4 q.-1]]>>.
+Definition quaternion_gtype :=
+ locked_with gtype_key (coset_groupType quaternion_kernel).
+ +
+End SpecializeExtremals.
+ +
+Notation "''Mod_' m" := (modular_gtype m) : type_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m] : group_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m]%G : Group_scope.
+ +
+Notation "''D_' m" := (dihedral_gtype m) : type_scope.
+Notation "''D_' m" := [set: gsort 'D_m] : group_scope.
+Notation "''D_' m" := [set: gsort 'D_m]%G : Group_scope.
+ +
+Notation "''SD_' m" := (semidihedral_gtype m) : type_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m] : group_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m]%G : Group_scope.
+ +
+Notation "''Q_' m" := (quaternion_gtype m) : type_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m] : group_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m]%G : Group_scope.
+ +
+Section ExtremalTheory.
+ +
+Implicit Types (gT : finGroupType) (p q m n : nat).
+ +
+
+
++Let a : 'Z_p := Zp1.
+Let b : 'Z_q := Zp1.
+ +
+Definition aut_of :=
+ odflt 1 [pick s in Aut B | p > 1 & (#[s] %| p) && (s b == b ^+ e)].
+ +
+Lemma aut_dvdn : #[aut_of] %| #[a].
+ +
+Definition act_morphism := eltm_morphism aut_dvdn.
+ +
+Definition base_act := ([Aut B] \o act_morphism)%gact.
+ +
+Lemma act_dom : <[a]> \subset act_dom base_act.
+ +
+Definition gact := (base_act \ act_dom)%gact.
+Fact gtype_key : unit.
+Definition gtype := locked_with gtype_key (sdprod_groupType gact).
+ +
+Hypotheses (p_gt1 : p > 1) (q_gt1 : q > 1).
+ +
+Lemma card : #|[set: gtype]| = (p × q)%N.
+ +
+Lemma Grp : (∃ s, [/\ s \in Aut B, #[s] %| p & s b = b ^+ e]) →
+ [set: gtype] \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ e)).
+ +
+End Construction.
+ +
+End Extremal.
+ +
+Section SpecializeExtremals.
+ +
+Import Extremal.
+ +
+Variable m : nat.
+Let p := pdiv m.
+Let q := m %/ p.
+ +
+Definition modular_gtype := gtype q p (q %/ p).+1.
+Definition dihedral_gtype := gtype q 2 q.-1.
+Definition semidihedral_gtype := gtype q 2 (q %/ p).-1.
+Definition quaternion_kernel :=
+ <<[set u | u ^+ 2 == 1] :\: [set u ^+ 2 | u in [set: gtype q 4 q.-1]]>>.
+Definition quaternion_gtype :=
+ locked_with gtype_key (coset_groupType quaternion_kernel).
+ +
+End SpecializeExtremals.
+ +
+Notation "''Mod_' m" := (modular_gtype m) : type_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m] : group_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m]%G : Group_scope.
+ +
+Notation "''D_' m" := (dihedral_gtype m) : type_scope.
+Notation "''D_' m" := [set: gsort 'D_m] : group_scope.
+Notation "''D_' m" := [set: gsort 'D_m]%G : Group_scope.
+ +
+Notation "''SD_' m" := (semidihedral_gtype m) : type_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m] : group_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m]%G : Group_scope.
+ +
+Notation "''Q_' m" := (quaternion_gtype m) : type_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m] : group_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m]%G : Group_scope.
+ +
+Section ExtremalTheory.
+ +
+Implicit Types (gT : finGroupType) (p q m n : nat).
+ +
+
+ This is Aschbacher (23.3), with the isomorphism made explicit, and a
+ slightly reworked case analysis on the prime and exponent; in particular
+ the inverting involution is available for all non-trivial p-cycles.
+
+
+Lemma cyclic_pgroup_Aut_structure gT p (G : {group gT}) :
+ p.-group G → cyclic G → G :!=: 1 →
+ let q := #|G| in let n := (logn p q).-1 in
+ let A := Aut G in let P := 'O_p(A) in let F := 'O_p^'(A) in
+ ∃ m : {perm gT} → 'Z_q,
+ [/\ [/\ {in A & G, ∀ a x, x ^+ m a = a x},
+ m 1 = 1%R ∧ {in A &, {morph m : a b / a × b >-> (a × b)%R}},
+ {in A &, injective m} ∧ image m A =i GRing.unit,
+ ∀ k, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+ & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+ [/\ abelian A, cyclic F, #|F| = p.-1
+ & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+ & if n == 0%N then A = F else
+ ∃ t, [/\ t \in A, #[t] = 2, m t = - 1%R
+ & if odd p then
+ [/\ cyclic A ∧ cyclic P,
+ ∃ s, [/\ s \in A, #[s] = (p ^ n)%N, m s = p.+1%:R & P = <[s]>]
+ & ∃ s0, [/\ s0 \in A, #[s0] = p, m s0 = (p ^ n).+1%:R
+ & 'Ohm_1(P) = <[s0]>]]
+ else if n == 1%N then A = <[t]>
+ else ∃ s,
+ [/\ s \in A, #[s] = (2 ^ n.-1)%N, m s = 5%:R, <[s]> \x <[t]> = A
+ & ∃ s0, [/\ s0 \in A, #[s0] = 2, m s0 = (2 ^ n).+1%:R,
+ m (s0 × t) = (2 ^ n).-1%:R & 'Ohm_1(<[s]>) = <[s0]>]]]].
+ +
+Definition extremal_generators gT (A : {set gT}) p n xy :=
+ let: (x, y) := xy in
+ [/\ #|A| = (p ^ n)%N, x \in A, #[x] = (p ^ n.-1)%N & y \in A :\: <[x]>].
+ +
+Lemma extremal_generators_facts gT (G : {group gT}) p n x y :
+ prime p → extremal_generators G p n (x, y) →
+ [/\ p.-group G, maximal <[x]> G, <[x]> <| G,
+ <[x]> × <[y]> = G & <[y]> \subset 'N(<[x]>)].
+ +
+Section ModularGroup.
+ +
+Variables p n : nat.
+Let m := (p ^ n)%N.
+Let q := (p ^ n.-1)%N.
+Let r := (p ^ n.-2)%N.
+ +
+Hypotheses (p_pr : prime p) (n_gt2 : n > 2).
+Let p_gt1 := prime_gt1 p_pr.
+Let p_gt0 := ltnW p_gt1.
+Let def_n := esym (subnKC n_gt2).
+Let def_p : pdiv m = p.
+Let def_q : m %/ p = q.
+Let def_r : q %/ p = r.
+Let ltqm : q < m.
+Let ltrq : r < q.
+Let r_gt0 : 0 < r.
+Let q_gt1 : q > 1.
+ +
+Lemma card_modular_group : #|'Mod_(p ^ n)| = (p ^ n)%N.
+ +
+Lemma Grp_modular_group :
+ 'Mod_(p ^ n) \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ r.+1)).
+ +
+Definition modular_group_generators gT (xy : gT × gT) :=
+ let: (x, y) := xy in #[y] = p ∧ x ^ y = x ^+ r.+1.
+ +
+Lemma generators_modular_group gT (G : {group gT}) :
+ G \isog 'Mod_m →
+ exists2 xy, extremal_generators G p n xy & modular_group_generators xy.
+ +
+
+
++ p.-group G → cyclic G → G :!=: 1 →
+ let q := #|G| in let n := (logn p q).-1 in
+ let A := Aut G in let P := 'O_p(A) in let F := 'O_p^'(A) in
+ ∃ m : {perm gT} → 'Z_q,
+ [/\ [/\ {in A & G, ∀ a x, x ^+ m a = a x},
+ m 1 = 1%R ∧ {in A &, {morph m : a b / a × b >-> (a × b)%R}},
+ {in A &, injective m} ∧ image m A =i GRing.unit,
+ ∀ k, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+ & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+ [/\ abelian A, cyclic F, #|F| = p.-1
+ & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+ & if n == 0%N then A = F else
+ ∃ t, [/\ t \in A, #[t] = 2, m t = - 1%R
+ & if odd p then
+ [/\ cyclic A ∧ cyclic P,
+ ∃ s, [/\ s \in A, #[s] = (p ^ n)%N, m s = p.+1%:R & P = <[s]>]
+ & ∃ s0, [/\ s0 \in A, #[s0] = p, m s0 = (p ^ n).+1%:R
+ & 'Ohm_1(P) = <[s0]>]]
+ else if n == 1%N then A = <[t]>
+ else ∃ s,
+ [/\ s \in A, #[s] = (2 ^ n.-1)%N, m s = 5%:R, <[s]> \x <[t]> = A
+ & ∃ s0, [/\ s0 \in A, #[s0] = 2, m s0 = (2 ^ n).+1%:R,
+ m (s0 × t) = (2 ^ n).-1%:R & 'Ohm_1(<[s]>) = <[s0]>]]]].
+ +
+Definition extremal_generators gT (A : {set gT}) p n xy :=
+ let: (x, y) := xy in
+ [/\ #|A| = (p ^ n)%N, x \in A, #[x] = (p ^ n.-1)%N & y \in A :\: <[x]>].
+ +
+Lemma extremal_generators_facts gT (G : {group gT}) p n x y :
+ prime p → extremal_generators G p n (x, y) →
+ [/\ p.-group G, maximal <[x]> G, <[x]> <| G,
+ <[x]> × <[y]> = G & <[y]> \subset 'N(<[x]>)].
+ +
+Section ModularGroup.
+ +
+Variables p n : nat.
+Let m := (p ^ n)%N.
+Let q := (p ^ n.-1)%N.
+Let r := (p ^ n.-2)%N.
+ +
+Hypotheses (p_pr : prime p) (n_gt2 : n > 2).
+Let p_gt1 := prime_gt1 p_pr.
+Let p_gt0 := ltnW p_gt1.
+Let def_n := esym (subnKC n_gt2).
+Let def_p : pdiv m = p.
+Let def_q : m %/ p = q.
+Let def_r : q %/ p = r.
+Let ltqm : q < m.
+Let ltrq : r < q.
+Let r_gt0 : 0 < r.
+Let q_gt1 : q > 1.
+ +
+Lemma card_modular_group : #|'Mod_(p ^ n)| = (p ^ n)%N.
+ +
+Lemma Grp_modular_group :
+ 'Mod_(p ^ n) \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ r.+1)).
+ +
+Definition modular_group_generators gT (xy : gT × gT) :=
+ let: (x, y) := xy in #[y] = p ∧ x ^ y = x ^+ r.+1.
+ +
+Lemma generators_modular_group gT (G : {group gT}) :
+ G \isog 'Mod_m →
+ exists2 xy, extremal_generators G p n xy & modular_group_generators xy.
+ +
+
+ This is an adaptation of Aschbacher, exercise 8.2:
+
+-
+
- We allow an alternative to the # [x] = p ^ n.-1 condition that meshes + better with the modular_Grp lemma above. + + +
- We state explicitly some "obvious" properties of G, namely that G is + the non-abelian semi-direct product < [x]> ><| < [y]> and that y ^+ j + acts on < [x]> via z |-> z ^+ (j * p ^ n.-2).+1 + + +
- We also give the values of the 'Mho^k(G). + + +
- We corrected a pair of typos. + +
+Lemma modular_group_structure gT (G : {group gT}) x y :
+ extremal_generators G p n (x, y) →
+ G \isog 'Mod_m → modular_group_generators (x, y) →
+ let X := <[x]> in
+ [/\ [/\ X ><| <[y]> = G, ~~ abelian G
+ & {in X, ∀ z j, z ^ (y ^+ j) = z ^+ (j × r).+1}],
+ [/\ 'Z(G) = <[x ^+ p]>, 'Phi(G) = 'Z(G) & #|'Z(G)| = r],
+ [/\ G^`(1) = <[x ^+ r]>, #|G^`(1)| = p & nil_class G = 2],
+ ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>
+ & if (p, n) == (2, 3) then 'Ohm_1(G) = G else
+ ∀ k, 0 < k < n.-1 →
+ <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G)
+ ∧ #|'Ohm_k(G)| = (p ^ k.+1)%N].
+ +
+End ModularGroup.
+ +
+
+
++ extremal_generators G p n (x, y) →
+ G \isog 'Mod_m → modular_group_generators (x, y) →
+ let X := <[x]> in
+ [/\ [/\ X ><| <[y]> = G, ~~ abelian G
+ & {in X, ∀ z j, z ^ (y ^+ j) = z ^+ (j × r).+1}],
+ [/\ 'Z(G) = <[x ^+ p]>, 'Phi(G) = 'Z(G) & #|'Z(G)| = r],
+ [/\ G^`(1) = <[x ^+ r]>, #|G^`(1)| = p & nil_class G = 2],
+ ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>
+ & if (p, n) == (2, 3) then 'Ohm_1(G) = G else
+ ∀ k, 0 < k < n.-1 →
+ <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G)
+ ∧ #|'Ohm_k(G)| = (p ^ k.+1)%N].
+ +
+End ModularGroup.
+ +
+
+ Basic properties of dihedral groups; these will be refined for dihedral
+ 2-groups in the section on extremal 2-groups.
+
+
+Section DihedralGroup.
+ +
+Variable q : nat.
+Hypothesis q_gt1 : q > 1.
+Let m := q.*2.
+ +
+Let def2 : pdiv m = 2.
+ +
+Let def_q : m %/ pdiv m = q.
+ +
+Section Dihedral_extension.
+ +
+Variable p : nat.
+Hypotheses (p_gt1 : p > 1) (even_p : 2 %| p).
+ +
+Lemma card_ext_dihedral : #|ED| = (p./2 × m)%N.
+ +
+Lemma Grp_ext_dihedral : ED \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x^-1)).
+ +
+End Dihedral_extension.
+ +
+Lemma card_dihedral : #|'D_m| = m.
+ +
+Lemma Grp_dihedral : 'D_m \isog Grp (x : y : (x ^+ q, y ^+ 2, x ^ y = x^-1)).
+ +
+Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : (x ^+ 2, y ^+ 2, (x × y) ^+ q)).
+ +
+End DihedralGroup.
+ +
+Lemma involutions_gen_dihedral gT (x y : gT) :
+ let G := <<[set x; y]>> in
+ #[x] = 2 → #[y] = 2 → x != y → G \isog 'D_#|G|.
+ +
+Lemma Grp_2dihedral n : n > 1 →
+ 'D_(2 ^ n) \isog Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x^-1)).
+ +
+Lemma card_2dihedral n : n > 1 → #|'D_(2 ^ n)| = (2 ^ n)%N.
+ +
+Lemma card_semidihedral n : n > 3 → #|'SD_(2 ^ n)| = (2 ^ n)%N.
+ +
+Lemma Grp_semidihedral n : n > 3 →
+ 'SD_(2 ^ n) \isog
+ Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x ^+ (2 ^ n.-2).-1)).
+ +
+Section Quaternion.
+ +
+Variable n : nat.
+Hypothesis n_gt2 : n > 2.
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let r := (2 ^ n.-2)%N.
+Let GrpQ := 'Q_m \isog Grp (x : y : (x ^+ q, y ^+ 2 = x ^+ r, x ^ y = x^-1)).
+Let defQ : #|'Q_m| = m ∧ GrpQ.
+ +
+Lemma card_quaternion : #|'Q_m| = m.
+Lemma Grp_quaternion : GrpQ.
+ +
+End Quaternion.
+ +
+Lemma eq_Mod8_D8 : 'Mod_8 = 'D_8.
+ +
+Section ExtremalStructure.
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n : nat).
+Implicit Type H : {group gT}.
+ +
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let q_gt0: q > 0.
+Let r := (2 ^ n.-2)%N.
+Let r_gt0: r > 0.
+ +
+Let def2qr : n > 1 → [/\ 2 × q = m, 2 × r = q, q < m & r < q]%N.
+ +
+Lemma generators_2dihedral :
+ n > 1 → G \isog 'D_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x^-1.
+ +
+Lemma generators_semidihedral :
+ n > 3 → G \isog 'SD_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x ^+ r.-1.
+ +
+Lemma generators_quaternion :
+ n > 2 → G \isog 'Q_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in [/\ #[y] = 4, y ^+ 2 = x ^+ r & x ^ y = x^-1].
+ +
+Variables x y : gT.
+Implicit Type M : {group gT}.
+ +
+Let X := <[x]>.
+Let Y := <[y]>.
+Let yG := y ^: G.
+Let xyG := (x × y) ^: G.
+Let My := <<yG>>.
+Let Mxy := <<xyG>>.
+ +
+Theorem dihedral2_structure :
+ n > 1 → extremal_generators G 2 n (x, y) → G \isog 'D_m →
+ [/\ [/\ X ><| Y = G, {in G :\: X, ∀ t, #[t] = 2}
+ & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ 'Ohm_1(G) = G ∧ (∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>),
+ [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+ & ∀ M, maximal M G = pred3 X My Mxy M]
+ & if n == 2 then (2.-abelem G : Prop) else
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ My \isog 'D_q, Mxy \isog 'D_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+Theorem quaternion_structure :
+ n > 2 → extremal_generators G 2 n (x, y) → G \isog 'Q_m →
+ [/\ [/\ pprod X Y = G, {in G :\: X, ∀ t, #[t] = 4}
+ & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ ∀ u, u \in G → #[u] = 2 → u = x ^+ r,
+ 'Ohm_1(G) = <[x ^+ r]> ∧ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+ & ∀ M, maximal M G = pred3 X My Mxy M]
+ & n > 3 →
+ [/\ My \isog 'Q_q, Mxy \isog 'Q_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+Theorem semidihedral_structure :
+ n > 3 → extremal_generators G 2 n (x, y) → G \isog 'SD_m → #[y] = 2 →
+ [/\ [/\ X ><| Y = G, #[x × y] = 4
+ & {in X & G :\: X, ∀ z t, z ^ t = z ^+ r.-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ 'Ohm_1(G) = My ∧ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+ & ∀ H, maximal H G = pred3 X My Mxy H]
+ & [/\ My \isog 'D_q, Mxy \isog 'Q_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+End ExtremalStructure.
+ +
+Section ExtremalClass.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Inductive extremal_group_type :=
+ ModularGroup | Dihedral | SemiDihedral | Quaternion | NotExtremal.
+ +
+Definition index_extremal_group_type c :=
+ match c with
+ | ModularGroup ⇒ 0
+ | Dihedral ⇒ 1
+ | SemiDihedral ⇒ 2
+ | Quaternion ⇒ 3
+ | NotExtremal ⇒ 4
+ end%N.
+ +
+Definition enum_extremal_groups :=
+ [:: ModularGroup; Dihedral; SemiDihedral; Quaternion].
+ +
+Lemma cancel_index_extremal_groups :
+ cancel index_extremal_group_type (nth NotExtremal enum_extremal_groups).
+ +
+Import choice.
+ +
+Definition extremal_group_eqMixin := CanEqMixin extgK.
+Canonical extremal_group_eqType := EqType _ extremal_group_eqMixin.
+Definition extremal_group_choiceMixin := CanChoiceMixin extgK.
+Canonical extremal_group_choiceType := ChoiceType _ extremal_group_choiceMixin.
+Definition extremal_group_countMixin := CanCountMixin extgK.
+Canonical extremal_group_countType := CountType _ extremal_group_countMixin.
+Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
+ Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups.
+Canonical extremal_group_finType := FinType _ extremal_group_finMixin.
+ +
+Definition extremal_class (A : {set gT}) :=
+ let m := #|A| in let p := pdiv m in let n := logn p m in
+ if (n > 1) && (A \isog 'D_(2 ^ n)) then Dihedral else
+ if (n > 2) && (A \isog 'Q_(2 ^ n)) then Quaternion else
+ if (n > 3) && (A \isog 'SD_(2 ^ n)) then SemiDihedral else
+ if (n > 2) && (A \isog 'Mod_(p ^ n)) then ModularGroup else
+ NotExtremal.
+ +
+Definition extremal2 A := extremal_class A \in behead enum_extremal_groups.
+ +
+Lemma dihedral_classP :
+ extremal_class G = Dihedral ↔ (exists2 n, n > 1 & G \isog 'D_(2 ^ n)).
+ +
+Lemma quaternion_classP :
+ extremal_class G = Quaternion ↔ (exists2 n, n > 2 & G \isog 'Q_(2 ^ n)).
+ +
+Lemma semidihedral_classP :
+ extremal_class G = SemiDihedral ↔ (exists2 n, n > 3 & G \isog 'SD_(2 ^ n)).
+ +
+Lemma odd_not_extremal2 : odd #|G| → ~~ extremal2 G.
+ +
+Lemma modular_group_classP :
+ extremal_class G = ModularGroup
+ ↔ (exists2 p, prime p &
+ exists2 n, n ≥ (p == 2) + 3 & G \isog 'Mod_(p ^ n)).
+ +
+End ExtremalClass.
+ +
+Theorem extremal2_structure (gT : finGroupType) (G : {group gT}) n x y :
+ let cG := extremal_class G in
+ let m := (2 ^ n)%N in let q := (2 ^ n.-1)%N in let r := (2 ^ n.-2)%N in
+ let X := <[x]> in let yG := y ^: G in let xyG := (x × y) ^: G in
+ let My := <<yG>> in let Mxy := <<xyG>> in
+ extremal_generators G 2 n (x, y) →
+ extremal2 G → (cG == SemiDihedral) ==> (#[y] == 2) →
+ [/\ [/\ (if cG == Quaternion then pprod X <[y]> else X ><| <[y]>) = G,
+ if cG == SemiDihedral then #[x × y] = 4 else
+ {in G :\: X, ∀ z, #[z] = (if cG == Dihedral then 2 else 4)},
+ if cG != Quaternion then True else
+ {in G, ∀ z, #[z] = 2 → z = x ^+ r}
+ & {in X & G :\: X, ∀ t z,
+ t ^ z = (if cG == SemiDihedral then t ^+ r.-1 else t^-1)}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ if n > 2 then 'Z(G) = <[x ^+ r]> ∧ #|'Z(G)| = 2 else 2.-abelem G,
+ 'Ohm_1(G) = (if cG == Quaternion then <[x ^+ r]> else
+ if cG == SemiDihedral then My else G),
+ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+ & ∀ H : {group gT}, maximal H G = (gval H \in pred3 X My Mxy)]
+ & if n ≤ (cG == Quaternion) + 2 then True else
+ [/\ ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X,
+ if cG == Quaternion then My \isog 'Q_q else My \isog 'D_q,
+ extremal_class My = (if cG == Quaternion then cG else Dihedral),
+ if cG == Dihedral then Mxy \isog 'D_q else Mxy \isog 'Q_q
+ & extremal_class Mxy = (if cG == Dihedral then cG else Quaternion)]].
+ +
+
+
++ +
+Variable q : nat.
+Hypothesis q_gt1 : q > 1.
+Let m := q.*2.
+ +
+Let def2 : pdiv m = 2.
+ +
+Let def_q : m %/ pdiv m = q.
+ +
+Section Dihedral_extension.
+ +
+Variable p : nat.
+Hypotheses (p_gt1 : p > 1) (even_p : 2 %| p).
+ +
+Lemma card_ext_dihedral : #|ED| = (p./2 × m)%N.
+ +
+Lemma Grp_ext_dihedral : ED \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x^-1)).
+ +
+End Dihedral_extension.
+ +
+Lemma card_dihedral : #|'D_m| = m.
+ +
+Lemma Grp_dihedral : 'D_m \isog Grp (x : y : (x ^+ q, y ^+ 2, x ^ y = x^-1)).
+ +
+Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : (x ^+ 2, y ^+ 2, (x × y) ^+ q)).
+ +
+End DihedralGroup.
+ +
+Lemma involutions_gen_dihedral gT (x y : gT) :
+ let G := <<[set x; y]>> in
+ #[x] = 2 → #[y] = 2 → x != y → G \isog 'D_#|G|.
+ +
+Lemma Grp_2dihedral n : n > 1 →
+ 'D_(2 ^ n) \isog Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x^-1)).
+ +
+Lemma card_2dihedral n : n > 1 → #|'D_(2 ^ n)| = (2 ^ n)%N.
+ +
+Lemma card_semidihedral n : n > 3 → #|'SD_(2 ^ n)| = (2 ^ n)%N.
+ +
+Lemma Grp_semidihedral n : n > 3 →
+ 'SD_(2 ^ n) \isog
+ Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x ^+ (2 ^ n.-2).-1)).
+ +
+Section Quaternion.
+ +
+Variable n : nat.
+Hypothesis n_gt2 : n > 2.
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let r := (2 ^ n.-2)%N.
+Let GrpQ := 'Q_m \isog Grp (x : y : (x ^+ q, y ^+ 2 = x ^+ r, x ^ y = x^-1)).
+Let defQ : #|'Q_m| = m ∧ GrpQ.
+ +
+Lemma card_quaternion : #|'Q_m| = m.
+Lemma Grp_quaternion : GrpQ.
+ +
+End Quaternion.
+ +
+Lemma eq_Mod8_D8 : 'Mod_8 = 'D_8.
+ +
+Section ExtremalStructure.
+ +
+Variables (gT : finGroupType) (G : {group gT}) (n : nat).
+Implicit Type H : {group gT}.
+ +
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let q_gt0: q > 0.
+Let r := (2 ^ n.-2)%N.
+Let r_gt0: r > 0.
+ +
+Let def2qr : n > 1 → [/\ 2 × q = m, 2 × r = q, q < m & r < q]%N.
+ +
+Lemma generators_2dihedral :
+ n > 1 → G \isog 'D_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x^-1.
+ +
+Lemma generators_semidihedral :
+ n > 3 → G \isog 'SD_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x ^+ r.-1.
+ +
+Lemma generators_quaternion :
+ n > 2 → G \isog 'Q_m →
+ exists2 xy, extremal_generators G 2 n xy
+ & let: (x, y) := xy in [/\ #[y] = 4, y ^+ 2 = x ^+ r & x ^ y = x^-1].
+ +
+Variables x y : gT.
+Implicit Type M : {group gT}.
+ +
+Let X := <[x]>.
+Let Y := <[y]>.
+Let yG := y ^: G.
+Let xyG := (x × y) ^: G.
+Let My := <<yG>>.
+Let Mxy := <<xyG>>.
+ +
+Theorem dihedral2_structure :
+ n > 1 → extremal_generators G 2 n (x, y) → G \isog 'D_m →
+ [/\ [/\ X ><| Y = G, {in G :\: X, ∀ t, #[t] = 2}
+ & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ 'Ohm_1(G) = G ∧ (∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>),
+ [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+ & ∀ M, maximal M G = pred3 X My Mxy M]
+ & if n == 2 then (2.-abelem G : Prop) else
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ My \isog 'D_q, Mxy \isog 'D_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+Theorem quaternion_structure :
+ n > 2 → extremal_generators G 2 n (x, y) → G \isog 'Q_m →
+ [/\ [/\ pprod X Y = G, {in G :\: X, ∀ t, #[t] = 4}
+ & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ ∀ u, u \in G → #[u] = 2 → u = x ^+ r,
+ 'Ohm_1(G) = <[x ^+ r]> ∧ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+ & ∀ M, maximal M G = pred3 X My Mxy M]
+ & n > 3 →
+ [/\ My \isog 'Q_q, Mxy \isog 'Q_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+Theorem semidihedral_structure :
+ n > 3 → extremal_generators G 2 n (x, y) → G \isog 'SD_m → #[y] = 2 →
+ [/\ [/\ X ><| Y = G, #[x × y] = 4
+ & {in X & G :\: X, ∀ z t, z ^ t = z ^+ r.-1}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+ 'Ohm_1(G) = My ∧ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+ & ∀ H, maximal H G = pred3 X My Mxy H]
+ & [/\ My \isog 'D_q, Mxy \isog 'Q_q
+ & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+ +
+End ExtremalStructure.
+ +
+Section ExtremalClass.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Inductive extremal_group_type :=
+ ModularGroup | Dihedral | SemiDihedral | Quaternion | NotExtremal.
+ +
+Definition index_extremal_group_type c :=
+ match c with
+ | ModularGroup ⇒ 0
+ | Dihedral ⇒ 1
+ | SemiDihedral ⇒ 2
+ | Quaternion ⇒ 3
+ | NotExtremal ⇒ 4
+ end%N.
+ +
+Definition enum_extremal_groups :=
+ [:: ModularGroup; Dihedral; SemiDihedral; Quaternion].
+ +
+Lemma cancel_index_extremal_groups :
+ cancel index_extremal_group_type (nth NotExtremal enum_extremal_groups).
+ +
+Import choice.
+ +
+Definition extremal_group_eqMixin := CanEqMixin extgK.
+Canonical extremal_group_eqType := EqType _ extremal_group_eqMixin.
+Definition extremal_group_choiceMixin := CanChoiceMixin extgK.
+Canonical extremal_group_choiceType := ChoiceType _ extremal_group_choiceMixin.
+Definition extremal_group_countMixin := CanCountMixin extgK.
+Canonical extremal_group_countType := CountType _ extremal_group_countMixin.
+Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
+ Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups.
+Canonical extremal_group_finType := FinType _ extremal_group_finMixin.
+ +
+Definition extremal_class (A : {set gT}) :=
+ let m := #|A| in let p := pdiv m in let n := logn p m in
+ if (n > 1) && (A \isog 'D_(2 ^ n)) then Dihedral else
+ if (n > 2) && (A \isog 'Q_(2 ^ n)) then Quaternion else
+ if (n > 3) && (A \isog 'SD_(2 ^ n)) then SemiDihedral else
+ if (n > 2) && (A \isog 'Mod_(p ^ n)) then ModularGroup else
+ NotExtremal.
+ +
+Definition extremal2 A := extremal_class A \in behead enum_extremal_groups.
+ +
+Lemma dihedral_classP :
+ extremal_class G = Dihedral ↔ (exists2 n, n > 1 & G \isog 'D_(2 ^ n)).
+ +
+Lemma quaternion_classP :
+ extremal_class G = Quaternion ↔ (exists2 n, n > 2 & G \isog 'Q_(2 ^ n)).
+ +
+Lemma semidihedral_classP :
+ extremal_class G = SemiDihedral ↔ (exists2 n, n > 3 & G \isog 'SD_(2 ^ n)).
+ +
+Lemma odd_not_extremal2 : odd #|G| → ~~ extremal2 G.
+ +
+Lemma modular_group_classP :
+ extremal_class G = ModularGroup
+ ↔ (exists2 p, prime p &
+ exists2 n, n ≥ (p == 2) + 3 & G \isog 'Mod_(p ^ n)).
+ +
+End ExtremalClass.
+ +
+Theorem extremal2_structure (gT : finGroupType) (G : {group gT}) n x y :
+ let cG := extremal_class G in
+ let m := (2 ^ n)%N in let q := (2 ^ n.-1)%N in let r := (2 ^ n.-2)%N in
+ let X := <[x]> in let yG := y ^: G in let xyG := (x × y) ^: G in
+ let My := <<yG>> in let Mxy := <<xyG>> in
+ extremal_generators G 2 n (x, y) →
+ extremal2 G → (cG == SemiDihedral) ==> (#[y] == 2) →
+ [/\ [/\ (if cG == Quaternion then pprod X <[y]> else X ><| <[y]>) = G,
+ if cG == SemiDihedral then #[x × y] = 4 else
+ {in G :\: X, ∀ z, #[z] = (if cG == Dihedral then 2 else 4)},
+ if cG != Quaternion then True else
+ {in G, ∀ z, #[z] = 2 → z = x ^+ r}
+ & {in X & G :\: X, ∀ t z,
+ t ^ z = (if cG == SemiDihedral then t ^+ r.-1 else t^-1)}],
+ [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+ & nil_class G = n.-1],
+ [/\ if n > 2 then 'Z(G) = <[x ^+ r]> ∧ #|'Z(G)| = 2 else 2.-abelem G,
+ 'Ohm_1(G) = (if cG == Quaternion then <[x ^+ r]> else
+ if cG == SemiDihedral then My else G),
+ 'Ohm_2(G) = G
+ & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+ [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+ & ∀ H : {group gT}, maximal H G = (gval H \in pred3 X My Mxy)]
+ & if n ≤ (cG == Quaternion) + 2 then True else
+ [/\ ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X,
+ if cG == Quaternion then My \isog 'Q_q else My \isog 'D_q,
+ extremal_class My = (if cG == Quaternion then cG else Dihedral),
+ if cG == Dihedral then Mxy \isog 'D_q else Mxy \isog 'Q_q
+ & extremal_class Mxy = (if cG == Dihedral then cG else Quaternion)]].
+ +
+
+ This is Aschbacher (23.4).
+
+
+Lemma maximal_cycle_extremal gT p (G X : {group gT}) :
+ p.-group G → ~~ abelian G → cyclic X → X \subset G → #|G : X| = p →
+ (extremal_class G == ModularGroup) || (p == 2) && extremal2 G.
+ +
+
+
++ p.-group G → ~~ abelian G → cyclic X → X \subset G → #|G : X| = p →
+ (extremal_class G == ModularGroup) || (p == 2) && extremal2 G.
+ +
+
+ This is Aschbacher (23.5)
+
+
+Lemma cyclic_SCN gT p (G U : {group gT}) :
+ p.-group G → U \in 'SCN(G) → ~~ abelian G → cyclic U →
+ [/\ p = 2, #|G : U| = 2 & extremal2 G]
+∨ ∃ M : {group gT},
+ [/\ M :=: 'C_G('Mho^1(U)), #|M : U| = p, extremal_class M = ModularGroup,
+ 'Ohm_1(M)%G \in 'E_p^2(G) & 'Ohm_1(M) \char G].
+ +
+
+
++ p.-group G → U \in 'SCN(G) → ~~ abelian G → cyclic U →
+ [/\ p = 2, #|G : U| = 2 & extremal2 G]
+∨ ∃ M : {group gT},
+ [/\ M :=: 'C_G('Mho^1(U)), #|M : U| = p, extremal_class M = ModularGroup,
+ 'Ohm_1(M)%G \in 'E_p^2(G) & 'Ohm_1(M) \char G].
+ +
+
+ This is Aschbacher, exercise (8.4)
+
+
+Lemma normal_rank1_structure gT p (G : {group gT}) :
+ p.-group G → (∀ X : {group gT}, X <| G → abelian X → cyclic X) →
+ cyclic G ∨ [&& p == 2, extremal2 G & (#|G| ≥ 16) || (G \isog 'Q_8)].
+ +
+
+
++ p.-group G → (∀ X : {group gT}, X <| G → abelian X → cyclic X) →
+ cyclic G ∨ [&& p == 2, extremal2 G & (#|G| ≥ 16) || (G \isog 'Q_8)].
+ +
+
+ Replacement for Section 4 proof.
+
+
+Lemma odd_pgroup_rank1_cyclic gT p (G : {group gT}) :
+ p.-group G → odd #|G| → cyclic G = ('r_p(G) ≤ 1).
+ +
+
+
++ p.-group G → odd #|G| → cyclic G = ('r_p(G) ≤ 1).
+ +
+
+ This is the second part of Aschbacher, exercise (8.4).
+
+
+Lemma prime_Ohm1P gT p (G : {group gT}) :
+ p.-group G → G :!=: 1 →
+ reflect (#|'Ohm_1(G)| = p)
+ (cyclic G || (p == 2) && (extremal_class G == Quaternion)).
+ +
+
+
++ p.-group G → G :!=: 1 →
+ reflect (#|'Ohm_1(G)| = p)
+ (cyclic G || (p == 2) && (extremal_class G == Quaternion)).
+ +
+
+ This is Aschbacher (23.9)
+
+
+Theorem symplectic_type_group_structure gT p (G : {group gT}) :
+ p.-group G → (∀ X : {group gT}, X \char G → abelian X → cyclic X) →
+ exists2 E : {group gT}, E :=: 1 ∨ extraspecial E
+ & ∃ R : {group gT},
+ [/\ cyclic R ∨ [/\ p = 2, extremal2 R & #|R| ≥ 16],
+ E \* R = G
+ & E :&: R = 'Z(E)].
+ +
+End ExtremalTheory.
+
++ p.-group G → (∀ X : {group gT}, X \char G → abelian X → cyclic X) →
+ exists2 E : {group gT}, E :=: 1 ∨ extraspecial E
+ & ∃ R : {group gT},
+ [/\ cyclic R ∨ [/\ p = 2, extremal2 R & #|R| ≥ 16],
+ E \* R = G
+ & E :&: R = 'Z(E)].
+ +
+End ExtremalTheory.
+