Library maximal

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


Import GroupScope.

Section Defs.

Variable gT : finGroupType.
Implicit Types A B D : {set gT}.
Implicit Type 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 Structure 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 : forall G, group_set (Fitting G).

Canonical Structure 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) : subgroup_scope.

Notation "''F' ( G )" := (Fitting G)
  (at level 8, format "''F' ( G )") : group_scope.
Notation "''F' ( G )" := (Fitting_group G) : subgroup_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 : forall G, 'Phi(G) \subset G.

Lemma Phi_sub_max : forall G M, maximal M G -> 'Phi(G) \subset M.

Lemma Phi_proper : forall G, G :!=: 1 -> 'Phi(G) \proper G.

Lemma Phi_nongen : forall G X, 'Phi(G) <*> X = G -> <<X>> = G.

Lemma Frattini_cont : forall (rT : finGroupType) G (f : {morphism G >-> rT}),
  f @* 'Phi(G) \subset 'Phi(f @* G).

End Frattini.

Canonical Structure Frattini_igFun := [igFun by Phi_sub & Frattini_cont].
Canonical Structure Frattini_gFun := [gFun by Frattini_cont].

Section Frattini0.

Variable gT : finGroupType.
Implicit Type rT : finGroupType.
Implicit Types D G : {group gT}.

Lemma Phi_char : forall G, 'Phi(G) \char G.

Lemma Phi_normal : forall G, 'Phi(G) <| G.

Lemma injm_Phi : forall rT D G (f : {morphism D >-> rT}),
  'injm f -> G \subset D -> f @* 'Phi(G) = 'Phi(f @* G).

Lemma isog_Phi : forall rT G (H : {group rT}),
  G \isog H -> 'Phi(G) \isog 'Phi(H).

Lemma PhiJ : forall G x, 'Phi(G :^ x) = 'Phi(G) :^ x.

End Frattini0.

Section Frattini2.

Variables gT : finGroupType.
Implicit Type G : {group gT}.

Lemma Phi_quotient_id : forall G, 'Phi (G / 'Phi(G)) = 1.

Lemma Phi_quotient_cyclic : forall 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).

End Frattini3.

Section Frattini4.

Variables (p : nat) (gT : finGroupType).
Implicit Type rT : finGroupType.
Implicit Types P G H K D : {group gT}.

Lemma PhiS : forall G H, p.-group H -> G \subset H -> 'Phi(G) \subset 'Phi(H).

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

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

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

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

Lemma Phi_mulg : forall H K,
    p.-group H -> p.-group K -> K \subset 'C(H) ->
  'Phi(H * K) = 'Phi(H) * 'Phi(K).

End Frattini4.

Section Simple.

Implicit Types gT rT : finGroupType.

Lemma charsimpleP : forall gT (G : {group gT}),
   reflect
     (G :!=: 1 /\ forall K : {group gT}, K :!=: 1 -> K \char G -> K :=: G)
     (charsimple G).

End Simple.

Section Fitting.

Variable gT : finGroupType.
Implicit Types G H : {group gT}.

Lemma Fitting_normal : forall G, 'F(G) <| G.

Lemma Fitting_sub : forall G, 'F(G) \subset G.

Lemma Fitting_nil : forall G, nilpotent 'F(G).

Lemma Fitting_max : forall G H, H <| G -> nilpotent H -> H \subset 'F(G).

Lemma pcore_Fitting : forall pi G, 'O_pi('F(G)) \subset 'O_pi(G).

Lemma p_core_Fitting : forall (p : nat) G, 'O_p('F(G)) = 'O_p(G).

Lemma nilpotent_Fitting : forall G, nilpotent G -> 'F(G) = G.

Lemma Fitting_eq_pcore : forall (p : nat) G, 'O_p^'(G) = 1 -> 'F(G) = 'O_p(G).

Lemma FittingEgen : forall 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 : forall gT (G H : {group gT}),
  H \subset G -> H :&: 'F(G) \subset 'F(H).

Lemma FittingJ : forall gT (G : {group gT}) x, 'F(G :^ x) = 'F(G) :^ x.

End FittingFun.

Canonical Structure Fitting_igFun := [igFun by Fitting_sub & morphim_Fitting].
Canonical Structure Fitting_gFun := [gFun by morphim_Fitting].
Canonical Structure 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 : forall H : {group rT}, G \isog H -> 'F(G) \isog 'F(H).

End IsoFitting.

Section CharSimple.

Variable gT : finGroupType.
Implicit Type rT : finGroupType.
Implicit Types G H K L : {group gT}.

Lemma minnormal_charsimple : forall G H, minnormal H G -> charsimple H.

Lemma maxnormal_charsimple : forall G H L,
  G <| L -> maxnormal H G L -> charsimple (G / H).

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

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

Lemma abelem_charsimple : forall (p : nat) G,
  p.-abelem G -> G :!=: 1 -> charsimple G.

Lemma charsimple_dprod : forall G, charsimple G ->
  exists 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 : forall G, solvable G -> simple G -> prime #|G|.

Lemma charsimple_solvable : forall G,
  charsimple G -> solvable G -> is_abelem G.

Lemma minnormal_solvable : forall L G H : {group gT},
  minnormal H L -> H \subset G -> solvable G ->
  [/\ L \subset 'N(H), H :!=: 1 & is_abelem H].

Lemma solvable_norm_abelem : forall L G,
  solvable G -> G <| L -> G :!=: 1 ->
  exists H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].

Lemma trivg_Fitting : forall G, solvable G -> ('F(G) == 1) = (G :==: 1).

Lemma Fitting_pcore : forall 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 : forall 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}).

 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 : forall E,
  prime p -> #|E| = (p ^ 3)%N -> #|'Z(E)| = p -> extraspecial E.

Lemma p3group_extraspecial : forall G,
  p.-group G -> ~~ abelian G -> logn p #|G| <= 3 -> extraspecial G.

Lemma extraspecial_nonabelian : forall G, extraspecial G -> ~~ abelian G.

Lemma exponent_2extraspecial : forall G,
  2.-group G -> extraspecial G -> exponent G = 4.

Lemma injm_special : forall D G (f : {morphism D >-> rT}),
  'injm f -> G \subset D -> special G -> special (f @* G).

Lemma injm_extraspecial : forall D G (f : {morphism D >-> rT}),
  'injm f -> G \subset D -> extraspecial G -> extraspecial (f @* G).

Lemma isog_special : forall G (R : {group rT}),
  G \isog R -> special G -> special R.

Lemma isog_extraspecial : forall G (R : {group rT}),
  G \isog R -> extraspecial G -> extraspecial R.

Lemma cprod_extraspecial : forall 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).


 This encasulates Aschbacher (23.10)(1). 
Lemma cent1_extraspecial_maximal : forall 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 : forall 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 : forall 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 : forall 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 : forall 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 : forall 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).


 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 : forall k, coprime k p ->
  exists2 f, f \in Aut S & forall 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 Type A Z H : {group gT}.

Lemma SCN_P : forall A, reflect (A <| G /\ 'C_G(A) = A) (A \in 'SCN(G)).

Lemma SCN_abelian : forall A, A \in 'SCN(G) -> abelian A.

Lemma exponent_Ohm1_class2 : forall 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 : forall A, A \in 'SCN(G) -> [max A | (A <| G) && abelian A].

Lemma max_SCN : forall 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 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 : forall Z,
    odd p -> p.-group G -> [max Z | (Z <| G) && p.-abelem Z] ->
  'Ohm_1('C_G(Z)) = Z.

Lemma critical_class2 : forall 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 : forall H,
  critical H G -> p.-group G -> p.-group 'C(H | [Aut G]).

End SCN.

Implicit Arguments SCN_P [gT G A].