Library mathcomp.solvable.nilpotent
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ 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 B ⇒ coset B @*^-1 'Z(A / B)) 1.
+ +
+End SeriesDefs.
+ +
+
+
++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 B ⇒ coset 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.
+ +
+
+
++ +
+ +
+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.
+
++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.
+