Library mathcomp.solvable.extraspecial
+ +
+(* (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 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 Open Scope ring_scope.
+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).
+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.
+ +
+ +
+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}.
+ +
+
+
++Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+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).
+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.
+ +
+ +
+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).
+
+
+