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.

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.

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.


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 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).
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).
The second concluding remark of Aschbacher (23.14).
The final concluding remark of Aschbacher (23.14).