- -

Library mathcomp.solvable.extremal

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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.
-

- -

- 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).
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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_type 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.
- -
-

- -

- 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 ].
- -
-

- -

- 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 )].
- -
-

- -

- 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).
- -
-

- -

- 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 )).
- -
-

- -

- 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.
-