+ +

Library mathcomp.solvable.maximal

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ This file establishes basic properties of several important classes of + maximal subgroups: maximal, max and min normal, simple, characteristically + simple subgroups, the Frattini and Fitting subgroups, the Thompson + critical subgroup, special and extra-special groups, and self-centralising + normal (SCN) subgroups. In detail, we define: + charsimple G == G is characteristically simple (it has no nontrivial + characteristic subgroups, and is nontrivial) + 'Phi(G) == the Frattini subgroup of G, i.e., the intersection of + all its maximal proper subgroups. + 'F(G) == the Fitting subgroup of G, i.e., the largest normal + nilpotent subgroup of G (defined as the (direct) + product of all the p-cores of G). + critical C G == C is a critical subgroup of G: C is characteristic + (but not functorial) in G, the center of C contains + both its Frattini subgroup and the commutator [G, C], + and is equal to the centraliser of C in G. The + Thompson_critical theorem provides critical subgroups + for p-groups; we also show that in this case the + centraliser of C in Aut G is a p-group as well. + special G == G is a special group: its center, Frattini, and + derived sugroups coincide (we follow Aschbacher in + not considering nontrivial elementary abelian groups + as special); we show that a p-group factors under + coprime action into special groups (Aschbacher 24.7). + extraspecial G == G is a special group whose center has prime order + (hence G is non-abelian). + 'SCN(G) == the set of self-centralising normal abelian subgroups + of G (the A <| G such that 'C_G(A) = A). + 'SCN_n(G) == the subset of 'SCN(G) containing all groups with rank + at least n (i.e., A \in 'SCN(G) and 'm(A) >= n). +

+ +
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section Defs.
+ +
+Variable gT : finGroupType.
+Implicit Types (A B D : {set gT }) (G : {group gT }).
+ +
+Definition charsimple A := [min A of G | G :!=: 1 & G \char A ].
+ +
+Definition Frattini A := \bigcap_(G : {group gT } | maximal_eq G A ) G.
+ +
+Canonical Frattini_group A : {group gT } := Eval hnf in [group of Frattini A ].
+ +
+Definition Fitting A := \big [dprod /1]_(p <- primes #|A |) 'O_p (A ).
+ +
+Lemma Fitting_group_set G : group_set (Fitting G).
+ +
+Canonical Fitting_group G := group (Fitting_group_set G).
+ +
+Definition critical A B :=
+  [/\ A \char B ,
+      Frattini A \subset 'Z (A ),
+      [~: B , A ] \subset 'Z (A )
+   & 'C_B (A ) = 'Z (A )].
+ +
+Definition special A := Frattini A = 'Z (A ) ∧ A ^`(1) = 'Z (A ).
+ +
+Definition extraspecial A := special A ∧ prime #|'Z (A )|.
+ +
+Definition SCN B := [set A : {group gT } | A <| B & 'C_B (A ) == A ].
+ +
+Definition SCN_at n B := [set A in SCN B | n ≤ 'r (A )].
+ +
+End Defs.
+ +
+ +
+ +
+Notation "''Phi' ( A )" := (Frattini A)
+  (at level 8, format "''Phi' ( A )") : group_scope.
+Notation "''Phi' ( G )" := (Frattini_group G) : Group_scope.
+ +
+Notation "''F' ( G )" := (Fitting G)
+  (at level 8, format "''F' ( G )") : group_scope.
+Notation "''F' ( G )" := (Fitting_group G) : Group_scope.
+ +
+Notation "''SCN' ( B )" := (SCN B)
+  (at level 8, format "''SCN' ( B )") : group_scope.
+Notation "''SCN_' n ( B )" := (SCN_at n B)
+  (at level 8, n at level 2, format "''SCN_' n ( B )") : group_scope.
+ +
+Section PMax.
+ +
+Variables (gT : finGroupType) (p : nat) (P M : {group gT }).
+Hypothesis pP : p .-group P.
+ +
+Lemma p_maximal_normal : maximal M P → M <| P.
+ +
+Lemma p_maximal_index : maximal M P → #|P : M | = p.
+ +
+Lemma p_index_maximal : M \subset P → prime #|P : M | → maximal M P.
+ +
+End PMax.
+ +
+Section Frattini.
+ +
+Variables gT : finGroupType.
+Implicit Type G M : {group gT }.
+ +
+Lemma Phi_sub G : 'Phi (G ) \subset G.
+ +
+Lemma Phi_sub_max G M : maximal M G → 'Phi (G ) \subset M.
+ +
+Lemma Phi_proper G : G :!=: 1 → 'Phi (G ) \proper G.
+ +
+Lemma Phi_nongen G X : 'Phi (G ) <*> X = G → <<X >> = G.
+ +
+Lemma Frattini_continuous (rT : finGroupType) G (f : {morphism G >-> rT }) :
+  f @* 'Phi (G ) \subset 'Phi (f @* G ).
+ +
+End Frattini.
+ +
+Canonical Frattini_igFun := [igFun by Phi_sub & Frattini_continuous ].
+Canonical Frattini_gFun := [gFun by Frattini_continuous ].
+ +
+Section Frattini0.
+ +
+Variable gT : finGroupType.
+Implicit Types (rT : finGroupType) (D G : {group gT }).
+ +
+Lemma Phi_char G : 'Phi (G ) \char G.
+ +
+Lemma Phi_normal G : 'Phi (G ) <| G.
+ +
+Lemma injm_Phi rT D G (f : {morphism D >-> rT }) :
+  'injm f → G \subset D → f @* 'Phi (G ) = 'Phi (f @* G ).
+ +
+Lemma isog_Phi rT G (H : {group rT }) : G \isog H → 'Phi (G ) \isog 'Phi (H ).
+ +
+Lemma PhiJ G x : 'Phi (G :^ x ) = 'Phi (G ) :^ x.
+ +
+End Frattini0.
+ +
+Section Frattini2.
+ +
+Variables gT : finGroupType.
+Implicit Type G : {group gT }.
+ +
+Lemma Phi_quotient_id G : 'Phi (G / 'Phi (G )) = 1.
+ +
+Lemma Phi_quotient_cyclic G : cyclic (G / 'Phi (G )) → cyclic G.
+ +
+Variables (p : nat) (P : {group gT }).
+ +
+Lemma trivg_Phi : p .-group P → ('Phi (P ) == 1) = p .-abelem P.
+ +
+End Frattini2.
+ +
+Section Frattini3.
+ +
+Variables (gT : finGroupType) (p : nat) (P : {group gT }).
+Hypothesis pP : p .-group P.
+ +
+Lemma Phi_quotient_abelem : p .-abelem (P / 'Phi (P )).
+ +
+Lemma Phi_joing : 'Phi (P ) = P ^`(1) <*> 'Mho ^1(P ).
+ +
+Lemma Phi_Mho : abelian P → 'Phi (P ) = 'Mho ^1(P ).
+ +
+End Frattini3.
+ +
+Section Frattini4.
+ +
+Variables (p : nat) (gT : finGroupType).
+Implicit Types (rT : finGroupType) (P G H K D : {group gT }).
+ +
+Lemma PhiS G H : p .-group H → G \subset H → 'Phi (G ) \subset 'Phi (H ).
+ +
+Lemma morphim_Phi rT P D (f : {morphism D >-> rT }) :
+  p .-group P → P \subset D → f @* 'Phi (P ) = 'Phi (f @* P ).
+ +
+Lemma quotient_Phi P H :
+  p .-group P → P \subset 'N (H ) → 'Phi (P ) / H = 'Phi (P / H ).
+ +
+

+ +

+ This is Aschbacher (23.2) +

+Lemma Phi_min G H :
+  p .-group G → G \subset 'N (H ) → p .-abelem (G / H) → 'Phi (G ) \subset H.
+ +
+Lemma Phi_cprod G H K :
+  p .-group G → H \* K = G → 'Phi (H ) \* 'Phi (K ) = 'Phi (G ).
+ +
+Lemma Phi_mulg H K :
+    p .-group H → p .-group K → K \subset 'C (H ) →
+  'Phi (H × K ) = 'Phi (H ) × 'Phi (K ).
+ +
+Lemma charsimpleP G :
+  reflect (G :!=: 1 ∧ ∀ K, K :!=: 1 → K \char G → K :=: G)
+          (charsimple G).
+ +
+End Frattini4.
+ +
+Section Fitting.
+ +
+Variable gT : finGroupType.
+Implicit Types (p : nat) (G H : {group gT }).
+ +
+Lemma Fitting_normal G : 'F (G ) <| G.
+ +
+Lemma Fitting_sub G : 'F (G ) \subset G.
+ +
+Lemma Fitting_nil G : nilpotent 'F (G ).
+ +
+Lemma Fitting_max G H : H <| G → nilpotent H → H \subset 'F (G ).
+ +
+Lemma pcore_Fitting pi G : 'O_pi ('F (G )) \subset 'O_pi (G ).
+ +
+Lemma p_core_Fitting p G : 'O_p ('F (G )) = 'O_p (G ).
+ +
+Lemma nilpotent_Fitting G : nilpotent G → 'F (G ) = G.
+ +
+Lemma Fitting_eq_pcore p G : 'O_p ^'(G ) = 1 → 'F (G ) = 'O_p (G ).
+ +
+Lemma FittingEgen G :
+  'F (G ) = <<\bigcup_(p < #|G |.+1 | (p : nat ) \in \pi (G )) 'O_p (G )>>.
+ +
+End Fitting.
+ +
+Section FittingFun.
+ +
+Implicit Types gT rT : finGroupType.
+ +
+Lemma morphim_Fitting : GFunctor.pcontinuous Fitting.
+ +
+Lemma FittingS gT (G H : {group gT }) : H \subset G → H :&: 'F (G ) \subset 'F (H ).
+ +
+Lemma FittingJ gT (G : {group gT }) x : 'F (G :^ x ) = 'F (G ) :^ x.
+ +
+End FittingFun.
+ +
+Canonical Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting ].
+Canonical Fitting_gFun := [gFun by morphim_Fitting ].
+Canonical Fitting_pgFun := [pgFun by morphim_Fitting ].
+ +
+Section IsoFitting.
+ +
+Variables (gT rT : finGroupType) (G D : {group gT }) (f : {morphism D >-> rT }).
+ +
+Lemma Fitting_char : 'F (G ) \char G.
+ +
+Lemma injm_Fitting : 'injm f → G \subset D → f @* 'F (G ) = 'F (f @* G ).
+ +
+Lemma isog_Fitting (H : {group rT }) : G \isog H → 'F (G ) \isog 'F (H ).
+ +
+End IsoFitting.
+ +
+Section CharSimple.
+ +
+Variable gT : finGroupType.
+Implicit Types (rT : finGroupType) (G H K L : {group gT }) (p : nat).
+ +
+Lemma minnormal_charsimple G H : minnormal H G → charsimple H.
+ +
+Lemma maxnormal_charsimple G H L :
+  G <| L → maxnormal H G L → charsimple (G / H).
+ +
+Lemma abelem_split_dprod rT p (A B : {group rT }) :
+  p .-abelem A → B \subset A → ∃ C : {group rT }, B \x C = A.
+ +
+Lemma p_abelem_split1 rT p (A : {group rT }) x :
+     p .-abelem A → x \in A →
+  ∃ B : {group rT }, [/\ B \subset A , #|B | = #|A | %/ #[x ] & <[x ]> \x B = A ].
+ +
+Lemma abelem_charsimple p G : p .-abelem G → G :!=: 1 → charsimple G.
+ +
+Lemma charsimple_dprod G : charsimple G →
+  ∃ H : {group gT }, [/\ H \subset G , simple H
+                         & exists2 I : {set {perm gT }}, I \subset Aut G
+                         & \big [dprod /1]_(f in I ) f @: H = G ].
+ +
+Lemma simple_sol_prime G : solvable G → simple G → prime #|G |.
+ +
+Lemma charsimple_solvable G : charsimple G → solvable G → is_abelem G.
+ +
+Lemma minnormal_solvable L G H :
+    minnormal H L → H \subset G → solvable G →
+  [/\ L \subset 'N (H ), H :!=: 1 & is_abelem H ].
+ +
+Lemma solvable_norm_abelem L G :
+    solvable G → G <| L → G :!=: 1 →
+  ∃ H : {group gT }, [/\ H \subset G , H <| L , H :!=: 1 & is_abelem H ].
+ +
+Lemma trivg_Fitting G : solvable G → ('F (G ) == 1) = (G :==: 1).
+ +
+Lemma Fitting_pcore pi G : 'F ('O_pi (G )) = 'O_pi ('F (G )).
+ +
+End CharSimple.
+ +
+Section SolvablePrimeFactor.
+ +
+Variables (gT : finGroupType) (G : {group gT }).
+ +
+Lemma index_maxnormal_sol_prime (H : {group gT }) :
+  solvable G → maxnormal H G G → prime #|G : H |.
+ +
+Lemma sol_prime_factor_exists :
+  solvable G → G :!=: 1 → {H : {group gT } | H <| G & prime #|G : H | }.
+ +
+End SolvablePrimeFactor.
+ +
+Section Special.
+ +
+Variables (gT : finGroupType) (p : nat) (A G : {group gT }).
+ +
+

+ +

+ This is Aschbacher (23.7) +

+Lemma center_special_abelem : p .-group G → special G → p .-abelem 'Z (G ).
+ +
+Lemma exponent_special : p .-group G → special G → exponent G %| p ^ 2.
+ +
+

+ +

+ Aschbacher 24.7 (replaces Gorenstein 5.3.7) +

+Theorem abelian_charsimple_special :
+    p .-group G → coprime #|G | #|A | → [~: G , A ] = G →
+    \bigcup_(H : {group gT } | (H \char G ) && abelian H ) H \subset 'C (A ) →
+  special G ∧ 'C_G (A ) = 'Z (G ).
+ +
+End Special.
+ +
+Section Extraspecial.
+ +
+Variables (p : nat) (gT rT : finGroupType).
+Implicit Types D E F G H K M R S T U : {group gT }.
+ +
+Section Basic.
+ +
+Variable S : {group gT }.
+Hypotheses (pS : p .-group S) (esS : extraspecial S).
+ +
+Let pZ : p .-group 'Z (S ) := pgroupS (center_sub S) pS.
+Lemma extraspecial_prime : prime p.
+ +
+Lemma card_center_extraspecial : #|'Z (S )| = p.
+ +
+Lemma min_card_extraspecial : #|S | ≥ p ^ 3.
+ +
+End Basic.
+ +
+Lemma card_p3group_extraspecial E :
+  prime p → #|E | = (p ^ 3)%N → #|'Z (E )| = p → extraspecial E.
+ +
+Lemma p3group_extraspecial G :
+  p .-group G → ~~ abelian G → logn p #|G | ≤ 3 → extraspecial G.
+ +
+Lemma extraspecial_nonabelian G : extraspecial G → ~~ abelian G.
+ +
+Lemma exponent_2extraspecial G : 2.-group G → extraspecial G → exponent G = 4.
+ +
+Lemma injm_special D G (f : {morphism D >-> rT }) :
+  'injm f → G \subset D → special G → special (f @* G).
+ +
+Lemma injm_extraspecial D G (f : {morphism D >-> rT }) :
+  'injm f → G \subset D → extraspecial G → extraspecial (f @* G).
+ +
+Lemma isog_special G (R : {group rT }) :
+  G \isog R → special G → special R.
+ +
+Lemma isog_extraspecial G (R : {group rT }) :
+  G \isog R → extraspecial G → extraspecial R.
+ +
+Lemma cprod_extraspecial G H K :
+    p .-group G → H \* K = G → H :&: K = 'Z (H ) →
+  extraspecial H → extraspecial K → extraspecial G.
+ +
+

+ +

+ Lemmas bundling Aschbacher (23.10) with (19.1), (19.2), (19.12) and (20.8) +

+Section ExtraspecialFormspace.
+ +
+Variable G : {group gT }.
+Hypotheses (pG : p .-group G) (esG : extraspecial G).
+ +
+Let p_pr := extraspecial_prime pG esG.
+Let oZ := card_center_extraspecial pG esG.
+Let p_gt1 := prime_gt1 p_pr.
+Let p_gt0 := prime_gt0 p_pr.
+ +
+

+ +

+ This encasulates Aschbacher (23.10)(1). +

+Lemma cent1_extraspecial_maximal x :
+ x \in G → x \notin 'Z (G ) → maximal 'C_G [x ] G.
+ +
+

+ +

+ This is the tranposition of the hyperplane dimension theorem (Aschbacher + (19.1)) to subgroups of an extraspecial group. +

+Lemma subcent1_extraspecial_maximal U x :
+ U \subset G → x \in G :\: 'C (U ) → maximal 'C_U [x ] U.
+ +
+

+ +

+ This is the tranposition of the orthogonal subspace dimension theorem + (Aschbacher (19.2)) to subgroups of an extraspecial group. +

+Lemma card_subcent_extraspecial U :
+ U \subset G → #|'C_G (U )| = (#|'Z (G ) :&: U | × #|G : U |)%N.
+ +
+

+ +

+ This is the tranposition of the proof that a singular vector is contained + in a hyperbolic plane (Aschbacher (19.12)) to subgroups of an extraspecial + group. +

+Lemma split1_extraspecial x :
+    x \in G :\: 'Z (G ) →
+  {E : {group gT } & {R : {group gT } |
+    [/\ #|E | = (p ^ 3)%N ∧ #|R | = #|G | %/ p ^ 2,
+        E \* R = G ∧ E :&: R = 'Z (E ),
+        'Z (E ) = 'Z (G ) ∧ 'Z (R ) = 'Z (G ),
+        extraspecial E ∧ x \in E
+      & if abelian R then R :=: 'Z (G ) else extraspecial R ]}}.
+ +
+

+ +

+ This is the tranposition of the proof that the dimension of any maximal + totally singular subspace is equal to the Witt index (Aschbacher (20.8)), + to subgroups of an extraspecial group (in a slightly more general form, + since we allow for p != 2). + Note that Aschbacher derives this from the Witt lemma, which we avoid. +

+Lemma pmaxElem_extraspecial : 'E ×_p (G ) = 'E_p ^('r_p (G ))(G ).
+ +
+End ExtraspecialFormspace.
+ +
+

+ +

+ This is B & G, Theorem 4.15, as done in Aschbacher (23.8) +

+Lemma critical_extraspecial R S :
+ p .-group R → S \subset R → extraspecial S → [~: S , R ] \subset S ^`(1) →
+ S \* 'C_R (S ) = R.
+ +
+

+ +

+ This is part of Aschbacher (23.13) and (23.14). +

+Theorem extraspecial_structure S : p .-group S → extraspecial S →
+ {Es | all (fun E ⇒ (#|E | == p ^ 3)%N && ('Z (E ) == 'Z (S ))) Es
+ & \big [cprod /1%g]_(E <- Es ) E \* 'Z (S ) = S }.
+ +
+Section StructureCorollaries.
+ +
+Variable S : {group gT }.
+Hypotheses (pS : p .-group S) (esS : extraspecial S).
+ +
+Let p_pr := extraspecial_prime pS esS.
+Let oZ := card_center_extraspecial pS esS.
+ +
+

+ +

+ This is Aschbacher (23.10)(2). +

+Lemma card_extraspecial : {n | n > 0 & #|S | = (p ^ n .*2 .+1)%N}.
+ +
+Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z (S ) \isog Aut 'Z (S ).
+ +
+

+ +

+ These are the parts of Aschbacher (23.12) and exercise 8.5 that are later + used in Aschbacher (34.9), which itself replaces the informal discussion + quoted from Gorenstein in the proof of B & G, Theorem 2.5. +

+Lemma center_aut_extraspecial k : coprime k p →
+ exists2 f, f \in Aut S & ∀ z, z \in 'Z (S ) → f z = (z ^+ k)%g.
+ +
+End StructureCorollaries.
+ +
+End Extraspecial.
+ +
+Section SCN.
+ +
+Variables (gT : finGroupType) (p : nat) (G : {group gT }).
+Implicit Types A Z H : {group gT }.
+ +
+Lemma SCN_P A : reflect (A <| G ∧ 'C_G (A ) = A) (A \in 'SCN (G )).
+ +
+Lemma SCN_abelian A : A \in 'SCN (G ) → abelian A.
+ +
+Lemma exponent_Ohm1_class2 H :
+ odd p → p .-group H → nil_class H ≤ 2 → exponent 'Ohm_1 (H ) %| p.
+ +
+

+ +

+ SCN_max and max_SCN cover Aschbacher 23.15(1) +

+Lemma SCN_max A : A \in 'SCN (G ) → [max A | A <| G & abelian A ].
+ +
+Lemma max_SCN A :
+ p .-group G → [max A | A <| G & abelian A ] → A \in 'SCN (G ).
+ +
+

+ +

+ The two other assertions of Aschbacher 23.15 state properties of the + normal series 1 <| Z = 'Ohm_1(A) <| A with A \in 'SCN(G). +

+ +
+Section SCNseries.
+ +
+Variables A : {group gT }.
+Hypothesis SCN_A : A \in 'SCN (G ).
+ +
+Let Z := 'Ohm_1 (A ).
+Let cAA := SCN_abelian SCN_A.
+Let sZA: Z \subset A := Ohm_sub 1 A.
+Let nZA : A \subset 'N (Z ) := sub_abelian_norm cAA sZA.
+ +
+

+ +

+ This is Aschbacher 23.15(2). +

+Lemma der1_stab_Ohm1_SCN_series : ('C (Z ) :&: 'C_G (A / Z | 'Q ))^`(1) \subset A.
+ +
+

+ +

+ This is Aschbacher 23.15(3); note that this proof does not depend on the + maximality of A. +

+Lemma Ohm1_stab_Ohm1_SCN_series :
+ odd p → p .-group G → 'Ohm_1 ('C_G (Z )) \subset 'C_G (A / Z | 'Q ).
+ +
+End SCNseries.
+ +
+

+ +

+ This is Aschbacher 23.16. +

+Lemma Ohm1_cent_max_normal_abelem Z :
+ odd p → p .-group G → [max Z | Z <| G & p .-abelem Z ] → 'Ohm_1 ('C_G (Z )) = Z.
+ +
+Lemma critical_class2 H : critical H G → nil_class H ≤ 2.
+ +
+

+ +

+ This proof of the Thompson critical lemma is adapted from Aschbacher 23.6 +

+Lemma Thompson_critical : p .-group G → {K : {group gT } | critical K G }.
+ +
+Lemma critical_p_stab_Aut H :
+ critical H G → p .-group G → p .-group 'C (H | [Aut G ]).
+ +
+End SCN.
+ +
+