Initial commit

1 files changed, 755 insertions, 0 deletions

diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
new file mode 100644
index 0000000..5b271de
--- /dev/null
+++ b/mathcomp/solvable/nilpotent.v
@@ -0,0 +1,755 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+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.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+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).                                                         *)
+Definition lower_central_at n := lower_central_at_rec n.-1.
+
+(* 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.
+
+Arguments Scope lower_central_at [nat_scope _ group_scope].
+Arguments Scope upper_central_at [nat_scope _ group_scope].
+
+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 :=
+  [forall (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 :=
+  [forall (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1].
+
+End PropertiesDefs.
+
+Arguments Scope nilpotent [_ group_scope].
+Arguments Scope nil_class [_ group_scope].
+Arguments Scope solvable [_ group_scope].
+Prenex Implicits nil_class nilpotent solvable.
+
+Section NilpotentProps.
+
+Variable gT: finGroupType.
+Implicit Types (A B : {set gT}) (G H : {group gT}).
+
+Lemma nilpotent1 : nilpotent [1 gT].
+Proof. by apply/forall_inP=> H; rewrite commG1 setIid -subG1. Qed.
+
+Lemma nilpotentS A B : B \subset A -> nilpotent A -> nilpotent B.
+Proof.
+move=> sBA nilA; apply/forall_inP=> H sHR.
+have:= forallP nilA H; rewrite (subset_trans sHR) //.
+by apply: subset_trans (setIS _ _) (setSI _ _); rewrite ?commgS.
+Qed.
+
+Lemma nil_comm_properl G H A :
+    nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) ->
+  [~: H, A] \proper H.
+Proof.
+move=> nilG sHG ntH; rewrite subsetI properE; case/andP=> sAG nHA.
+rewrite (subset_trans (commgS H (subset_gen A))) ?commg_subl ?gen_subG //.
+apply: contra ntH => sHR; have:= forallP nilG H; rewrite subsetI sHG.
+by rewrite (subset_trans sHR) ?commgS.
+Qed.
+
+Lemma nil_comm_properr G A H :
+    nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) ->
+  [~: A, H] \proper H.
+Proof. by rewrite commGC; apply: nil_comm_properl. Qed.
+ 
+Lemma centrals_nil (s : seq {group gT}) G :
+  G.-central.-series 1%G s -> last 1%G s = G -> nilpotent G.
+Proof.
+move=> cGs defG; apply/forall_inP=> H /subsetIP[sHG sHR].
+move: sHG; rewrite -{}defG -subG1 -[1]/(gval 1%G). 
+elim: s 1%G cGs => //= L s IHs K /andP[/and3P[sRK sKL sLG] /IHs sHL] sHs.
+exact: subset_trans sHR (subset_trans (commSg _ (sHL sHs)) sRK).
+Qed.
+
+End NilpotentProps.
+
+Section LowerCentral.
+
+Variable gT : finGroupType.
+Implicit Types (A B : {set gT}) (G H : {group gT}).
+
+Lemma lcn0 A : 'L_0(A) = A. Proof. by []. Qed.
+Lemma lcn1 A : 'L_1(A) = A. Proof. by []. Qed.
+Lemma lcnSn n A : 'L_n.+2(A) = [~: 'L_n.+1(A), A]. Proof. by []. Qed.
+Lemma lcnSnS n G : [~: 'L_n(G), G] \subset 'L_n.+1(G).
+Proof. by case: n => //; exact: der1_subG. Qed.
+Lemma lcnE n A : 'L_n.+1(A) = lower_central_at_rec n A.
+Proof. by []. Qed.
+Lemma lcn2 A : 'L_2(A) = A^`(1). Proof. by []. Qed.
+
+Lemma lcn_group_set n G : group_set 'L_n(G).
+Proof. by case: n => [|[|n]]; exact: groupP. Qed.
+
+Canonical lower_central_at_group n G := Group (lcn_group_set n G).
+
+Lemma lcn_char n G : 'L_n(G) \char G.
+Proof.
+by case: n => [|n]; last elim: n => [|n IHn]; rewrite ?lcnSn ?charR ?char_refl.
+Qed.
+
+Lemma lcn_normal n G : 'L_n(G) <|  G.
+Proof. by apply: char_normal; exact: lcn_char. Qed.
+
+Lemma lcn_sub n G : 'L_n(G) \subset G.
+Proof. by case/andP: (lcn_normal n G). Qed.
+
+Lemma lcn_norm n G : G \subset 'N('L_n(G)).
+Proof. by case/andP: (lcn_normal n G). Qed.
+
+Lemma lcn_subS n G : 'L_n.+1(G) \subset 'L_n(G).
+Proof.
+case: n => // n; rewrite lcnSn commGC commg_subr.
+by case/andP: (lcn_normal n.+1 G).
+Qed.
+
+Lemma lcn_normalS n G : 'L_n.+1(G) <| 'L_n(G).
+Proof. by apply: normalS (lcn_normal _ _); rewrite (lcn_subS, lcn_sub). Qed.
+
+Lemma lcn_central n G : 'L_n(G) / 'L_n.+1(G) \subset 'Z(G / 'L_n.+1(G)).
+Proof.
+case: n => [|n]; first by rewrite trivg_quotient sub1G.
+by rewrite subsetI quotientS ?lcn_sub ?quotient_cents2r.
+Qed.
+
+Lemma lcn_sub_leq m n G : n <= m -> 'L_m(G) \subset 'L_n(G).
+Proof.
+by move/subnK <-; elim: {m}(m - n) => // m; exact: subset_trans (lcn_subS _ _).
+Qed.
+
+Lemma lcnS n A B : A \subset B -> 'L_n(A) \subset 'L_n(B).
+Proof.
+by case: n => // n sAB; elim: n => // n IHn; rewrite !lcnSn genS ?imset2S.
+Qed.
+
+Lemma lcn_cprod n A B G : A \* B = G -> 'L_n(A) \* 'L_n(B) = 'L_n(G).
+Proof.
+case: n => // n /cprodP[[H K -> ->{A B}] defG cHK].
+have sL := subset_trans (lcn_sub _ _); rewrite cprodE ?(centSS _ _ cHK) ?sL //.
+symmetry; elim: n => // n; rewrite lcnSn => ->; rewrite commMG /=; last first.
+  by apply: subset_trans (commg_normr _ _); rewrite sL // -defG mulG_subr.
+rewrite -!(commGC G) -defG -{1}(centC cHK).
+rewrite !commMG ?normsR ?lcn_norm ?cents_norm // 1?centsC //.
+by rewrite -!(commGC 'L__(_)) -!lcnSn !(commG1P _) ?mul1g ?sL // centsC.
+Qed.
+
+Lemma lcn_dprod n A B G : A \x B = G -> 'L_n(A) \x 'L_n(B) = 'L_n(G).
+Proof.
+move=> defG; have [[K H defA defB] _ _ tiAB] := dprodP defG.
+rewrite !dprodEcp // in defG *; first exact: lcn_cprod.
+by rewrite defA defB; apply/trivgP; rewrite -tiAB defA defB setISS ?lcn_sub.
+Qed.
+
+Lemma der_cprod n A B G : A \* B = G -> A^`(n) \* B^`(n) = G^`(n).
+Proof. by move=> defG; elim: n => {defG}// n; apply: (lcn_cprod 2). Qed.
+
+Lemma der_dprod n A B G : A \x B = G -> A^`(n) \x B^`(n) = G^`(n).
+Proof. by move=> defG; elim: n => {defG}// n; apply: (lcn_dprod 2). Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first exact/esym/trivgP/lcn_sub.
+by rewrite -(lcn_cprod n dG); have [[_ H _ dH]] := cprodP dG; rewrite dH (IH H).
+Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first exact/esym/trivgP/lcn_sub.
+by rewrite -(lcn_dprod n dG); have [[_ H _ dH]] := dprodP dG; rewrite dH (IH H).
+Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first by rewrite gF1.
+by rewrite -(der_cprod n dG); have [[_ H _ dH]] := cprodP dG; rewrite dH (IH H).
+Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first by rewrite gF1.
+by rewrite -(der_dprod n dG); have [[_ H _ dH]] := dprodP dG; rewrite dH (IH H).
+Qed.
+
+Lemma nilpotent_class G : nilpotent G = (nil_class G < #|G|).
+Proof.
+rewrite /nil_class; set s := mkseq _ _.
+transitivity (1 \in s); last by rewrite -index_mem size_mkseq.
+apply/idP/mapP=> {s}/= [nilG | [n _ Ln1]]; last first.
+  apply/forall_inP=> H /subsetIP[sHG sHR].
+  rewrite -subG1 {}Ln1; elim: n => // n IHn.
+  by rewrite (subset_trans sHR) ?commSg.
+pose m := #|G|.-1; exists m; first by rewrite mem_iota /= prednK.
+rewrite ['L__(G)]card_le1_trivg //= -(subnn m).
+elim: {-2}m => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS].
+case: (eqsVneq 'L_n.+1(G) 1) => [-> | ntLn]; first by rewrite comm1G cards1.
+case: (m - n) => [|m' /= IHn]; first by rewrite leqNgt cardG_gt1 ntLn.
+rewrite -ltnS (leq_trans (proper_card _) IHn) //.
+by rewrite (nil_comm_properl nilG) ?lcn_sub // subsetI subxx lcn_norm.
+Qed.
+
+Lemma lcn_nil_classP n G :
+  nilpotent G -> reflect ('L_n.+1(G) = 1) (nil_class G <= n).
+Proof.
+rewrite nilpotent_class /nil_class; set s := mkseq _ _.
+set c := index 1 s => lt_c_G; case: leqP => [le_c_n | lt_n_c].
+  have Lc1: nth 1 s c = 1 by rewrite nth_index // -index_mem size_mkseq.
+  by left; apply/trivgP; rewrite -Lc1 nth_mkseq ?lcn_sub_leq.
+right; apply/eqP/negPf; rewrite -(before_find 1 lt_n_c) nth_mkseq //.
+exact: ltn_trans lt_n_c lt_c_G.
+Qed.
+
+Lemma lcnP G : reflect (exists n, 'L_n.+1(G) = 1) (nilpotent G).
+Proof.
+apply: (iffP idP) => [nilG | [n Ln1]].
+  by exists (nil_class G); exact/lcn_nil_classP.
+apply/forall_inP=> H /subsetIP[sHG sHR]; rewrite -subG1 -{}Ln1.
+by elim: n => // n IHn; rewrite (subset_trans sHR) ?commSg.
+Qed.
+
+Lemma abelian_nil G : abelian G -> nilpotent G.
+Proof. by move=> abG; apply/lcnP; exists 1%N; exact/commG1P. Qed.
+
+Lemma nil_class0 G : (nil_class G == 0) = (G :==: 1).
+Proof.
+apply/idP/eqP=> [nilG | ->].
+  by apply/(lcn_nil_classP 0); rewrite ?nilpotent_class (eqP nilG) ?cardG_gt0.
+by rewrite -leqn0; apply/(lcn_nil_classP 0); rewrite ?nilpotent1.
+Qed.
+
+Lemma nil_class1 G : (nil_class G <= 1) = abelian G.
+Proof.
+have [-> | ntG] := eqsVneq G 1.
+  by rewrite abelian1 leq_eqVlt ltnS leqn0 nil_class0 eqxx orbT.
+apply/idP/idP=> cGG.
+  apply/commG1P; apply/(lcn_nil_classP 1); rewrite // nilpotent_class.
+  by rewrite (leq_ltn_trans cGG) // cardG_gt1.
+by apply/(lcn_nil_classP 1); rewrite ?abelian_nil //; apply/commG1P.
+Qed.
+
+Lemma cprod_nil A B G : A \* B = G -> nilpotent G = nilpotent A && nilpotent B.
+Proof.
+move=> defG; case/cprodP: defG (defG) => [[H K -> ->{A B}] defG _] defGc.
+apply/idP/andP=> [nilG | [/lcnP[m LmH1] /lcnP[n LnK1]]].
+  by rewrite !(nilpotentS _ nilG) // -defG (mulG_subr, mulG_subl).
+apply/lcnP; exists (m + n.+1); apply/trivgP.
+case/cprodP: (lcn_cprod (m.+1 + n.+1) defGc) => _ <- _.
+by rewrite mulG_subG /= -{1}LmH1 -LnK1 !lcn_sub_leq ?leq_addl ?leq_addr.
+Qed.
+
+Lemma mulg_nil G H :
+  H \subset 'C(G) -> nilpotent (G * H) = nilpotent G && nilpotent H.
+Proof. by move=> cGH; rewrite -(cprod_nil (cprodEY cGH)) /= cent_joinEr. Qed.
+
+Lemma dprod_nil A B G : A \x B = G -> nilpotent G = nilpotent A && nilpotent B.
+Proof. by case/dprodP=> [[H K -> ->] <- cHK _]; rewrite mulg_nil.
+Qed.
+
+Lemma bigdprod_nil I r (P : pred I) (A_ : I -> {set gT}) G :
+  \big[dprod/1]_(i <- r | P i) A_ i = G
+  -> (forall i, P i -> nilpotent (A_ i)) -> nilpotent G.
+Proof.
+move=> defG nilA; elim/big_rec: _ => [|i B Pi nilB] in G defG *.
+  by rewrite -defG nilpotent1.
+have [[_ H _ defB] _ _ _] := dprodP defG.
+by rewrite (dprod_nil defG) nilA //= defB nilB.
+Qed.
+
+End LowerCentral.
+
+Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope.
+
+Lemma lcn_cont n : GFunctor.continuous (lower_central_at n).
+Proof.
+case: n => //; elim=> // n IHn g0T h0T H phi.
+by rewrite !lcnSn morphimR ?lcn_sub // commSg ?IHn.
+Qed.
+
+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 : exists hZ : GFunctor.pmap, @upper_central_at n = hZ.
+Proof.
+elim: n => [|n' [hZ defZ]]; first by exists trivGfun_pgFun.
+by exists [pgFun of center %% hZ]; rewrite /= -defZ.
+Qed.
+
+(* Now extract all the intermediate facts of the last proof. *)
+
+Lemma ucn_group_set gT (G : {group gT}) : group_set 'Z_n(G).
+Proof. by have [hZ ->] := ucn_pmap; exact: groupP. Qed.
+
+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.
+Proof. by have [hZ ->] := ucn_pmap; exact: gFsub. Qed.
+
+Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n).
+Proof. by have [hZ ->] := ucn_pmap; exact: pmorphimF. Qed.
+
+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. Proof. exact: gFchar. Qed.
+Lemma ucn_norm : G \subset 'N('Z_n(G)). Proof. exact: gFnorm. Qed.
+Lemma ucn_normal : 'Z_n(G) <| G. Proof. exact: gFnormal. Qed.
+
+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.
+Proof. by []. Qed.
+
+Lemma ucnSn n A : 'Z_n.+1(A) = coset 'Z_n(A) @*^-1 'Z(A / 'Z_n(A)).
+Proof. by []. Qed.
+
+Lemma ucnE n A : 'Z_n(A) = upper_central_at_rec n A.
+Proof. by []. Qed.
+
+Lemma ucn_subS n G : 'Z_n(G) \subset 'Z_n.+1(G).
+Proof. by rewrite -{1}['Z_n(G)]ker_coset morphpreS ?sub1G. Qed.
+
+Lemma ucn_sub_geq m n G : n >= m -> 'Z_m(G) \subset 'Z_n(G).
+Proof.
+move/subnK <-; elim: {n}(n - m) => // n IHn.
+exact: subset_trans (ucn_subS _ _).
+Qed.
+
+Lemma ucn_central n G : 'Z_n.+1(G) / 'Z_n(G) = 'Z(G / 'Z_n(G)).
+Proof. by rewrite ucnSn cosetpreK. Qed.
+
+Lemma ucn_normalS n G : 'Z_n(G) <| 'Z_n.+1(G).
+Proof. by rewrite (normalS _ _ (ucn_normal n G)) ?ucn_subS ?ucn_sub. Qed.
+
+Lemma ucn_comm n G : [~: 'Z_n.+1(G), G] \subset 'Z_n(G).
+Proof.
+rewrite -quotient_cents2 ?normal_norm ?ucn_normal ?ucn_normalS //.
+by rewrite ucn_central subsetIr.
+Qed.
+
+Lemma ucn1 G : 'Z_1(G) = 'Z(G).
+Proof.
+apply: (quotient_inj (normal1 _) (normal1 _)).
+by rewrite /= (ucn_central 0) -injmF ?norms1 ?coset1_injm.
+Qed.
+
+Lemma ucnSnR n G : 'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].
+Proof.
+apply/setP=> x; rewrite inE -(setIidPr (ucn_sub n.+1 G)) inE ucnSn.
+case Gx: (x \in G) => //=; have nZG := ucn_norm n G.
+rewrite -sub1set -sub_quotient_pre -?quotient_cents2 ?sub1set ?(subsetP nZG) //.
+by rewrite subsetI quotientS ?sub1set.
+Qed.
+
+Lemma ucn_cprod n A B G : A \* B = G -> 'Z_n(A) \* 'Z_n(B) = 'Z_n(G).
+Proof.
+case/cprodP=> [[H K -> ->{A B}] mulHK cHK].
+elim: n => [|n /cprodP[_ /= defZ cZn]]; first exact: cprod1g.
+set Z := 'Z_n(G) in defZ cZn; rewrite (ucnSn n G) /= -/Z.
+have /mulGsubP[nZH nZK]: H * K \subset 'N(Z) by rewrite mulHK gFnorm.
+have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z).
+  by rewrite -mulHK quotientMl // center_prod ?quotient_cents.
+have ZquoZ (B A : {group gT}):
+  B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z.
+- move=> cAB {defZ}defZ; have cAZnB := subset_trans (ucn_sub n B) cAB. 
+  have /second_isom[/=]: A \subset 'N(Z).
+    by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC.
+  suffices ->: Z :&: A = 'Z_n(A).
+    by move=> f inj_f im_f; rewrite -!im_f ?gFsub // ucn_central injm_center.
+  rewrite -defZ -group_modl ?gFsub //; apply/mulGidPl.
+  have [-> | n_gt0] := posnP n; first exact: subsetIl.
+  by apply: subset_trans (ucn_sub_geq A n_gt0); rewrite /= setIC ucn1 setIS.
+rewrite (ZquoZ H K) 1?centsC 1?(centC cZn) // {ZquoZ}(ZquoZ K H) //.
+have cZn1: 'Z_n.+1(K) \subset 'C('Z_n.+1(H)) by apply: centSS cHK; apply: gFsub.
+rewrite -quotientMl ?quotientK ?mul_subG ?(subset_trans (gFsub _ _)) //=.
+rewrite cprodE // -cent_joinEr ?mulSGid //= cent_joinEr //= -/Z.
+by rewrite -defZ mulgSS ?ucn_subS.
+Qed.
+
+Lemma ucn_dprod n A B G : A \x B = G -> 'Z_n(A) \x 'Z_n(B) = 'Z_n(G).
+Proof.
+move=> defG; have [[K H defA defB] _ _ tiAB] := dprodP defG.
+rewrite !dprodEcp // in defG *; first exact: ucn_cprod.
+by rewrite defA defB; apply/trivgP; rewrite -tiAB defA defB setISS ?ucn_sub.
+Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first by rewrite gF1.
+by rewrite -(ucn_cprod n dG); have [[_ H _ dH]] := cprodP dG; rewrite dH (IH H).
+Qed.
+
+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).
+Proof.
+elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first by rewrite gF1.
+by rewrite -(ucn_dprod n dG); have [[_ H _ dH]] := dprodP dG; rewrite dH (IH H).
+Qed.
+
+Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G).
+Proof.
+rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G).
+elim: {1 3}n 0 (addn0 n) => [j <- //|i IHi j].
+rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn.
+have nZG := normal_norm (ucn_normal j G).
+have nZL := subset_trans (lcn_sub _ _) nZG.
+by rewrite -sub_morphim_pre // subsetI morphimS ?lcn_sub // quotient_cents2.
+Qed.
+
+Lemma ucnP G : reflect (exists n, 'Z_n(G) = G) (nilpotent G).
+Proof.
+apply: (iffP (lcnP G)) => [] [n /eqP clGn];
+  by exists n; apply/eqP; rewrite ucn_lcnP in clGn *.
+Qed.
+
+Lemma ucn_nil_classP n G :
+  nilpotent G -> reflect ('Z_n(G) = G) (nil_class G <= n).
+Proof.
+move=> nilG; rewrite (sameP (lcn_nil_classP n nilG) eqP) ucn_lcnP; exact: eqP.
+Qed.
+
+Lemma ucn_id n G : 'Z_n('Z_n(G)) = 'Z_n(G).
+Proof. by rewrite -{2}['Z_n(G)]gFid. Qed.
+
+Lemma ucn_nilpotent n G : nilpotent 'Z_n(G). 
+Proof. by apply/ucnP; exists n; rewrite ucn_id. Qed.
+
+Lemma nil_class_ucn n G : nil_class 'Z_n(G) <= n.
+Proof. by apply/ucn_nil_classP; rewrite ?ucn_nilpotent ?ucn_id. Qed.
+
+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).
+Proof.
+move=> sHG; case: n => //; elim=> // n IHn.
+by rewrite !lcnSn -IHn morphimR // (subset_trans _ sHG) // lcn_sub.
+Qed.
+
+Lemma injm_ucn n G : 'injm f -> G \subset D -> f @* 'Z_n(G) = 'Z_n(f @* G).
+Proof. exact: injmF. Qed.
+
+Lemma morphim_nil G : nilpotent G -> nilpotent (f @* G).
+Proof.
+case/ucnP=> n ZnG; apply/ucnP; exists n; apply/eqP.
+by rewrite eqEsubset ucn_sub /= -{1}ZnG morphim_ucn.
+Qed.
+
+Lemma injm_nil G : 'injm f -> G \subset D -> nilpotent (f @* G) = nilpotent G.
+Proof.
+move=> injf sGD; apply/idP/idP; last exact: morphim_nil.
+case/ucnP=> n; rewrite -injm_ucn // => /injm_morphim_inj defZ.
+by apply/ucnP; exists n; rewrite defZ ?(subset_trans (ucn_sub n G)).
+Qed.
+
+Lemma nil_class_morphim G : nilpotent G -> nil_class (f @* G) <= nil_class G.
+Proof.
+move=> nilG; rewrite (sameP (ucn_nil_classP _ (morphim_nil nilG)) eqP) /=.
+by rewrite eqEsubset ucn_sub -{1}(ucn_nil_classP _ nilG (leqnn _)) morphim_ucn.
+Qed.
+
+Lemma nil_class_injm G :
+  'injm f -> G \subset D -> nil_class (f @* G) = nil_class G.
+Proof.
+move=> injf sGD; case nilG: (nilpotent G).
+  apply/eqP; rewrite eqn_leq nil_class_morphim //.
+  rewrite (sameP (lcn_nil_classP _ nilG) eqP) -subG1.
+  rewrite -(injmSK injf) ?(subset_trans (lcn_sub _ _)) // morphim1.
+  by rewrite morphim_lcn // (lcn_nil_classP _ _ (leqnn _)) //= injm_nil.
+transitivity #|G|; apply/eqP; rewrite eqn_leq.
+  rewrite -(card_injm injf sGD) (leq_trans (index_size _ _)) ?size_mkseq //.
+  by rewrite leqNgt -nilpotent_class injm_nil ?nilG.
+rewrite (leq_trans (index_size _ _)) ?size_mkseq // leqNgt -nilpotent_class.
+by rewrite nilG.
+Qed.
+
+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)).
+Proof.
+elim: m => [|m IHm]; first exact: trivg_quotient.
+apply/setP=> Zx; have [x Nx ->{Zx}] := cosetP Zx.
+have [sZG nZG] := andP (ucn_normal n G).
+rewrite (ucnSnR m) inE -!sub1set -morphim_set1 //= -quotientR ?sub1set // -IHm.
+rewrite !quotientSGK ?(ucn_sub_geq, leq_addl, comm_subG _ nZG, sub1set) //=.
+by rewrite addSn /= ucnSnR inE.
+Qed.
+
+Lemma isog_nil rT G (L : {group rT}) : G \isog L -> nilpotent G = nilpotent L.
+Proof. by case/isogP=> f injf <-; rewrite injm_nil. Qed.
+
+Lemma isog_nil_class rT G (L : {group rT}) :
+  G \isog L -> nil_class G = nil_class L.
+Proof. by case/isogP=> f injf <-; rewrite nil_class_injm. Qed.
+
+Lemma quotient_nil G H : nilpotent G -> nilpotent (G / H).
+Proof. exact: morphim_nil. Qed.
+  
+Lemma quotient_center_nil G : nilpotent (G / 'Z(G)) = nilpotent G.
+Proof.
+rewrite -ucn1; apply/idP/idP; last exact: quotient_nil.
+case/ucnP=> c nilGq; apply/ucnP; exists c.+1; have nsZ1G := ucn_normal 1 G.
+apply: (quotient_inj _ nsZ1G); last by rewrite /= -(addn1 c) quotient_ucn_add.
+by rewrite (normalS _ _ nsZ1G) ?ucn_sub ?ucn_sub_geq.
+Qed.
+
+Lemma nil_class_quotient_center G :
+  nilpotent (G) -> nil_class (G / 'Z(G)) = (nil_class G).-1.
+Proof.
+move=> nilG; have nsZ1G := ucn_normal 1 G.
+apply/eqP; rewrite -ucn1 eqn_leq; apply/andP; split.
+  apply/ucn_nil_classP; rewrite ?quotient_nil //= -quotient_ucn_add ucn1.
+  by rewrite (ucn_nil_classP _ _ _) ?addn1 ?leqSpred.
+rewrite -subn1 leq_subLR addnC; apply/ucn_nil_classP => //=.
+apply: (quotient_inj _ nsZ1G) => /=.
+  by apply: normalS (ucn_sub _ _) nsZ1G; rewrite /= addnS ucn_sub_geq.
+by rewrite quotient_ucn_add; apply/ucn_nil_classP; rewrite //= quotient_nil.
+Qed.
+
+Lemma nilpotent_sub_norm G H :
+  nilpotent G -> H \subset G -> 'N_G(H) \subset H -> G :=: H.
+Proof.
+move=> nilG sHG sNH; apply/eqP; rewrite eqEsubset sHG andbT; apply/negP=> nsGH.
+have{nsGH} [i sZH []]: exists2 i, 'Z_i(G) \subset H & ~ 'Z_i.+1(G) \subset H.
+  case/ucnP: nilG => n ZnG; rewrite -{}ZnG in nsGH.
+  elim: n => [|i IHi] in nsGH *; first by rewrite sub1G in nsGH.
+  by case sZH: ('Z_i(G) \subset H); [exists i | apply: IHi; rewrite sZH].
+apply: subset_trans sNH; rewrite subsetI ucn_sub -commg_subr.
+by apply: subset_trans sZH; apply: subset_trans (ucn_comm i G); exact: commgS.
+Qed.
+
+Lemma nilpotent_proper_norm G H :
+  nilpotent G -> H \proper G -> H \proper 'N_G(H).
+Proof.
+move=> nilG; rewrite properEneq properE subsetI normG => /andP[neHG sHG].
+by rewrite sHG; apply: contra neHG; move/(nilpotent_sub_norm nilG)->.
+Qed.
+
+Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G.
+Proof.
+move=> nilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) => // m IHm H.
+rewrite ltnS => leGHm sHG; have:= sHG; rewrite subEproper.
+case/predU1P=> [->|]; first exact: subnormal_refl.
+move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK.
+have snHK: H <|<| K by rewrite normal_subnormal ?normalSG.
+have sKG: K \subset G by rewrite subsetIl.
+apply: subnormal_trans snHK (IHm _ (leq_trans _ leGHm) sKG).
+by rewrite ltn_sub2l ?proper_card ?(proper_sub_trans prHK).
+Qed.
+
+Lemma TI_center_nil G H : nilpotent G -> H <| G -> H :&: 'Z(G) = 1 -> H :=: 1.
+Proof.
+move=> nilG /andP[sHG nHG] tiHZ.
+rewrite -{1}(setIidPl sHG); have{nilG} /ucnP[n <-] := nilG.
+elim: n => [|n IHn]; apply/trivgP; rewrite ?subsetIr // -tiHZ.
+rewrite [H :&: 'Z(G)]setIA subsetI setIS ?ucn_sub //= (sameP commG1P trivgP).
+rewrite -commg_subr commGC in nHG.
+rewrite -IHn subsetI (subset_trans _ nHG) ?commSg ?subsetIl //=.
+by rewrite (subset_trans _ (ucn_comm n G)) ?commSg ?subsetIr.
+Qed.
+
+Lemma meet_center_nil G H :
+  nilpotent G -> H <| G -> H :!=: 1 -> H :&: 'Z(G) != 1.
+Proof. by move=> nilG nsHG; apply: contraNneq => /TI_center_nil->. Qed.
+
+Lemma center_nil_eq1 G : nilpotent G -> ('Z(G) == 1) = (G :==: 1).
+Proof.
+move=> nilG; apply/eqP/eqP=> [Z1 | ->]; last exact: center1.
+by rewrite (TI_center_nil nilG) // (setIidPr (center_sub G)).
+Qed.
+
+Lemma cyclic_nilpotent_quo_der1_cyclic G :
+  nilpotent G -> cyclic (G / G^`(1)) -> cyclic G.
+Proof.
+move=> nG; rewrite (isog_cyclic (quotient1_isog G)).
+have [-> // | ntG' cGG'] := (eqVneq G^`(1) 1)%g.
+suffices: 'L_2(G) \subset G :&: 'L_3(G) by move/(eqfun_inP nG)=> <-.
+rewrite subsetI lcn_sub /= -quotient_cents2 ?lcn_norm //.
+apply: cyclic_factor_abelian (lcn_central 2 G) _.
+by rewrite (isog_cyclic (third_isog _ _ _)) ?lcn_normal // lcn_subS.
+Qed.
+
+End QuotientNil.
+
+Section Solvable.
+
+Variable gT : finGroupType.
+Implicit Types G H : {group gT}.
+
+Lemma nilpotent_sol G : nilpotent G -> solvable G.
+Proof.
+move=> nilG; apply/forall_inP=> H /subsetIP[sHG sHH'].
+by rewrite (forall_inP nilG) // subsetI sHG (subset_trans sHH') ?commgS.
+Qed.
+
+Lemma abelian_sol G : abelian G -> solvable G.
+Proof. by move/abelian_nil; exact: nilpotent_sol. Qed.
+
+Lemma solvable1 : solvable [1 gT]. Proof. exact: abelian_sol (abelian1 gT). Qed.
+
+Lemma solvableS G H : H \subset G -> solvable G -> solvable H.
+Proof.
+move=> sHG solG;  apply/forall_inP=> K /subsetIP[sKH sKK'].
+by rewrite (forall_inP solG) // subsetI (subset_trans sKH).
+Qed.
+
+Lemma sol_der1_proper G H :
+  solvable G -> H \subset G -> H :!=: 1 -> H^`(1) \proper H.
+Proof.
+move=> solG sHG ntH; rewrite properE comm_subG //; apply: implyP ntH.
+by have:= forallP solG H; rewrite subsetI sHG implybNN. 
+Qed.
+
+Lemma derivedP G : reflect (exists n, G^`(n) = 1) (solvable G).
+Proof.
+apply: (iffP idP) => [solG | [n solGn]]; last first.
+  apply/forall_inP=> H /subsetIP[sHG sHH'].
+  rewrite -subG1 -{}solGn; elim: n => // n IHn.
+  exact: subset_trans sHH' (commgSS _ _).
+suffices IHn n: #|G^`(n)| <= (#|G|.-1 - n).+1.
+  by exists #|G|.-1; rewrite [G^`(_)]card_le1_trivg ?(leq_trans (IHn _)) ?subnn.
+elim: n => [|n IHn]; first by rewrite subn0 prednK.
+rewrite dergSn subnS -ltnS.
+have [-> | ntGn] := eqVneq G^`(n) 1; first by rewrite commG1 cards1.
+case: (_ - _) IHn => [|n']; first by rewrite leqNgt cardG_gt1 ntGn.
+by apply: leq_trans (proper_card _); exact: sol_der1_proper (der_sub _ _) _.
+Qed.
+
+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).
+Proof.
+move/(solvableS (subsetIr D G)); case/derivedP=> n Gn1; apply/derivedP.
+by exists n; rewrite /= -morphimIdom -morphim_der ?subsetIl // Gn1 morphim1.
+Qed.
+
+Lemma injm_sol : 'injm f -> G \subset D -> solvable (f @* G) = solvable G.
+Proof.
+move=> injf sGD; apply/idP/idP; last exact: morphim_sol.
+case/derivedP=> n Gn1; apply/derivedP; exists n; apply/trivgP.
+rewrite -(injmSK injf) ?(subset_trans (der_sub _ _)) ?morphim_der //.
+by rewrite Gn1 morphim1.
+Qed.
+
+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.
+Proof. by case/isogP=> f injf <-; rewrite injm_sol. Qed.
+
+Lemma quotient_sol G H : solvable G -> solvable (G / H).
+Proof. exact: morphim_sol. Qed.
+
+Lemma series_sol G H : H <| G -> solvable G = solvable H && solvable (G / H).
+Proof.
+case/andP=> sHG nHG; apply/idP/andP=> [solG | [solH solGH]].
+  by rewrite quotient_sol // (solvableS sHG).
+apply/forall_inP=> K /subsetIP[sKG sK'K].
+suffices sKH: K \subset H by rewrite (forall_inP solH) // subsetI sKH.
+have nHK := subset_trans sKG nHG.
+rewrite -quotient_sub1 // subG1 (forall_inP solGH) //.
+by rewrite subsetI -morphimR ?morphimS.
+Qed.
+
+Lemma metacyclic_sol G : metacyclic G -> solvable G.
+Proof.
+case/metacyclicP=> K [cycK nsKG cycGq].
+by rewrite (series_sol nsKG) !abelian_sol ?cyclic_abelian.
+Qed.
+
+End QuotientSol.