(Joint Center)Library BGsection1

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div fintype.
Require Import bigop prime binomial finset fingroup morphism perm automorphism.
Require Import quotient action gproduct gfunctor commutator.
Require Import ssralg finalg zmodp cyclic center pgroup finmodule gseries.
Require Import nilpotent sylow abelian maximal hall extremal.
Require Import matrix mxalgebra mxrepresentation mxabelem.

This file contains most of the material in B & G, section 1, including the definitions: p.-length_1 G == the upper p-series of G has length <= 1, i.e., 'O_{p^',p,p^'}(G) = G p_elt_gen p G == the subgroup of G generated by its p-elements. This file currently covers B & G 1.3-4, 1.6, 1.8-1.21, and also Gorenstein 8.1.3 and 2.8.1 (maximal order of a p-subgroup of GL(2,p)). This file also provides, mostly for future reference, the following definitions, drawn from Gorenstein, Chapter 8, and B & G, Appendix B: p.-constrained G <-> the p',p core of G contains the centralisers of all its Sylow p-subgroups. The Hall-Higman Lemma 1.2.3 (B & G, 1.15a) asserts that this holds for all solvable groups. p.-stable G <-> a rather group theoretic generalization of the Hall-Higman type condition that in a faithful p-modular linear representation of G no p-element has a quadratic minimal polynomial, to groups G with a non-trivial p-core. p.-abelian_constrained <-> the p',p core of G contains all the normal abelian subgroups of the Sylow p-subgroups of G. It is via this property and the ZL theorem (the substitute for the ZJ theorem) that the p-stability of groups of odd order is exploited in the proof of the Odd Order Theorem. generated_by p G == G is generated by a set of subgroups satisfying p : pred {group gT} norm_abelian X A == A is abelian and normalised by X. p_norm_abelian p X A == A is an abelian p-group normalised by X. 'L_ [G](X) == the group generated by the abelian subgroups of G normalized by X. 'L_{n}(G) == the Puig group series, defined by the recurrence 'L_{0}(G) = 1, 'L_{n.+1}(G) = 'L_ [G]('L_{n}(G)). 'L_*(G) == the lower limit of the Puig series. 'L(G) == the Puig subgroup: the upper limit of the Puig series: 'L(G) = 'L_ [G]('L_*(G)) and conversely. The following notation is used locally here and in AppendixB, but is NOT exported: D --> G == G is generated by abelian groups normalised by D := generated_by (norm_abelian D) G

Set Implicit Arguments.

Import GroupScope.

Section Definitions.

Variables (n : nat) (gT : finGroupType).
Implicit Type p : nat.

Definition plength_1 p (G : {set gT}) := 'O_{p^', p, p^'}(G) == G.

Definition p_elt_gen p (G : {set gT}) := <<[set x in G | p.-elt x]>>.

Definition p_constrained p (G : {set gT}) :=
   P : {group gT},
    p.-Sylow('O_{p^',p}(G)) P
  'C_G(P) \subset 'O_{p^',p}(G).

Definition p_abelian_constrained p (G : {set gT}) :=
   S A : {group gT},
    p.-Sylow(G) Sabelian AA <| S
  A \subset 'O_{p^',p}(G).

Definition p_stable p (G : {set gT}) :=
   P A : {group gT},
     p.-group P'O_p^'(G) × P <| G
     p.-subgroup('N_G(P)) A[~: P, A, A] = 1 →
  A / 'C_G(P) \subset 'O_p('N_G(P) / 'C_G(P)).

Definition generated_by (gp : pred {group gT}) (E : {set gT}) :=
  [ gE : {set {group gT}}, <<\bigcup_(G in gE | gp G) G>> == E].

Definition norm_abelian (D : {set gT}) : pred {group gT} :=
  fun A(D \subset 'N(A)) && abelian A.

Definition p_norm_abelian p (D : {set gT}) : pred {group gT} :=
  fun Ap.-group A && norm_abelian D A.

Definition Puig_succ (D E : {set gT}) :=
  <<\bigcup_(A in subgroups D | norm_abelian E A) A>>.

Definition Puig_rec D := iter n (Puig_succ D) 1.

End Definitions.

This must be defined outside a Section to avoid spurrious delta-reduction
Definition Puig_at := nosimpl Puig_rec.

Definition Puig_inf (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2 G.

Definition Puig (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2.+1 G.

Notation "p .-length_1" := (plength_1 p)
  (at level 2, format "p .-length_1") : group_scope.

Notation "p .-constrained" := (p_constrained p)
  (at level 2, format "p .-constrained") : group_scope.
Notation "p .-abelian_constrained" := (p_abelian_constrained p)
  (at level 2, format "p .-abelian_constrained") : group_scope.
Notation "p .-stable" := (p_stable p)
  (at level 2, format "p .-stable") : group_scope.

Notation "''L_[' G ] ( L )" := (Puig_succ G L)
  (at level 8, format "''L_[' G ] ( L )") : group_scope.
Notation "''L_{' n } ( G )" := (Puig_at n G)
  (at level 8, format "''L_{' n } ( G )") : group_scope.
Notation "''L_*' ( G )" := (Puig_inf G)
  (at level 8, format "''L_*' ( G )") : group_scope.
Notation "''L' ( G )" := (Puig G)
  (at level 8, format "''L' ( G )") : group_scope.

Section BGsection1.

Implicit Types (gT : finGroupType) (p : nat).

This is B & G, Lemma 1.1, first part.
Lemma minnormal_solvable_abelem gT (M G : {group gT}) :
  minnormal M Gsolvable Mis_abelem M.

This is B & G, Lemma 1.2, second part.
Lemma minnormal_solvable_Fitting_center gT (M G : {group gT}) :
  minnormal M GM \subset Gsolvable MM \subset 'Z('F(G)).

Lemma sol_chief_abelem gT (G V U : {group gT}) :
  solvable Gchief_factor G V Uis_abelem (U / V).

Section HallLemma.

Variables (gT : finGroupType) (G G' : {group gT}).

Hypothesis solG : solvable G.
Hypothesis nsG'G : G' <| G.
Let sG'G := normal_sub nsG'G.
Let nG'G := normal_norm nsG'G.
Let nsF'G : 'F(G') <| G := char_normal_trans (Fitting_char G') nsG'G.

Let Gchief (UV : {group gT} × {group gT}) := chief_factor G UV.2 UV.1.
Let H := \bigcap_(UV | Gchief UV) 'C(UV.1 / UV.2 | 'Q).
Let H' :=
  G' :&: \bigcap_(UV | Gchief UV && (UV.1 \subset 'F(G'))) 'C(UV.1 / UV.2 | 'Q).

This is B & G Proposition 1.2, non trivial inclusion of the first equality.
This is B & G Proposition 1.2, non trivial inclusion of the second equality.
This is B & G, Proposition 1.3 (due to P. Hall).
Proposition cent_sub_Fitting gT (G : {group gT}) :
  solvable G'C_G('F(G)) \subset 'F(G).

This is B & G, Proposition 1.4, for internal actions.
Proposition coprime_trivg_cent_Fitting gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  'C_A(G) = 1 → 'C_A('F(G)) = 1.

A "contrapositive" of Proposition 1.4 above.
Proposition coprime_cent_Fitting gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  'C_A('F(G)) \subset 'C(G).

B & G Proposition 1.5 is covered by several lemmas in hall.v : 1.5a -> coprime_Hall_exists (internal action) ext_coprime_Hall_exists (general group action) 1.5b -> coprime_Hall_subset (internal action) ext_coprime_Hall_subset (general group action) 1.5c -> coprime_Hall_trans (internal action) ext_coprime_Hall_trans (general group action) 1.5d -> coprime_quotient_cent (internal action) ext_coprime_quotient_cent (general group action) several stronger variants are proved for internal action 1.5e -> coprime_comm_pcore (internal action only)
A stronger variant of B & G, Proposition 1.6(a).
Proposition coprimeR_cent_prod gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|[~: G, A]| #|A|solvable [~: G, A]
  [~: G, A] × 'C_G(A) = G.

This is B & G, Proposition 1.6(a).
Proposition coprime_cent_prod gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  [~: G, A] × 'C_G(A) = G.

This is B & G, Proposition 1.6(b).
Proposition coprime_commGid gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  [~: G, A, A] = [~: G, A].

This is B & G, Proposition 1.6(c).
Proposition coprime_commGG1P gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  [~: G, A, A] = 1 → A \subset 'C(G).

This is B & G, Proposition 1.6(d), TI-part, from finmod.v
This is B & G, Proposition 1.6(d) (direct product)
Proposition coprime_abelian_cent_dprod gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|abelian G
  [~: G, A] \x 'C_G(A) = G.

This is B & G, Proposition 1.6(e), which generalises Aschbacher (24.3).
Proposition coprime_abelian_faithful_Ohm1 gT (A G : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|abelian G
  A \subset 'C('Ohm_1(G))A \subset 'C(G).

B & G, Lemma 1.7 is covered by several lemmas in maximal.v : 1.7a -> Phi_nongen 1.7b -> Phi_quotient_abelem 1.7c -> trivg_Phi 1.7d -> Phi_joing
This is B & G, Proposition 1.8, or Aschbacher 24.1. Note that the coprime assumption is slightly weaker than requiring that A be a p'-group.
Proposition coprime_cent_Phi gT p (A G : {group gT}) :
    p.-group Gcoprime #|G| #|A|[~: G, A] \subset 'Phi(G)
  A \subset 'C(G).

This is B & G, Proposition 1.9, base (and most common) case, for internal coprime action.
Proposition stable_factor_cent gT (A G H : {group gT}) :
    A \subset 'C(H)stable_factor A H G
    coprime #|G| #|A|solvable G
  A \subset 'C(G).

This is B & G, Proposition 1.9 (for internal coprime action)
Proposition stable_series_cent gT (A G : {group gT}) s :
   last 1%G s :=: G(A.-stable).-series 1%G s
   coprime #|G| #|A|solvable G
  A \subset 'C(G).

This is B & G, Proposition 1.10.
Proposition coprime_nil_faithful_cent_stab gT (A G : {group gT}) :
     A \subset 'N(G)coprime #|G| #|A|nilpotent G
  let C := 'C_G(A) in 'C_G(C) \subset CA \subset 'C(G).

B & G, Theorem 1.11, via Aschbacher 24.7 rather than Gorenstein 5.3.10.
Theorem coprime_odd_faithful_Ohm1 gT p (A G : {group gT}) :
    p.-group GA \subset 'N(G)coprime #|G| #|A|odd #|G|
  A \subset 'C('Ohm_1(G))A \subset 'C(G).

This is B & G, Corollary 1.12.
Corollary coprime_odd_faithful_cent_abelem gT p (A G E : {group gT}) :
    E \in 'E_p(G)p.-group G
    A \subset 'N(G)coprime #|G| #|A|odd #|G|
  A \subset 'C('Ldiv_p('C_G(E)))A \subset 'C(G).

This is B & G, Theorem 1.13.
Theorem critical_odd gT p (G : {group gT}) :
    p.-group Godd #|G|G :!=: 1 →
  {H : {group gT} |
     [/\ H \char G, [~: H, G] \subset 'Z(H), nil_class H 2, exponent H = p
       & p.-group 'C(H | [Aut G])]}.

Section CoprimeQuotientPgroup.

This is B & G, Lemma 1.14, which we divide in four lemmas, each one giving the (sub)centraliser or (sub)normaliser of a quotient by a coprime p-group acting on it. Note that we weaken the assumptions of B & G -- M does not need to be normal in G, T need not be a subgroup of G, p need not be a prime, and M only needs to be coprime with T. Note also that the subcenter quotient lemma is special case of a lemma in coprime_act.

Variables (gT : finGroupType) (p : nat) (T M G : {group gT}).
Hypothesis pT : p.-group T.
Hypotheses (nMT : T \subset 'N(M)) (coMT : coprime #|M| #|T|).

This is B & G, Lemma 1.14, for a global normaliser.
This is B & G, Lemma 1.14, for a global centraliser.
This is B & G, Lemma 1.14, for a local normaliser.
This is B & G, Lemma 1.14, for a local centraliser.
This is B & G, Proposition 1.15a (Lemma 1.2.3 of P. Hall & G. Higman).
This is Gorenstein, Proposition 8.1.3.
This is B & G, Proposition 1.15b (due to D. Goldschmith).
This is B & G, Proposition 1.16, second assertion. Contrary to the text, we derive this directly, rather than by induction on the first, because this is actually how the proof is done in Gorenstein. Note that the non cyclic assumption for A is not needed here.
Proposition coprime_abelian_gen_cent gT (A G : {group gT}) :
   abelian AA \subset 'N(G)coprime #|G| #|A|
  <<\bigcup_(B : {group gT} | cyclic (A / B) && (B <| A)) 'C_G(B)>> = G.

B & G, Proposition 1.16, first assertion.
Proposition coprime_abelian_gen_cent1 gT (A G : {group gT}) :
   abelian A~~ cyclic AA \subset 'N(G)coprime #|G| #|A|
  <<\bigcup_(a in A^#) 'C_G[a]>> = G.

Section Focal_Subgroup.

Variables (gT : finGroupType) (G S : {group gT}) (p : nat).
Hypothesis sylS : p.-Sylow(G) S.

Import finalg FiniteModule GRing.Theory.

This is B & G, Theorem 1.17 ("Focal Subgroup Theorem", D. G. Higman), also Gorenstein Theorem 7.3.4 and Aschbacher (37.4).
Theorem focal_subgroup_gen :
  S :&: G^`(1) = <<[set [~ x, u] | x in S, u in G & x ^ u \in S]>>.

This is B & G, Theorem 1.18 (due to Burnside).
This is B & G, Corollary 1.19(a).
This is B & G, Corollary 1.19(b).
Corollary Zgroup_der1_Hall gT (G : {group gT}) :
  Zgroup GHall G G^`(1).

This is Aschbacher (39.2).
This is Aschbacher (39.3).
Lemma Zgroup_metacyclic gT (G : {group gT}) : Zgroup Gmetacyclic G.

This is B & G, Theorem 1.20 (Maschke's Theorem) for internal action on elementary abelian subgroups; a more general case, for linear represenations on matrices, can be found in mxrepresentation.v.
Theorem Maschke_abelem gT p (G V U : {group gT}) :
  p.-abelem Vp^'.-group GU \subset V
    G \subset 'N(V)G \subset 'N(U)
  exists2 W : {group gT}, U \x W = V & G \subset 'N(W).

Section Plength1.

Variables (gT : finGroupType) (p : nat).
Implicit Types G H : {group gT}.

Some basic properties of p.-length_1 that are direct consequences of their definition using p-series.
This is the characterization given in Section 10 of B & G, p. 75, just before Theorem 10.6.
This is B & G, Lemma 1.21(a).
Lemma plength1S G H : H \subset Gp.-length_1 Gp.-length_1 H.

Lemma plength1_quo G H : p.-length_1 Gp.-length_1 (G / H).

This is B & G, Lemma 1.21(b).
Lemma p'quo_plength1 G H :
  H <| Gp^'.-group Hp.-length_1 (G / H) = p.-length_1 G.

This is B & G, Lemma 1.21(c).
Lemma pquo_plength1 G H :
    H <| Gp.-group H'O_p^'(G / H) = 1->
  p.-length_1 (G / H) = p.-length_1 G.

Canonical p_elt_gen_group A : {group gT} :=
  Eval hnf in [group of p_elt_gen p A].

Note that p_elt_gen could be a functor.
This is B & G, Lemma 1.21(d).
This is B & G, Lemma 1.21(e).
Lemma quo2_plength1 gT p (G H K : {group gT}) :
  H <| GK <| GH :&: K = 1 →
     p.-length_1 (G / H) && p.-length_1 (G / K) = p.-length_1 G.

B & G Lemma 1.22 is covered by sylow.normal_pgroup.
Encapsulation of the use of the order of GL_2(p), via abelem groups.
Lemma logn_quotient_cent_abelem gT p (A E : {group gT}) :
    A \subset 'N(E)p.-abelem Elogn p #|E| 2 →
  logn p #|A : 'C_A(E)| 1.

End BGsection1.

Section PuigSeriesGroups.

Implicit Type gT : finGroupType.

Canonical Puig_succ_group gT (D E : {set gT}) := [group of 'L_[D](E)].

Fact Puig_at_group_set n gT D : @group_set gT 'L_{n}(D).

Canonical Puig_at_group n gT D := Group (@Puig_at_group_set n gT D).
Canonical Puig_inf_group gT (D : {set gT}) := [group of 'L_*(D)].
Canonical Puig_group gT (D : {set gT}) := [group of 'L(D)].

End PuigSeriesGroups.

Notation "''L_[' G ] ( L )" := (Puig_succ_group G L) : Group_scope.
Notation "''L_{' n } ( G )" := (Puig_at_group n G)
  (at level 8, format "''L_{' n } ( G )") : Group_scope.
Notation "''L_*' ( G )" := (Puig_inf_group G) : Group_scope.
Notation "''L' ( G )" := (Puig_group G) : Group_scope.

Elementary properties of the Puig series.
Section PuigBasics.

Variable gT : finGroupType.
Implicit Types (D E : {set gT}) (G H : {group gT}).

Lemma Puig0 D : 'L_{0}(D) = 1.
Lemma PuigS n D : 'L_{n.+1}(D) = 'L_[D]('L_{n}(D)).
Lemma Puig_recE n D : Puig_rec n D = 'L_{n}(D).
Lemma Puig_def D : 'L(D) = 'L_[D]('L_*(D)).

Local Notation "D --> E" := (generated_by (norm_abelian D) E)
  (at level 70, no associativity) : group_scope.

Lemma Puig_gen D E : E --> 'L_[D](E).

Lemma Puig_max G D E : D --> EE \subset GE \subset 'L_[G](D).

Lemma norm_abgenS D1 D2 E : D1 \subset D2D2 --> ED1 --> E.

Lemma Puig_succ_sub G D : 'L_[G](D) \subset G.

Lemma Puig_at_sub n G : 'L_{n}(G) \subset G.

This is B & G, Lemma B.1(d), first part.
This is part of B & G, Lemma B.1(b).
Lemma Puig1 G : 'L_{1}(G) = G.

End PuigBasics.

Functoriality of the Puig series.