(Joint Center)Library MathComp.nilpotent

(* (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 path fintype div.
Require Import bigop prime finset fingroup morphism automorphism quotient.
Require Import commutator gproduct gfunctor center gseries cyclic.

This file defines nilpotent and solvable groups, and give some of their elementary properties; more will be added later (e.g., the nilpotence of p-groups in sylow.v, or the fact that minimal normal subgroups of solvable groups are elementary abelian in maximal.v). This file defines: nilpotent G == G is nilpotent, i.e., [~: H, G] is a proper subgroup of H for all nontrivial H <| G. solvable G == G is solvable, i.e., H^`(1) is a proper subgroup of H for all nontrivial subgroups H of G. 'L_n(G) == the nth term of the lower central series, namely [~: G, ..., G] (n Gs) if n > 0, with 'L_0(G) = G. G is nilpotent iff 'L_n(G) = 1 for some n. 'Z_n(G) == the nth term of the upper central series, i.e., with 'Z_0(G) = 1, 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)). nil_class G == the nilpotence class of G, i.e., the least n such that 'L_n.+1(G) = 1 (or, equivalently, 'Z_n(G) = G), if G is nilpotent; we take nil_class G = #|G| when G is not nilpotent, so nil_class G < #|G| iff G is nilpotent.

Set Implicit Arguments.

Import GroupScope.

Section SeriesDefs.

Variables (n : nat) (gT : finGroupType) (A : {set gT}).

Definition lower_central_at_rec := iter n (fun B[~: B, A]) A.

Definition upper_central_at_rec := iter n (fun Bcoset B @*^-1 'Z(A / B)) 1.

End SeriesDefs.

By convention, the lower central series starts at 1 while the upper series starts at 0 (sic).
Note: 'nosimpl' MUST be used outside of a section -- the end of section "cooking" destroys it.
Definition upper_central_at := nosimpl upper_central_at_rec.


Notation "''L_' n ( G )" := (lower_central_at n G)
  (at level 8, n at level 2, format "''L_' n ( G )") : group_scope.

Notation "''Z_' n ( G )" := (upper_central_at n G)
  (at level 8, n at level 2, format "''Z_' n ( G )") : group_scope.

Section PropertiesDefs.

Variables (gT : finGroupType) (A : {set gT}).

Definition nilpotent :=
  [ (G : {group gT} | G \subset A :&: [~: G, A]), G :==: 1].

Definition nil_class := index 1 (mkseq (fun n'L_n.+1(A)) #|A|).

Definition solvable :=
  [ (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1].

End PropertiesDefs.


Section NilpotentProps.

Variable gT: finGroupType.
Implicit Types (A B : {set gT}) (G H : {group gT}).

Lemma nilpotent1 : nilpotent [1 gT].

Lemma nilpotentS A B : B \subset Anilpotent Anilpotent B.

Lemma nil_comm_properl G H A :
    nilpotent GH \subset GH :!=: 1 → A \subset 'N_G(H)
  [~: H, A] \proper H.

Lemma nil_comm_properr G A H :
    nilpotent GH \subset GH :!=: 1 → A \subset 'N_G(H)
  [~: A, H] \proper H.

Lemma centrals_nil (s : seq {group gT}) G :
  G.-central.-series 1%G slast 1%G s = Gnilpotent G.

End NilpotentProps.

Section LowerCentral.

Variable gT : finGroupType.
Implicit Types (A B : {set gT}) (G H : {group gT}).

Lemma lcn0 A : 'L_0(A) = A.
Lemma lcn1 A : 'L_1(A) = A.
Lemma lcnSn n A : 'L_n.+2(A) = [~: 'L_n.+1(A), A].
Lemma lcnSnS n G : [~: 'L_n(G), G] \subset 'L_n.+1(G).
Lemma lcnE n A : 'L_n.+1(A) = lower_central_at_rec n A.
Lemma lcn2 A : 'L_2(A) = A^`(1).

Lemma lcn_group_set n G : group_set 'L_n(G).

Canonical lower_central_at_group n G := Group (lcn_group_set n G).

Lemma lcn_char n G : 'L_n(G) \char G.

Lemma lcn_normal n G : 'L_n(G) <| G.

Lemma lcn_sub n G : 'L_n(G) \subset G.

Lemma lcn_norm n G : G \subset 'N('L_n(G)).

Lemma lcn_subS n G : 'L_n.+1(G) \subset 'L_n(G).

Lemma lcn_normalS n G : 'L_n.+1(G) <| 'L_n(G).

Lemma lcn_central n G : 'L_n(G) / 'L_n.+1(G) \subset 'Z(G / 'L_n.+1(G)).

Lemma lcn_sub_leq m n G : n m'L_m(G) \subset 'L_n(G).

Lemma lcnS n A B : A \subset B'L_n(A) \subset 'L_n(B).

Lemma lcn_cprod n A B G : A \* B = G'L_n(A) \* 'L_n(B) = 'L_n(G).

Lemma lcn_dprod n A B G : A \x B = G'L_n(A) \x 'L_n(B) = 'L_n(G).

Lemma der_cprod n A B G : A \* B = GA^`(n) \* B^`(n) = G^`(n).

Lemma der_dprod n A B G : A \x B = GA^`(n) \x B^`(n) = G^`(n).

Lemma lcn_bigcprod n I r P (F : I{set gT}) G :
    \big[cprod/1]_(i <- r | P i) F i = G
  \big[cprod/1]_(i <- r | P i) 'L_n(F i) = 'L_n(G).

Lemma lcn_bigdprod n I r P (F : I{set gT}) G :
    \big[dprod/1]_(i <- r | P i) F i = G
  \big[dprod/1]_(i <- r | P i) 'L_n(F i) = 'L_n(G).

Lemma der_bigcprod n I r P (F : I{set gT}) G :
    \big[cprod/1]_(i <- r | P i) F i = G
  \big[cprod/1]_(i <- r | P i) (F i)^`(n) = G^`(n).

Lemma der_bigdprod n I r P (F : I{set gT}) G :
    \big[dprod/1]_(i <- r | P i) F i = G
  \big[dprod/1]_(i <- r | P i) (F i)^`(n) = G^`(n).

Lemma nilpotent_class G : nilpotent G = (nil_class G < #|G|).

Lemma lcn_nil_classP n G :
  nilpotent Greflect ('L_n.+1(G) = 1) (nil_class G n).

Lemma lcnP G : reflect ( n, 'L_n.+1(G) = 1) (nilpotent G).

Lemma abelian_nil G : abelian Gnilpotent G.

Lemma nil_class0 G : (nil_class G == 0) = (G :==: 1).

Lemma nil_class1 G : (nil_class G 1) = abelian G.

Lemma cprod_nil A B G : A \* B = Gnilpotent G = nilpotent A && nilpotent B.

Lemma mulg_nil G H :
  H \subset 'C(G)nilpotent (G × H) = nilpotent G && nilpotent H.

Lemma dprod_nil A B G : A \x B = Gnilpotent G = nilpotent A && nilpotent B.

Lemma bigdprod_nil I r (P : pred I) (A_ : I{set gT}) G :
  \big[dprod/1]_(i <- r | P i) A_ i = G
  → ( i, P inilpotent (A_ i)) → nilpotent G.

End LowerCentral.

Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope.

Lemma lcn_cont n : GFunctor.continuous (lower_central_at n).

Canonical lcn_igFun n := [igFun by lcn_sub^~ n & lcn_cont n].
Canonical lcn_gFun n := [gFun by lcn_cont n].
Canonical lcn_mgFun n := [mgFun by fun _ G H ⇒ @lcnS _ n G H].

Section UpperCentralFunctor.

Variable n : nat.
Implicit Type gT : finGroupType.

Lemma ucn_pmap : hZ : GFunctor.pmap, @upper_central_at n = hZ.

Now extract all the intermediate facts of the last proof.

Lemma ucn_group_set gT (G : {group gT}) : group_set 'Z_n(G).

Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G).

Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G.

Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n).

Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn].
Canonical ucn_gFun := [gFun by morphim_ucn].
Canonical ucn_pgFun := [pgFun by morphim_ucn].

Variable (gT : finGroupType) (G : {group gT}).

Lemma ucn_char : 'Z_n(G) \char G.
Lemma ucn_norm : G \subset 'N('Z_n(G)).
Lemma ucn_normal : 'Z_n(G) <| G.

End UpperCentralFunctor.

Notation "''Z_' n ( G )" := (upper_central_at_group n G) : Group_scope.

Section UpperCentral.

Variable gT : finGroupType.
Implicit Types (A B : {set gT}) (G H : {group gT}).

Lemma ucn0 A : 'Z_0(A) = 1.

Lemma ucnSn n A : 'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).

Lemma ucnE n A : 'Z_n(A) = upper_central_at_rec n A.

Lemma ucn_subS n G : 'Z_n(G) \subset 'Z_n.+1(G).

Lemma ucn_sub_geq m n G : n m'Z_m(G) \subset 'Z_n(G).

Lemma ucn_central n G : 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).

Lemma ucn_normalS n G : 'Z_n(G) <| 'Z_n.+1(G).

Lemma ucn_comm n G : [~: 'Z_n.+1(G), G] \subset 'Z_n(G).

Lemma ucn1 G : 'Z_1(G) = 'Z(G).

Lemma ucnSnR n G : 'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].

Lemma ucn_cprod n A B G : A \* B = G'Z_n(A) \* 'Z_n(B) = 'Z_n(G).

Lemma ucn_dprod n A B G : A \x B = G'Z_n(A) \x 'Z_n(B) = 'Z_n(G).

Lemma ucn_bigcprod n I r P (F : I{set gT}) G :
    \big[cprod/1]_(i <- r | P i) F i = G
  \big[cprod/1]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).

Lemma ucn_bigdprod n I r P (F : I{set gT}) G :
    \big[dprod/1]_(i <- r | P i) F i = G
  \big[dprod/1]_(i <- r | P i) 'Z_n(F i) = 'Z_n(G).

Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G).

Lemma ucnP G : reflect ( n, 'Z_n(G) = G) (nilpotent G).

Lemma ucn_nil_classP n G :
  nilpotent Greflect ('Z_n(G) = G) (nil_class G n).

Lemma ucn_id n G : 'Z_n('Z_n(G)) = 'Z_n(G).

Lemma ucn_nilpotent n G : nilpotent 'Z_n(G).

Lemma nil_class_ucn n G : nil_class 'Z_n(G) n.

End UpperCentral.

Section MorphNil.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Implicit Type G : {group aT}.

Lemma morphim_lcn n G : G \subset Df @* 'L_n(G) = 'L_n(f @* G).

Lemma injm_ucn n G : 'injm fG \subset Df @* 'Z_n(G) = 'Z_n(f @* G).

Lemma morphim_nil G : nilpotent Gnilpotent (f @* G).

Lemma injm_nil G : 'injm fG \subset Dnilpotent (f @* G) = nilpotent G.

Lemma nil_class_morphim G : nilpotent Gnil_class (f @* G) nil_class G.

Lemma nil_class_injm G :
  'injm fG \subset Dnil_class (f @* G) = nil_class G.

End MorphNil.

Section QuotientNil.

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

Lemma quotient_ucn_add m n G : 'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).

Lemma isog_nil rT G (L : {group rT}) : G \isog Lnilpotent G = nilpotent L.

Lemma isog_nil_class rT G (L : {group rT}) :
  G \isog Lnil_class G = nil_class L.

Lemma quotient_nil G H : nilpotent Gnilpotent (G / H).

Lemma quotient_center_nil G : nilpotent (G / 'Z(G)) = nilpotent G.

Lemma nil_class_quotient_center G :
  nilpotent (G) → nil_class (G / 'Z(G)) = (nil_class G).-1.

Lemma nilpotent_sub_norm G H :
  nilpotent GH \subset G'N_G(H) \subset HG :=: H.

Lemma nilpotent_proper_norm G H :
  nilpotent GH \proper GH \proper 'N_G(H).

Lemma nilpotent_subnormal G H : nilpotent GH \subset GH <|<| G.

Lemma TI_center_nil G H : nilpotent GH <| GH :&: 'Z(G) = 1 → H :=: 1.

Lemma meet_center_nil G H :
  nilpotent GH <| GH :!=: 1 → H :&: 'Z(G) != 1.

Lemma center_nil_eq1 G : nilpotent G('Z(G) == 1) = (G :==: 1).

Lemma cyclic_nilpotent_quo_der1_cyclic G :
  nilpotent Gcyclic (G / G^`(1)) → cyclic G.

End QuotientNil.

Section Solvable.

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

Lemma nilpotent_sol G : nilpotent Gsolvable G.

Lemma abelian_sol G : abelian Gsolvable G.

Lemma solvable1 : solvable [1 gT].

Lemma solvableS G H : H \subset Gsolvable Gsolvable H.

Lemma sol_der1_proper G H :
  solvable GH \subset GH :!=: 1 → H^`(1) \proper H.

Lemma derivedP G : reflect ( n, G^`(n) = 1) (solvable G).

End Solvable.

Section MorphSol.

Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
Variable G : {group gT}.

Lemma morphim_sol : solvable Gsolvable (f @* G).

Lemma injm_sol : 'injm fG \subset Dsolvable (f @* G) = solvable G.

End MorphSol.

Section QuotientSol.

Variables gT rT : finGroupType.
Implicit Types G H K : {group gT}.

Lemma isog_sol G (L : {group rT}) : G \isog Lsolvable G = solvable L.

Lemma quotient_sol G H : solvable Gsolvable (G / H).

Lemma series_sol G H : H <| Gsolvable G = solvable H && solvable (G / H).

Lemma metacyclic_sol G : metacyclic Gsolvable G.

End QuotientSol.