From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.solvable.extremal.html | 534 +++++++++++++-------------- 1 file changed, 267 insertions(+), 267 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.extremal.html') diff --git a/docs/htmldoc/mathcomp.solvable.extremal.html b/docs/htmldoc/mathcomp.solvable.extremal.html index b05aa23..a4ce716 100644 --- a/docs/htmldoc/mathcomp.solvable.extremal.html +++ b/docs/htmldoc/mathcomp.solvable.extremal.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -86,7 +85,7 @@ Section Construction.

-Variables q p e : nat.
+Variables q p e : nat.
@@ -97,39 +96,39 @@

-Let a : 'Z_p := Zp1.
-Let b : 'Z_q := Zp1.
+Let a : 'Z_p := Zp1.
+Let b : 'Z_q := Zp1.

Definition aut_of :=
-  odflt 1 [pick s in Aut B | p > 1 & (#[s] %| p) && (s b == b ^+ e)].
+  odflt 1 [pick s in Aut B | p > 1 & (#[s] %| p) && (s b == b ^+ e)].

-Lemma aut_dvdn : #[aut_of] %| #[a].
+Lemma aut_dvdn : #[aut_of] %| #[a].

Definition act_morphism := eltm_morphism aut_dvdn.

-Definition base_act := ([Aut B] \o act_morphism)%gact.
+Definition base_act := ([Aut B] \o act_morphism)%gact.

-Lemma act_dom : <[a]> \subset act_dom base_act.
+Lemma act_dom : <[a]> \subset act_dom base_act.

-Definition gact := (base_act \ act_dom)%gact.
-Fact gtype_key : unit.
-Definition gtype := locked_with gtype_key (sdprod_groupType gact).
+Definition gact := (base_act \ act_dom)%gact.
+Fact gtype_key : unit.
+Definition gtype := locked_with gtype_key (sdprod_groupType gact).

-Hypotheses (p_gt1 : p > 1) (q_gt1 : q > 1).
+Hypotheses (p_gt1 : p > 1) (q_gt1 : q > 1).

-Lemma card : #|[set: gtype]| = (p × q)%N.
+Lemma card : #|[set: gtype]| = (p × q)%N.

-Lemma Grp : (∃ s, [/\ s \in Aut B, #[s] %| p & s b = b ^+ e]) →
-  [set: gtype] \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ e)).
+Lemma Grp : (∃ s, [/\ s \in Aut B, #[s] %| p & s b = b ^+ e]) →
+  [set: gtype] \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ e)).

End Construction.
@@ -144,47 +143,47 @@ Import Extremal.

-Variable m : nat.
+Variable m : nat.
Let p := pdiv m.
-Let q := m %/ p.
+Let q := m %/ p.

-Definition modular_gtype := gtype q p (q %/ p).+1.
-Definition dihedral_gtype := gtype q 2 q.-1.
-Definition semidihedral_gtype := gtype q 2 (q %/ p).-1.
+Definition modular_gtype := gtype q p (q %/ p).+1.
+Definition dihedral_gtype := gtype q 2 q.-1.
+Definition semidihedral_gtype := gtype q 2 (q %/ p).-1.
Definition quaternion_kernel :=
-  <<[set u | u ^+ 2 == 1] :\: [set u ^+ 2 | u in [set: gtype q 4 q.-1]]>>.
+  <<[set u | u ^+ 2 == 1] :\: [set u ^+ 2 | u in [set: gtype q 4 q.-1]]>>.
Definition quaternion_gtype :=
-  locked_with gtype_key (coset_groupType quaternion_kernel).
+  locked_with gtype_key (coset_groupType quaternion_kernel).

End SpecializeExtremals.

-Notation "''Mod_' m" := (modular_gtype m) : type_scope.
-Notation "''Mod_' m" := [set: gsort 'Mod_m] : group_scope.
-Notation "''Mod_' m" := [set: gsort 'Mod_m]%G : Group_scope.
+Notation "''Mod_' m" := (modular_gtype m) : type_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m] : group_scope.
+Notation "''Mod_' m" := [set: gsort 'Mod_m]%G : Group_scope.

-Notation "''D_' m" := (dihedral_gtype m) : type_scope.
-Notation "''D_' m" := [set: gsort 'D_m] : group_scope.
-Notation "''D_' m" := [set: gsort 'D_m]%G : Group_scope.
+Notation "''D_' m" := (dihedral_gtype m) : type_scope.
+Notation "''D_' m" := [set: gsort 'D_m] : group_scope.
+Notation "''D_' m" := [set: gsort 'D_m]%G : Group_scope.

-Notation "''SD_' m" := (semidihedral_gtype m) : type_scope.
-Notation "''SD_' m" := [set: gsort 'SD_m] : group_scope.
-Notation "''SD_' m" := [set: gsort 'SD_m]%G : Group_scope.
+Notation "''SD_' m" := (semidihedral_gtype m) : type_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m] : group_scope.
+Notation "''SD_' m" := [set: gsort 'SD_m]%G : Group_scope.

-Notation "''Q_' m" := (quaternion_gtype m) : type_scope.
-Notation "''Q_' m" := [set: gsort 'Q_m] : group_scope.
-Notation "''Q_' m" := [set: gsort 'Q_m]%G : Group_scope.
+Notation "''Q_' m" := (quaternion_gtype m) : type_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m] : group_scope.
+Notation "''Q_' m" := [set: gsort 'Q_m]%G : Group_scope.

Section ExtremalTheory.

-Implicit Types (gT : finGroupType) (p q m n : nat).
+Implicit Types (gT : finGroupType) (p q m n : nat).

@@ -195,79 +194,79 @@ the inverting involution is available for all non-trivial p-cycles.
-Lemma cyclic_pgroup_Aut_structure gT p (G : {group gT}) :
-    p.-group G → cyclic G → G :!=: 1 →
-  let q := #|G| in let n := (logn p q).-1 in
-  let A := Aut G in let P := 'O_p(A) in let F := 'O_p^'(A) in
-  ∃ m : {perm gT} → 'Z_q,
-  [/\ [/\ {in A & G, ∀ a x, x ^+ m a = a x},
-          m 1 = 1%R ∧ {in A &, {morph m : a b / a × b >-> (a × b)%R}},
-          {in A &, injective m} ∧ image m A =i GRing.unit,
-          ∀ k, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
-        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
-      [/\ abelian A, cyclic F, #|F| = p.-1
-        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
- & if n == 0%N then A = F else
-      ∃ t, [/\ t \in A, #[t] = 2, m t = - 1%R
-      & if odd p then
-        [/\ cyclic A ∧ cyclic P,
-           ∃ s, [/\ s \in A, #[s] = (p ^ n)%N, m s = p.+1%:R & P = <[s]>]
-         & ∃ s0, [/\ s0 \in A, #[s0] = p, m s0 = (p ^ n).+1%:R
-                        & 'Ohm_1(P) = <[s0]>]]
- else if n == 1%N then A = <[t]>
-   else ∃ s,
-        [/\ s \in A, #[s] = (2 ^ n.-1)%N, m s = 5%:R, <[s]> \x <[t]> = A
-      & ∃ s0, [/\ s0 \in A, #[s0] = 2, m s0 = (2 ^ n).+1%:R,
-                       m (s0 × t) = (2 ^ n).-1%:R & 'Ohm_1(<[s]>) = <[s0]>]]]].
- -
-Definition extremal_generators gT (A : {set gT}) p n xy :=
-  let: (x, y) := xy in
-  [/\ #|A| = (p ^ n)%N, x \in A, #[x] = (p ^ n.-1)%N & y \in A :\: <[x]>].
- -
-Lemma extremal_generators_facts gT (G : {group gT}) p n x y :
-    prime p → extremal_generators G p n (x, y) →
-  [/\ p.-group G, maximal <[x]> G, <[x]> <| G,
-      <[x]> × <[y]> = G & <[y]> \subset 'N(<[x]>)].
+Lemma cyclic_pgroup_Aut_structure gT p (G : {group gT}) :
+    p.-group G → cyclic G → G :!=: 1 →
+  let q := #|G| in let n := (logn p q).-1 in
+  let A := Aut G in let P := 'O_p(A) in let F := 'O_p^'(A) in
+  ∃ m : {perm gT} → 'Z_q,
+  [/\ [/\ {in A & G, ∀ a x, x ^+ m a = a x},
+          m 1 = 1%R ∧ {in A &, {morph m : a b / a × b >-> (a × b)%R}},
+          {in A &, injective m} ∧ image m A =i GRing.unit,
+          ∀ k, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+      [/\ abelian A, cyclic F, #|F| = p.-1
+        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+ & if n == 0%N then A = F else
+      ∃ t, [/\ t \in A, #[t] = 2, m t = - 1%R
+      & if odd p then
+        [/\ cyclic A ∧ cyclic P,
+           ∃ s, [/\ s \in A, #[s] = (p ^ n)%N, m s = p.+1%:R & P = <[s]>]
+         & ∃ s0, [/\ s0 \in A, #[s0] = p, m s0 = (p ^ n).+1%:R
+                        & 'Ohm_1(P) = <[s0]>]]
+ else if n == 1%N then A = <[t]>
+   else ∃ s,
+        [/\ s \in A, #[s] = (2 ^ n.-1)%N, m s = 5%:R, <[s]> \x <[t]> = A
+      & ∃ s0, [/\ s0 \in A, #[s0] = 2, m s0 = (2 ^ n).+1%:R,
+                       m (s0 × t) = (2 ^ n).-1%:R & 'Ohm_1(<[s]>) = <[s0]>]]]].
+ +
+Definition extremal_generators gT (A : {set gT}) p n xy :=
+  let: (x, y) := xy in
+  [/\ #|A| = (p ^ n)%N, x \in A, #[x] = (p ^ n.-1)%N & y \in A :\: <[x]>].
+ +
+Lemma extremal_generators_facts gT (G : {group gT}) p n x y :
+    prime p → extremal_generators G p n (x, y) →
+  [/\ p.-group G, maximal <[x]> G, <[x]> <| G,
+      <[x]> × <[y]> = G & <[y]> \subset 'N(<[x]>)].

Section ModularGroup.

-Variables p n : nat.
-Let m := (p ^ n)%N.
-Let q := (p ^ n.-1)%N.
-Let r := (p ^ n.-2)%N.
+Variables p n : nat.
+Let m := (p ^ n)%N.
+Let q := (p ^ n.-1)%N.
+Let r := (p ^ n.-2)%N.

-Hypotheses (p_pr : prime p) (n_gt2 : n > 2).
+Hypotheses (p_pr : prime p) (n_gt2 : n > 2).
Let p_gt1 := prime_gt1 p_pr.
Let p_gt0 := ltnW p_gt1.
-Let def_n := esym (subnKC n_gt2).
-Let def_p : pdiv m = p.
-Let def_q : m %/ p = q.
-Let def_r : q %/ p = r.
-Let ltqm : q < m.
-Let ltrq : r < q.
-Let r_gt0 : 0 < r.
-Let q_gt1 : q > 1.
+Let def_n := esym (subnKC n_gt2).
+Let def_p : pdiv m = p.
+Let def_q : m %/ p = q.
+Let def_r : q %/ p = r.
+Let ltqm : q < m.
+Let ltrq : r < q.
+Let r_gt0 : 0 < r.
+Let q_gt1 : q > 1.

-Lemma card_modular_group : #|'Mod_(p ^ n)| = (p ^ n)%N.
+Lemma card_modular_group : #|'Mod_(p ^ n)| = (p ^ n)%N.

Lemma Grp_modular_group :
-  'Mod_(p ^ n) \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ r.+1)).
+  'Mod_(p ^ n) \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x ^+ r.+1)).

-Definition modular_group_generators gT (xy : gT × gT) :=
-  let: (x, y) := xy in #[y] = p ∧ x ^ y = x ^+ r.+1.
+Definition modular_group_generators gT (xy : gT × gT) :=
+  let: (x, y) := xy in #[y] = p ∧ x ^ y = x ^+ r.+1.

-Lemma generators_modular_group gT (G : {group gT}) :
-    G \isog 'Mod_m →
-  exists2 xy, extremal_generators G p n xy & modular_group_generators xy.
+Lemma generators_modular_group gT (G : {group gT}) :
+    G \isog 'Mod_m →
+  exists2 xy, extremal_generators G p n xy & modular_group_generators xy.

@@ -293,19 +292,19 @@
-Lemma modular_group_structure gT (G : {group gT}) x y :
-    extremal_generators G p n (x, y) →
-    G \isog 'Mod_m → modular_group_generators (x, y) →
-  let X := <[x]> in
-  [/\ [/\ X ><| <[y]> = G, ~~ abelian G
-        & {in X, ∀ z j, z ^ (y ^+ j) = z ^+ (j × r).+1}],
-      [/\ 'Z(G) = <[x ^+ p]>, 'Phi(G) = 'Z(G) & #|'Z(G)| = r],
-      [/\ G^`(1) = <[x ^+ r]>, #|G^`(1)| = p & nil_class G = 2],
-      ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>
-    & if (p, n) == (2, 3) then 'Ohm_1(G) = G else
-      ∀ k, 0 < k < n.-1 →
-         <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G)
-      ∧ #|'Ohm_k(G)| = (p ^ k.+1)%N].
+Lemma modular_group_structure gT (G : {group gT}) x y :
+    extremal_generators G p n (x, y) →
+    G \isog 'Mod_m → modular_group_generators (x, y) →
+  let X := <[x]> in
+  [/\ [/\ X ><| <[y]> = G, ~~ abelian G
+        & {in X, ∀ z j, z ^ (y ^+ j) = z ^+ (j × r).+1}],
+      [/\ 'Z(G) = <[x ^+ p]>, 'Phi(G) = 'Z(G) & #|'Z(G)| = r],
+      [/\ G^`(1) = <[x ^+ r]>, #|G^`(1)| = p & nil_class G = 2],
+      ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>
+    & if (p, n) == (2, 3) then 'Ohm_1(G) = G else
+      ∀ k, 0 < k < n.-1 →
+         <[x ^+ (p ^ (n - k.+1))]> \x <[y]> = 'Ohm_k(G)
+      ∧ #|'Ohm_k(G)| = (p ^ k.+1)%N].

End ModularGroup.
@@ -321,179 +320,179 @@ Section DihedralGroup.

-Variable q : nat.
-Hypothesis q_gt1 : q > 1.
-Let m := q.*2.
+Variable q : nat.
+Hypothesis q_gt1 : q > 1.
+Let m := q.*2.

-Let def2 : pdiv m = 2.
+Let def2 : pdiv m = 2.

-Let def_q : m %/ pdiv m = q.
+Let def_q : m %/ pdiv m = q.

Section Dihedral_extension.

-Variable p : nat.
-Hypotheses (p_gt1 : p > 1) (even_p : 2 %| p).
+Variable p : nat.
+Hypotheses (p_gt1 : p > 1) (even_p : 2 %| p).

-Lemma card_ext_dihedral : #|ED| = (p./2 × m)%N.
+Lemma card_ext_dihedral : #|ED| = (p./2 × m)%N.

-Lemma Grp_ext_dihedral : ED \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x^-1)).
+Lemma Grp_ext_dihedral : ED \isog Grp (x : y : (x ^+ q, y ^+ p, x ^ y = x^-1)).

End Dihedral_extension.

-Lemma card_dihedral : #|'D_m| = m.
+Lemma card_dihedral : #|'D_m| = m.

-Lemma Grp_dihedral : 'D_m \isog Grp (x : y : (x ^+ q, y ^+ 2, x ^ y = x^-1)).
+Lemma Grp_dihedral : 'D_m \isog Grp (x : y : (x ^+ q, y ^+ 2, x ^ y = x^-1)).

-Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : (x ^+ 2, y ^+ 2, (x × y) ^+ q)).
+Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : (x ^+ 2, y ^+ 2, (x × y) ^+ q)).

End DihedralGroup.

Lemma involutions_gen_dihedral gT (x y : gT) :
-    let G := <<[set x; y]>> in
-  #[x] = 2 → #[y] = 2 → x != y → G \isog 'D_#|G|.
+    let G := <<[set x; y]>> in
+  #[x] = 2 → #[y] = 2 → x != y → G \isog 'D_#|G|.

-Lemma Grp_2dihedral n : n > 1 →
-  'D_(2 ^ n) \isog Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x^-1)).
+Lemma Grp_2dihedral n : n > 1 →
+  'D_(2 ^ n) \isog Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x^-1)).

-Lemma card_2dihedral n : n > 1 → #|'D_(2 ^ n)| = (2 ^ n)%N.
+Lemma card_2dihedral n : n > 1 → #|'D_(2 ^ n)| = (2 ^ n)%N.

-Lemma card_semidihedral n : n > 3 → #|'SD_(2 ^ n)| = (2 ^ n)%N.
+Lemma card_semidihedral n : n > 3 → #|'SD_(2 ^ n)| = (2 ^ n)%N.

-Lemma Grp_semidihedral n : n > 3 →
-  'SD_(2 ^ n) \isog
-     Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x ^+ (2 ^ n.-2).-1)).
+Lemma Grp_semidihedral n : n > 3 →
+  'SD_(2 ^ n) \isog
+     Grp (x : y : (x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x ^+ (2 ^ n.-2).-1)).

Section Quaternion.

-Variable n : nat.
-Hypothesis n_gt2 : n > 2.
-Let m := (2 ^ n)%N.
-Let q := (2 ^ n.-1)%N.
-Let r := (2 ^ n.-2)%N.
-Let GrpQ := 'Q_m \isog Grp (x : y : (x ^+ q, y ^+ 2 = x ^+ r, x ^ y = x^-1)).
-Let defQ : #|'Q_m| = m ∧ GrpQ.
+Variable n : nat.
+Hypothesis n_gt2 : n > 2.
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let r := (2 ^ n.-2)%N.
+Let GrpQ := 'Q_m \isog Grp (x : y : (x ^+ q, y ^+ 2 = x ^+ r, x ^ y = x^-1)).
+Let defQ : #|'Q_m| = m ∧ GrpQ.

-Lemma card_quaternion : #|'Q_m| = m.
+Lemma card_quaternion : #|'Q_m| = m.
Lemma Grp_quaternion : GrpQ.

End Quaternion.

-Lemma eq_Mod8_D8 : 'Mod_8 = 'D_8.
+Lemma eq_Mod8_D8 : 'Mod_8 = 'D_8.

Section ExtremalStructure.

-Variables (gT : finGroupType) (G : {group gT}) (n : nat).
-Implicit Type H : {group gT}.
+Variables (gT : finGroupType) (G : {group gT}) (n : nat).
+Implicit Type H : {group gT}.

-Let m := (2 ^ n)%N.
-Let q := (2 ^ n.-1)%N.
-Let q_gt0: q > 0.
-Let r := (2 ^ n.-2)%N.
-Let r_gt0: r > 0.
+Let m := (2 ^ n)%N.
+Let q := (2 ^ n.-1)%N.
+Let q_gt0: q > 0.
+Let r := (2 ^ n.-2)%N.
+Let r_gt0: r > 0.

-Let def2qr : n > 1 → [/\ 2 × q = m, 2 × r = q, q < m & r < q]%N.
+Let def2qr : n > 1 → [/\ 2 × q = m, 2 × r = q, q < m & r < q]%N.

Lemma generators_2dihedral :
-    n > 1 → G \isog 'D_m →
-  exists2 xy, extremal_generators G 2 n xy
-           & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x^-1.
+    n > 1 → G \isog 'D_m →
+  exists2 xy, extremal_generators G 2 n xy
+           & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x^-1.

Lemma generators_semidihedral :
-    n > 3 → G \isog 'SD_m →
-  exists2 xy, extremal_generators G 2 n xy
-           & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x ^+ r.-1.
+    n > 3 → G \isog 'SD_m →
+  exists2 xy, extremal_generators G 2 n xy
+           & let: (x, y) := xy in #[y] = 2 ∧ x ^ y = x ^+ r.-1.

Lemma generators_quaternion :
-    n > 2 → G \isog 'Q_m →
-  exists2 xy, extremal_generators G 2 n xy
-           & let: (x, y) := xy in [/\ #[y] = 4, y ^+ 2 = x ^+ r & x ^ y = x^-1].
+    n > 2 → G \isog 'Q_m →
+  exists2 xy, extremal_generators G 2 n xy
+           & let: (x, y) := xy in [/\ #[y] = 4, y ^+ 2 = x ^+ r & x ^ y = x^-1].

Variables x y : gT.
-Implicit Type M : {group gT}.
+Implicit Type M : {group gT}.

-Let X := <[x]>.
-Let Y := <[y]>.
-Let yG := y ^: G.
-Let xyG := (x × y) ^: G.
-Let My := <<yG>>.
-Let Mxy := <<xyG>>.
+Let X := <[x]>.
+Let Y := <[y]>.
+Let yG := y ^: G.
+Let xyG := (x × y) ^: G.
+Let My := <<yG>>.
+Let Mxy := <<xyG>>.

Theorem dihedral2_structure :
-    n > 1 → extremal_generators G 2 n (x, y) → G \isog 'D_m →
-  [/\ [/\ X ><| Y = G, {in G :\: X, ∀ t, #[t] = 2}
-        & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
-      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
-        & nil_class G = n.-1],
-      'Ohm_1(G) = G ∧ (∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>),
-      [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
-        & ∀ M, maximal M G = pred3 X My Mxy M]
-    & if n == 2 then (2.-abelem G : Prop) else
-  [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
-       My \isog 'D_q, Mxy \isog 'D_q
-     & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+    n > 1 → extremal_generators G 2 n (x, y) → G \isog 'D_m →
+  [/\ [/\ X ><| Y = G, {in G :\: X, ∀ t, #[t] = 2}
+        & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+        & nil_class G = n.-1],
+      'Ohm_1(G) = G ∧ (∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>),
+      [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+        & ∀ M, maximal M G = pred3 X My Mxy M]
+    & if n == 2 then (2.-abelem G : Prop) else
+  [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+       My \isog 'D_q, Mxy \isog 'D_q
+     & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].

Theorem quaternion_structure :
-    n > 2 → extremal_generators G 2 n (x, y) → G \isog 'Q_m →
-  [/\ [/\ pprod X Y = G, {in G :\: X, ∀ t, #[t] = 4}
-        & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
-      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
-        & nil_class G = n.-1],
-      [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
-          ∀ u, u \in G → #[u] = 2 → u = x ^+ r,
-          'Ohm_1(G) = <[x ^+ r]> ∧ 'Ohm_2(G) = G
-         & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
-      [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
-        & ∀ M, maximal M G = pred3 X My Mxy M]
-    & n > 3 →
-     [/\ My \isog 'Q_q, Mxy \isog 'Q_q
-       & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+    n > 2 → extremal_generators G 2 n (x, y) → G \isog 'Q_m →
+  [/\ [/\ pprod X Y = G, {in G :\: X, ∀ t, #[t] = 4}
+        & {in X & G :\: X, ∀ z t, z ^ t = z^-1}],
+      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+        & nil_class G = n.-1],
+      [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+          ∀ u, u \in G → #[u] = 2 → u = x ^+ r,
+          'Ohm_1(G) = <[x ^+ r]> ∧ 'Ohm_2(G) = G
+         & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+      [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+        & ∀ M, maximal M G = pred3 X My Mxy M]
+    & n > 3 →
+     [/\ My \isog 'Q_q, Mxy \isog 'Q_q
+       & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].

Theorem semidihedral_structure :
-    n > 3 → extremal_generators G 2 n (x, y) → G \isog 'SD_m → #[y] = 2 →
-  [/\ [/\ X ><| Y = G, #[x × y] = 4
-        & {in X & G :\: X, ∀ z t, z ^ t = z ^+ r.-1}],
-      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
-        & nil_class G = n.-1],
-      [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
-          'Ohm_1(G) = My ∧ 'Ohm_2(G) = G
-         & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
-      [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
-        & ∀ H, maximal H G = pred3 X My Mxy H]
-    & [/\ My \isog 'D_q, Mxy \isog 'Q_q
-       & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].
+    n > 3 → extremal_generators G 2 n (x, y) → G \isog 'SD_m → #[y] = 2 →
+  [/\ [/\ X ><| Y = G, #[x × y] = 4
+        & {in X & G :\: X, ∀ z t, z ^ t = z ^+ r.-1}],
+      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+        & nil_class G = n.-1],
+      [/\ 'Z(G) = <[x ^+ r]>, #|'Z(G)| = 2,
+          'Ohm_1(G) = My ∧ 'Ohm_2(G) = G
+         & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+      [/\ yG :|: xyG = G :\: X ∧ [disjoint yG & xyG]
+        & ∀ H, maximal H G = pred3 X My Mxy H]
+    & [/\ My \isog 'D_q, Mxy \isog 'Q_q
+       & ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X]].

End ExtremalStructure.
@@ -502,7 +501,7 @@ Section ExtremalClass.

-Variables (gT : finGroupType) (G : {group gT}).
+Variables (gT : finGroupType) (G : {group gT}).

Inductive extremal_group_type :=
@@ -520,11 +519,11 @@
Definition enum_extremal_groups :=
-  [:: ModularGroup; Dihedral; SemiDihedral; Quaternion].
+  [:: ModularGroup; Dihedral; SemiDihedral; Quaternion].

Lemma cancel_index_extremal_groups :
-  cancel index_extremal_group_type (nth NotExtremal enum_extremal_groups).
+  cancel index_extremal_group_type (nth NotExtremal enum_extremal_groups).

Import choice.
@@ -536,76 +535,77 @@ Canonical extremal_group_choiceType := ChoiceType _ extremal_group_choiceMixin.
Definition extremal_group_countMixin := CanCountMixin extgK.
Canonical extremal_group_countType := CountType _ extremal_group_countMixin.
-Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
+Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups.
-Canonical extremal_group_finType := FinType _ extremal_group_finMixin.
+Canonical extremal_group_finType :=
+  FinType extremal_group_type extremal_group_finMixin.

-Definition extremal_class (A : {set gT}) :=
-  let m := #|A| in let p := pdiv m in let n := logn p m in
-  if (n > 1) && (A \isog 'D_(2 ^ n)) then Dihedral else
-  if (n > 2) && (A \isog 'Q_(2 ^ n)) then Quaternion else
-  if (n > 3) && (A \isog 'SD_(2 ^ n)) then SemiDihedral else
-  if (n > 2) && (A \isog 'Mod_(p ^ n)) then ModularGroup else
+Definition extremal_class (A : {set gT}) :=
+  let m := #|A| in let p := pdiv m in let n := logn p m in
+  if (n > 1) && (A \isog 'D_(2 ^ n)) then Dihedral else
+  if (n > 2) && (A \isog 'Q_(2 ^ n)) then Quaternion else
+  if (n > 3) && (A \isog 'SD_(2 ^ n)) then SemiDihedral else
+  if (n > 2) && (A \isog 'Mod_(p ^ n)) then ModularGroup else
  NotExtremal.

-Definition extremal2 A := extremal_class A \in behead enum_extremal_groups.
+Definition extremal2 A := extremal_class A \in behead enum_extremal_groups.

Lemma dihedral_classP :
-  extremal_class G = Dihedral ↔ (exists2 n, n > 1 & G \isog 'D_(2 ^ n)).
+  extremal_class G = Dihedral ↔ (exists2 n, n > 1 & G \isog 'D_(2 ^ n)).

Lemma quaternion_classP :
-  extremal_class G = Quaternion ↔ (exists2 n, n > 2 & G \isog 'Q_(2 ^ n)).
+  extremal_class G = Quaternion ↔ (exists2 n, n > 2 & G \isog 'Q_(2 ^ n)).

Lemma semidihedral_classP :
-  extremal_class G = SemiDihedral ↔ (exists2 n, n > 3 & G \isog 'SD_(2 ^ n)).
+  extremal_class G = SemiDihedral ↔ (exists2 n, n > 3 & G \isog 'SD_(2 ^ n)).

-Lemma odd_not_extremal2 : odd #|G| → ~~ extremal2 G.
+Lemma odd_not_extremal2 : odd #|G| → ~~ extremal2 G.

Lemma modular_group_classP :
-  extremal_class G = ModularGroup
-     ↔ (exists2 p, prime p &
-          exists2 n, n ≥ (p == 2) + 3 & G \isog 'Mod_(p ^ n)).
+  extremal_class G = ModularGroup
+     ↔ (exists2 p, prime p &
+          exists2 n, n ≥ (p == 2) + 3 & G \isog 'Mod_(p ^ n)).

End ExtremalClass.

-Theorem extremal2_structure (gT : finGroupType) (G : {group gT}) n x y :
+Theorem extremal2_structure (gT : finGroupType) (G : {group gT}) n x y :
  let cG := extremal_class G in
-  let m := (2 ^ n)%N in let q := (2 ^ n.-1)%N in let r := (2 ^ n.-2)%N in
-  let X := <[x]> in let yG := y ^: G in let xyG := (x × y) ^: G in
-  let My := <<yG>> in let Mxy := <<xyG>> in
-     extremal_generators G 2 n (x, y) →
-     extremal2 G → (cG == SemiDihedral) ==> (#[y] == 2) →
- [/\ [/\ (if cG == Quaternion then pprod X <[y]> else X ><| <[y]>) = G,
-         if cG == SemiDihedral then #[x × y] = 4 else
-           {in G :\: X, ∀ z, #[z] = (if cG == Dihedral then 2 else 4)},
-         if cG != Quaternion then True else
-         {in G, ∀ z, #[z] = 2 → z = x ^+ r}
-       & {in X & G :\: X, ∀ t z,
-            t ^ z = (if cG == SemiDihedral then t ^+ r.-1 else t^-1)}],
-      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
-        & nil_class G = n.-1],
-      [/\ if n > 2 then 'Z(G) = <[x ^+ r]> ∧ #|'Z(G)| = 2 else 2.-abelem G,
-          'Ohm_1(G) = (if cG == Quaternion then <[x ^+ r]> else
-                       if cG == SemiDihedral then My else G),
-          'Ohm_2(G) = G
-        & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
-     [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
-       & ∀ H : {group gT}, maximal H G = (gval H \in pred3 X My Mxy)]
-   & if n ≤ (cG == Quaternion) + 2 then True else
-     [/\ ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X,
-         if cG == Quaternion then My \isog 'Q_q else My \isog 'D_q,
-         extremal_class My = (if cG == Quaternion then cG else Dihedral),
-         if cG == Dihedral then Mxy \isog 'D_q else Mxy \isog 'Q_q
-       & extremal_class Mxy = (if cG == Dihedral then cG else Quaternion)]].
+  let m := (2 ^ n)%N in let q := (2 ^ n.-1)%N in let r := (2 ^ n.-2)%N in
+  let X := <[x]> in let yG := y ^: G in let xyG := (x × y) ^: G in
+  let My := <<yG>> in let Mxy := <<xyG>> in
+     extremal_generators G 2 n (x, y) →
+     extremal2 G → (cG == SemiDihedral) ==> (#[y] == 2) →
+ [/\ [/\ (if cG == Quaternion then pprod X <[y]> else X ><| <[y]>) = G,
+         if cG == SemiDihedral then #[x × y] = 4 else
+           {in G :\: X, ∀ z, #[z] = (if cG == Dihedral then 2 else 4)},
+         if cG != Quaternion then True else
+         {in G, ∀ z, #[z] = 2 → z = x ^+ r}
+       & {in X & G :\: X, ∀ t z,
+            t ^ z = (if cG == SemiDihedral then t ^+ r.-1 else t^-1)}],
+      [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r
+        & nil_class G = n.-1],
+      [/\ if n > 2 then 'Z(G) = <[x ^+ r]> ∧ #|'Z(G)| = 2 else 2.-abelem G,
+          'Ohm_1(G) = (if cG == Quaternion then <[x ^+ r]> else
+                       if cG == SemiDihedral then My else G),
+          'Ohm_2(G) = G
+        & ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (2 ^ k)]>],
+     [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG]
+       & ∀ H : {group gT}, maximal H G = (gval H \in pred3 X My Mxy)]
+   & if n ≤ (cG == Quaternion) + 2 then True else
+     [/\ ∀ U, cyclic U → U \subset G → #|G : U| = 2 → U = X,
+         if cG == Quaternion then My \isog 'Q_q else My \isog 'D_q,
+         extremal_class My = (if cG == Quaternion then cG else Dihedral),
+         if cG == Dihedral then Mxy \isog 'D_q else Mxy \isog 'Q_q
+       & extremal_class Mxy = (if cG == Dihedral then cG else Quaternion)]].

@@ -614,9 +614,9 @@ This is Aschbacher (23.4).
-Lemma maximal_cycle_extremal gT p (G X : {group gT}) :
-    p.-group G → ~~ abelian G → cyclic X → X \subset G → #|G : X| = p →
-  (extremal_class G == ModularGroup) || (p == 2) && extremal2 G.
+Lemma maximal_cycle_extremal gT p (G X : {group gT}) :
+    p.-group G → ~~ abelian G → cyclic X → X \subset G → #|G : X| = p →
+  (extremal_class G == ModularGroup) || (p == 2) && extremal2 G.

@@ -625,12 +625,12 @@ This is Aschbacher (23.5)
-Lemma cyclic_SCN gT p (G U : {group gT}) :
-    p.-group G → U \in 'SCN(G) → ~~ abelian G → cyclic U →
-    [/\ p = 2, #|G : U| = 2 & extremal2 G]
-∨ ∃ M : {group gT},
-   [/\ M :=: 'C_G('Mho^1(U)), #|M : U| = p, extremal_class M = ModularGroup,
-       'Ohm_1(M)%G \in 'E_p^2(G) & 'Ohm_1(M) \char G].
+Lemma cyclic_SCN gT p (G U : {group gT}) :
+    p.-group G → U \in 'SCN(G) → ~~ abelian G → cyclic U →
+    [/\ p = 2, #|G : U| = 2 & extremal2 G]
+∨ ∃ M : {group gT},
+   [/\ M :=: 'C_G('Mho^1(U)), #|M : U| = p, extremal_class M = ModularGroup,
+       'Ohm_1(M)%G \in 'E_p^2(G) & 'Ohm_1(M) \char G].

@@ -639,9 +639,9 @@ This is Aschbacher, exercise (8.4)
-Lemma normal_rank1_structure gT p (G : {group gT}) :
-    p.-group G → (∀ X : {group gT}, X <| G → abelian X → cyclic X) →
-  cyclic G ∨ [&& p == 2, extremal2 G & (#|G| ≥ 16) || (G \isog 'Q_8)].
+Lemma normal_rank1_structure gT p (G : {group gT}) :
+    p.-group G → (∀ X : {group gT}, X <| G → abelian X → cyclic X) →
+  cyclic G ∨ [&& p == 2, extremal2 G & (#|G| ≥ 16) || (G \isog 'Q_8)].

@@ -650,8 +650,8 @@ Replacement for Section 4 proof.
-Lemma odd_pgroup_rank1_cyclic gT p (G : {group gT}) :
-  p.-group G → odd #|G| → cyclic G = ('r_p(G) ≤ 1).
+Lemma odd_pgroup_rank1_cyclic gT p (G : {group gT}) :
+  p.-group G → odd #|G| → cyclic G = ('r_p(G) ≤ 1).

@@ -660,10 +660,10 @@ This is the second part of Aschbacher, exercise (8.4).
-Lemma prime_Ohm1P gT p (G : {group gT}) :
-    p.-group G → G :!=: 1 →
-  reflect (#|'Ohm_1(G)| = p)
-          (cyclic G || (p == 2) && (extremal_class G == Quaternion)).
+Lemma prime_Ohm1P gT p (G : {group gT}) :
+    p.-group G → G :!=: 1 →
+  reflect (#|'Ohm_1(G)| = p)
+          (cyclic G || (p == 2) && (extremal_class G == Quaternion)).

@@ -672,13 +672,13 @@ This is Aschbacher (23.9)
-Theorem symplectic_type_group_structure gT p (G : {group gT}) :
-    p.-group G → (∀ X : {group gT}, X \char G → abelian X → cyclic X) →
-  exists2 E : {group gT}, E :=: 1 ∨ extraspecial E
-  & ∃ R : {group gT},
-    [/\ cyclic R ∨ [/\ p = 2, extremal2 R & #|R| ≥ 16],
-        E \* R = G
-      & E :&: R = 'Z(E)].
+Theorem symplectic_type_group_structure gT p (G : {group gT}) :
+    p.-group G → (∀ X : {group gT}, X \char G → abelian X → cyclic X) →
+  exists2 E : {group gT}, E :=: 1 ∨ extraspecial E
+  & ∃ R : {group gT},
+    [/\ cyclic R ∨ [/\ p = 2, extremal2 R & #|R| ≥ 16],
+        E \* R = G
+      & E :&: R = 'Z(E)].

End ExtremalTheory.
-- cgit v1.2.3