Library mathcomp.solvable.extraspecial
(* (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.
From mathcomp Require Import extremal.
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.
From mathcomp Require Import extremal.
This file contains the fine structure thorems for extraspecial p-groups.
Together with the material in the maximal and extremal libraries, it
completes the coverage of Aschbacher, section 23.
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 q = 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
We construct and study the following extraspecial groups:
p^{1+2} == if p is prime, an extraspecial group of order p^3 that has
exponent p or 4, and p-rank 2: thus p^{1+2} is isomorphic to
'D_8 if p - 2, and NOT isomorphic to 'Mod_(p^3) if p is odd.
p^{1+2*n} == the central product of n copies of p^{1+2}, thus of order
p^(1+2*n) if p is a prime, and, when n > 0, a representative
of the (unique) isomorphism class of extraspecial groups of
order p^(1+2*n), of exponent p or 4, and p-rank n+1.
'D^n == an alternative (and preferred) notation for 2^{1+2*n}, which
is isomorphic to the central product of n copies od 'D_8.
'D^n*Q == the central product of 'D^n with 'Q_8, thus isomorphic to
all extraspecial groups of order 2 ^ (2 * n + 3) that are
not isomorphic to 'D^n.+1 (or, equivalently, have 2-rank n).
As in extremal.v, these notations are simultaneously defined in the %type,
%g and %G scopes -- depending on the syntactic context, they denote either
a finGroupType, the set, or the group of all its elements.
Set Implicit Arguments.
Local Notation "n %:R" := (n %:R%R).
Import GroupScope GRing.Theory.
Reserved Notation "p ^{1+2}" (at level 2, format "p ^{1+2}").
Reserved Notation "p ^{1+2* n }"
(at level 2, n at level 2, format "p ^{1+2* n }").
Reserved Notation "''D^' n" (at level 8, n at level 2, format "''D^' n").
Reserved Notation "''D^' n * 'Q'"
(at level 8, n at level 2, format "''D^' n * 'Q'").
Module Pextraspecial.
Section Construction.
Variable p : nat.
Definition act ij (k : 'Z_p) := let: (i, j) := ij in (i + k × j, j)%R.
Lemma actP : is_action [set: 'Z_p] act.
Canonical action := Action actP.
Lemma gactP : is_groupAction [set: 'Z_p × 'Z_p] action.
Definition groupAction := GroupAction gactP.
Fact gtype_key : unit.
Definition gtype := locked_with gtype_key (sdprod_groupType groupAction).
Definition ngtype := ncprod [set: gtype].
End Construction.
Definition ngtypeQ n := xcprod [set: ngtype 2 n] 'Q_8.
End Pextraspecial.
Notation "p ^{1+2}" := (Pextraspecial.gtype p) : type_scope.
Notation "p ^{1+2}" := [set: gsort p^{1+2}] : group_scope.
Notation "p ^{1+2}" := [set: gsort p^{1+2}]%G : Group_scope.
Notation "p ^{1+2* n }" := (Pextraspecial.ngtype p n) : type_scope.
Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}] : group_scope.
Notation "p ^{1+2* n }" := [set: gsort p^{1+2*n}]%G : Group_scope.
Notation "''D^' n" := (Pextraspecial.ngtype 2 n) : type_scope.
Notation "''D^' n" := [set: gsort 'D^n] : group_scope.
Notation "''D^' n" := [set: gsort 'D^n]%G : Group_scope.
Notation "''D^' n * 'Q'" := (Pextraspecial.ngtypeQ n) : type_scope.
Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q] : group_scope.
Notation "''D^' n * 'Q'" := [set: gsort 'D^n×Q]%G : Group_scope.
Section ExponentPextraspecialTheory.
Variable p : nat.
Hypothesis p_pr : prime p.
Let p_gt1 := prime_gt1 p_pr.
Let p_gt0 := ltnW p_gt1.
Local Notation gtype := Pextraspecial.gtype.
Local Notation actp := (Pextraspecial.groupAction p).
Lemma card_pX1p2 : #|p^{1+2}| = (p ^ 3)%N.
Lemma Grp_pX1p2 :
p^{1+2} \isog Grp (x : y : x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y]).
Lemma pX1p2_pgroup : p.-group p^{1+2}.
This is part of the existence half of Aschbacher ex. (8.7)(1)
This is part of the existence half of Aschbacher ex. (8.7)(1)
This is the uniqueness half of Aschbacher ex. (8.7)(1)
Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) :
extraspecial G → exponent G %| p → #|G| = (p ^ 3)%N → G \isog p^{1+2}.
End ExponentPextraspecialTheory.
Section GeneralExponentPextraspecialTheory.
Variable p : nat.
Lemma pX1p2id : p^{1+2*1} \isog p^{1+2}.
Lemma pX1p2S n : xcprod_spec p^{1+2} p^{1+2*n} p^{1+2*n.+1}%type.
Lemma card_pX1p2n n : prime p → #|p^{1+2*n}| = (p ^ n.*2.+1)%N.
Lemma pX1p2n_pgroup n : prime p → p.-group p^{1+2*n}.
extraspecial G → exponent G %| p → #|G| = (p ^ 3)%N → G \isog p^{1+2}.
End ExponentPextraspecialTheory.
Section GeneralExponentPextraspecialTheory.
Variable p : nat.
Lemma pX1p2id : p^{1+2*1} \isog p^{1+2}.
Lemma pX1p2S n : xcprod_spec p^{1+2} p^{1+2*n} p^{1+2*n.+1}%type.
Lemma card_pX1p2n n : prime p → #|p^{1+2*n}| = (p ^ n.*2.+1)%N.
Lemma pX1p2n_pgroup n : prime p → p.-group p^{1+2*n}.
This is part of the existence half of Aschbacher (23.13)
This is part of the existence half of Aschbacher (23.13) and (23.14)
This is Aschbacher (23.12)
Lemma Ohm1_extraspecial_odd (gT : finGroupType) (G : {group gT}) :
p.-group G → extraspecial G → odd #|G| →
let Y := 'Ohm_1(G) in
[/\ exponent Y = p, #|G : Y| %| p
& Y != G →
∃ E : {group gT},
[/\ #|G : Y| = p, #|E| = p ∨ extraspecial E,
exists2 X : {group gT}, #|X| = p & X \x E = Y
& ∃ M : {group gT},
[/\ M \isog 'Mod_(p ^ 3), M \* E = G & M :&: E = 'Z(M)]]].
p.-group G → extraspecial G → odd #|G| →
let Y := 'Ohm_1(G) in
[/\ exponent Y = p, #|G : Y| %| p
& Y != G →
∃ E : {group gT},
[/\ #|G : Y| = p, #|E| = p ∨ extraspecial E,
exists2 X : {group gT}, #|X| = p & X \x E = Y
& ∃ M : {group gT},
[/\ M \isog 'Mod_(p ^ 3), M \* E = G & M :&: E = 'Z(M)]]].
This is the uniqueness half of Aschbacher (23.13); the proof incorporates
in part the proof that symplectic spaces are hyperbolic (19.16).
Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) :
prime p → extraspecial G → #|G| = (p ^ n.*2.+1)%N → exponent G %| p →
G \isog p^{1+2*n}.
End GeneralExponentPextraspecialTheory.
Lemma isog_2X1p2 : 2^{1+2} \isog 'D_8.
Lemma Q8_extraspecial : extraspecial 'Q_8.
Lemma DnQ_P n : xcprod_spec 'D^n 'Q_8 ('D^n×Q)%type.
Lemma card_DnQ n : #|'D^n×Q| = (2 ^ n.+1.*2.+1)%N.
Lemma DnQ_pgroup n : 2.-group 'D^n×Q.
prime p → extraspecial G → #|G| = (p ^ n.*2.+1)%N → exponent G %| p →
G \isog p^{1+2*n}.
End GeneralExponentPextraspecialTheory.
Lemma isog_2X1p2 : 2^{1+2} \isog 'D_8.
Lemma Q8_extraspecial : extraspecial 'Q_8.
Lemma DnQ_P n : xcprod_spec 'D^n 'Q_8 ('D^n×Q)%type.
Lemma card_DnQ n : #|'D^n×Q| = (2 ^ n.+1.*2.+1)%N.
Lemma DnQ_pgroup n : 2.-group 'D^n×Q.
Final part of the existence half of Aschbacher (23.14).
A special case of the uniqueness half of Achsbacher (23.14).
Lemma card_isog8_extraspecial (gT : finGroupType) (G : {group gT}) :
#|G| = 8 → extraspecial G → (G \isog 'D_8) || (G \isog 'Q_8).
#|G| = 8 → extraspecial G → (G \isog 'D_8) || (G \isog 'Q_8).
The uniqueness half of Achsbacher (23.14). The proof incorporates in part
the proof that symplectic spces are hyperbolic (Aschbacher (19.16)), and
the determination of quadratic spaces over 'F_2 (21.2); however we use
the second part of exercise (8.4) to avoid resorting to Witt's lemma and
Galois theory as in (20.9) and (21.1).
Lemma isog_2extraspecial (gT : finGroupType) (G : {group gT}) n :
#|G| = (2 ^ n.*2.+1)%N → extraspecial G → G \isog 'D^n ∨ G \isog 'D^n.-1×Q.
#|G| = (2 ^ n.*2.+1)%N → extraspecial G → G \isog 'D^n ∨ G \isog 'D^n.-1×Q.
The first concluding remark of Aschbacher (23.14).
The second concluding remark of Aschbacher (23.14).
The final concluding remark of Aschbacher (23.14).