- -

Library mathcomp.solvable.extraspecial

- -

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

- -

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

- -

- This is part of the existence half of Aschbacher ex. (8.7)(1) -

-Lemma pX1p2_extraspecial : extraspecial p ^{1+2}.
- -
-

- -

- This is part of the existence half of Aschbacher ex. (8.7)(1) -

-Lemma exponent_pX1p2 : odd p → exponent p ^{1+2} %| p.
- -
-

- -

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

- -

- This is part of the existence half of Aschbacher (23.13) -

-Lemma exponent_pX1p2n n : prime p → odd p → exponent p ^{1+2*n } = p.
- -
-

- -

- This is part of the existence half of Aschbacher (23.13) and (23.14) -

-Lemma pX1p2n_extraspecial n : prime p → n > 0 → extraspecial p ^{1+2*n }.
- -
-

- -

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

- -

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

- -

- Final part of the existence half of Aschbacher (23.14). -

-Lemma DnQ_extraspecial n : extraspecial 'D ^n ×Q.
- -
-

- -

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

- -

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

- -

- The first concluding remark of Aschbacher (23.14). -

-Lemma rank_Dn n : 'r_2 ('D ^n ) = n .+1.
- -
-

- -

- The second concluding remark of Aschbacher (23.14). -

-Lemma rank_DnQ n : 'r_2 ('D ^n ×Q ) = n .+1.
- -
-

- -

- The final concluding remark of Aschbacher (23.14). -

-Lemma not_isog_Dn_DnQ n : ~~ ('D ^n \isog 'D ^n .-1 ×Q ).
-