Library mathcomp.solvable.extremal
(* (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 div.
From mathcomp Require Import choice fintype bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism presentation.
From mathcomp Require Import quotient action commutator gproduct gfunctor.
From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries.
From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism presentation.
From mathcomp Require Import quotient action commutator gproduct gfunctor.
From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries.
From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal.
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 Notation "n %:R" := (n %:R%R).
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.
Local Notation B := <[b]>.
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 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 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).
Local Notation ED := [set: gsort (Extremal.gtype q p q.-1)].
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).
Local Notation extgK := cancel_index_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)]].
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).
Local Notation ED := [set: gsort (Extremal.gtype q p q.-1)].
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).
Local Notation extgK := cancel_index_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.
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.