Library mathcomp.solvable.maximal

(* (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 choice.
From mathcomp Require Import div fintype finfun bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism quotient.
From mathcomp Require Import action commutator gproduct gfunctor ssralg.
From mathcomp Require Import finalg zmodp cyclic pgroup center gseries.
From mathcomp Require Import nilpotent sylow abelian finmodule.

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)
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)
This encasulates Aschbacher (23.10)(1).
This is the tranposition of the hyperplane dimension theorem (Aschbacher (19.1)) to subgroups of an extraspecial group.
This is the tranposition of the orthogonal subspace dimension theorem (Aschbacher (19.2)) to subgroups of an extraspecial group.
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.
This is B & G, Theorem 4.15, as done in Aschbacher (23.8)
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).
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)
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).
This is Aschbacher 23.15(3); note that this proof does not depend on the maximality of A.
This is Aschbacher 23.16.
This proof of the Thompson critical lemma is adapted from Aschbacher 23.6