(Joint Center)Library MathComp.maximal

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice div fintype.
Require Import finfun bigop finset prime binomial fingroup morphism perm.
Require Import automorphism quotient action commutator gproduct gfunctor.
Require Import ssralg finalg zmodp cyclic pgroup center gseries.
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 PM <| P.

Lemma p_maximal_index : maximal M P#|P : M| = p.

Lemma p_index_maximal : M \subset Pprime #|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 fG \subset Df @* '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 HG \subset H'Phi(G) \subset 'Phi(H).

Lemma morphim_Phi rT P D (f : {morphism D >-> rT}) :
  p.-group PP \subset Df @* 'Phi(P) = 'Phi(f @* P).

Lemma quotient_Phi P H :
  p.-group PP \subset 'N(H)'Phi(P) / H = 'Phi(P / H).

This is Aschbacher (23.2)
Lemma Phi_min G H :
  p.-group GG \subset 'N(H)p.-abelem (G / H) → 'Phi(G) \subset H.

Lemma Phi_cprod G H K :
  p.-group GH \* K = G'Phi(H) \* 'Phi(K) = 'Phi(G).

Lemma Phi_mulg H K :
    p.-group Hp.-group KK \subset 'C(H)
  'Phi(H × K) = 'Phi(H) × 'Phi(K).

Lemma charsimpleP G :
  reflect (G :!=: 1 K, K :!=: 1 → K \char GK :=: 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 <| Gnilpotent HH \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 GH :&: '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 fG \subset Df @* '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 Gcharsimple H.

Lemma maxnormal_charsimple G H L :
  G <| Lmaxnormal H G Lcharsimple (G / H).

Lemma abelem_split_dprod rT p (A B : {group rT}) :
  p.-abelem AB \subset A C : {group rT}, B \x C = A.

Lemma p_abelem_split1 rT p (A : {group rT}) x :
     p.-abelem Ax \in A
   B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].

Lemma abelem_charsimple p G : p.-abelem GG :!=: 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 Gsimple Gprime #|G|.

Lemma charsimple_solvable G : charsimple Gsolvable Gis_abelem G.

Lemma minnormal_solvable L G H :
    minnormal H LH \subset Gsolvable G
  [/\ L \subset 'N(H), H :!=: 1 & is_abelem H].

Lemma solvable_norm_abelem L G :
    solvable GG <| LG :!=: 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 Gmaxnormal H G Gprime #|G : H|.

Lemma sol_prime_factor_exists :
  solvable GG :!=: 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 Gcoprime #|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)| = pextraspecial E.

Lemma p3group_extraspecial G :
  p.-group G~~ abelian Glogn p #|G| 3 → extraspecial G.

Lemma extraspecial_nonabelian G : extraspecial G~~ abelian G.

Lemma exponent_2extraspecial G : 2.-group Gextraspecial Gexponent G = 4.

Lemma injm_special D G (f : {morphism D >-> rT}) :
  'injm fG \subset Dspecial Gspecial (f @* G).

Lemma injm_extraspecial D G (f : {morphism D >-> rT}) :
  'injm fG \subset Dextraspecial Gextraspecial (f @* G).

Lemma isog_special G (R : {group rT}) :
  G \isog Rspecial Gspecial R.

Lemma isog_extraspecial G (R : {group rT}) :
  G \isog Rextraspecial Gextraspecial R.

Lemma cprod_extraspecial G H K :
    p.-group GH \* K = GH :&: K = 'Z(H)
  extraspecial Hextraspecial Kextraspecial 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)
Lemma critical_extraspecial R S :
    p.-group RS \subset Rextraspecial 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 Sextraspecial 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 pp.-group Hnil_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).
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
Lemma Thompson_critical : p.-group G{K : {group gT} | critical K G}.

Lemma critical_p_stab_Aut H :
  critical H Gp.-group Gp.-group 'C(H | [Aut G]).

End SCN.

Implicit Arguments SCN_P [gT G A].