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