(Joint Center)Library MathComp.extraspecial

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import bigop finset prime binomial fingroup morphism perm automorphism.
Require Import presentation quotient action commutator gproduct gfunctor.
Require Import ssralg finalg zmodp cyclic pgroup center gseries.
Require Import nilpotent sylow abelian finmodule matrix maximal 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 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.

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)
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 Gextraspecial Godd #|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).
Final part of the existence half of Aschbacher (23.14).
A special case of the uniqueness half of Achsbacher (23.14).
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).
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).
The final concluding remark of Aschbacher (23.14).