Library extraspecial

 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.                 


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 Structure action := Action actP.

Lemma gactP : is_groupAction [set: 'Z_p * 'Z_p] action.
Canonical Structure groupAction := GroupAction gactP.

Definition gtype := locked (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 : subgroup_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 : subgroup_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 : subgroup_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 : subgroup_scope.

Section ExponentPextraspecialTheory.

Variable p : nat.
Hypothesis p_pr : prime p.

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) 
Lemma exponent_pX1p2 : odd p -> exponent p^{1+2} %| p.

 This is the uniqueness half of Aschbacher ex. (8.7)(1) 
Lemma isog_pX1p2 : forall (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 : forall n, xcprod_spec p^{1+2} p^{1+2*n} p^{1+2*n.+1}%type.

Lemma card_pX1p2n : forall n, prime p -> #|p^{1+2*n}| = (p ^ n.*2.+1)%N.

Lemma pX1p2n_pgroup : forall n, prime p -> p.-group p^{1+2*n}.

 This is part of the existence half of Aschbacher (23.13) 
Lemma exponent_pX1p2n : forall 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 : forall n,
  prime p -> n > 0 -> extraspecial p^{1+2*n}.

 This is Aschbacher (23.12) 
Lemma Ohm1_extraspecial_odd : forall (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 ->
      exists E : {group gT},
        [/\ #|G : Y| = p, #|E| = p \/ extraspecial E,
            exists2 X : {group gT}, #|X| = p & X \x E = Y
          & exists 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 : forall 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 : forall n, xcprod_spec 'D^n 'Q_8 ('D^n*Q)%type.

Lemma card_DnQ : forall n, #|'D^n*Q| = (2 ^ n.+1.*2.+1)%N.

Lemma DnQ_pgroup : forall n, 2.-group 'D^n*Q.

 Final part of the existence half of Aschbacher (23.14). 
Lemma DnQ_extraspecial : forall n, extraspecial 'D^n*Q.

 A special case of the uniqueness half of Achsbacher (23.14). 
Lemma card_isog8_extraspecial : forall (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 : forall (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 : forall n, 'r_2('D^n) = n.+1.

 The second concluding remark of Aschbacher (23.14). 
Lemma rank_DnQ : forall n, 'r_2('D^n*Q) = n.+1.

 The final concluding remark of Aschbacher (23.14). 
Lemma not_isog_Dn_DnQ : forall n, ~~ ('D^n \isog 'D^n.-1*Q).