# Library mathcomp.solvable.nilpotent

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

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 A nilpotent A nilpotent B.

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

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

Lemma centrals_nil (s : seq {group gT}) G :
G.-central.-series 1%G s last 1%G s = G nilpotent 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 = G A^`(n) \* B^`(n) = G^`(n).

Lemma der_dprod n A B G : A \x B = G A^`(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 G reflect ('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 G nilpotent 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 = G nilpotent 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 = G nilpotent 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 i nilpotent (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 G reflect ('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 D f @* 'L_n(G) = 'L_n(f @* G).

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

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

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

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

Lemma nil_class_injm G :
'injm f G \subset D nil_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 L nilpotent G = nilpotent L.

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

Lemma quotient_nil G H : nilpotent G nilpotent (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 G H \subset G 'N_G(H) \subset H G :=: H.

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

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

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

Lemma meet_center_nil G H :
nilpotent G H <| G H :!=: 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 G cyclic (G / G^`(1)) cyclic G.

End QuotientNil.

Section Solvable.

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

Lemma nilpotent_sol G : nilpotent G solvable G.

Lemma abelian_sol G : abelian G solvable G.

Lemma solvable1 : solvable [1 gT].

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

Lemma sol_der1_proper G H :
solvable G H \subset G H :!=: 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 G solvable (f @* G).

Lemma injm_sol : 'injm f G \subset D solvable (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 L solvable G = solvable L.

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

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

Lemma metacyclic_sol G : metacyclic G solvable G.

End QuotientSol.