- -

Library mathcomp.solvable.maximal

- -

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

- -

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

- -

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