Library MathComp.nilpotent

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.


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 Bcoset B @*^-1 'Z(A / B)) 1.

End SeriesDefs.

Definition lower_central_at n := lower_central_at_rec n.-1.

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 :=
  [ (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.

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_inPH; rewrite commG1 setIid -subG1. Qed.

Lemma nilpotentS A B : B \subset Anilpotent Anilpotent B.
Proof.
movesBA nilA; apply/forall_inPH 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 GH \subset GH :!=: 1 → A \subset 'N_G(H)
  [~: H, A] \proper H.
Proof.
movenilG sHG ntH; rewrite subsetI properE; case/andPsAG nHA.
rewrite (subset_trans (commgS H (subset_gen A))) ?commg_subl ?gen_subG //.
apply: contra ntHsHR; have:= forallP nilG H; rewrite subsetI sHG.
by rewrite (subset_trans sHR) ?commgS.
Qed.

Lemma nil_comm_properr G A H :
    nilpotent GH \subset GH :!=: 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 slast 1%G s = Gnilpotent G.
Proof.
movecGs defG; apply/forall_inPH /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.
movedefG; 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 = GA^`(n) \* B^`(n) = G^`(n).
Proof. by movedefG; elim: n ⇒ {defG}// n; apply: (lcn_cprod 2). Qed.

Lemma der_dprod n A B G : A \x B = GA^`(n) \x B^`(n) = G^`(n).
Proof. by movedefG; 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_inPH /subsetIP[sHG sHR].
  rewrite -subG1 {}Ln1; elim: n ⇒ // n IHn.
  by rewrite (subset_trans sHR) ?commSg.
pose m := #|G|.-1; 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 Greflect ('L_n.+1(G) = 1) (nil_class G n).
Proof.
rewrite nilpotent_class /nil_class; set s := mkseq _ _.
set c := index 1 slt_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 ( n, 'L_n.+1(G) = 1) (nilpotent G).
Proof.
apply: (iffP idP) ⇒ [nilG | [n Ln1]].
  by (nil_class G); exact/lcn_nil_classP.
apply/forall_inPH /subsetIP[sHG sHR]; rewrite -subG1 -{}Ln1.
by elim: n ⇒ // n IHn; rewrite (subset_trans sHR) ?commSg.
Qed.

Lemma abelian_nil G : abelian Gnilpotent G.
Proof. by moveabG; apply/lcnP; 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/idPcGG.
  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 = Gnilpotent G = nilpotent A && nilpotent B.
Proof.
movedefG; 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; (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 movecGH; rewrite -(cprod_nil (cprodEY cGH)) /= cent_joinEr. Qed.

Lemma dprod_nil A B G : A \x B = Gnilpotent 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
  → ( i, P inilpotent (A_ i)) → nilpotent G.
Proof.
movedefG 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 : hZ : GFunctor.pmap, @upper_central_at n = hZ.
Proof.
elim: n ⇒ [|n' [hZ defZ]]; first by trivGfun_pgFun.
by [pgFun of center %% hZ]; rewrite /= -defZ.
Qed.


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/setPx; 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.
- movecAB {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 movef 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.
movedefG; 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 ( n, 'Z_n(G) = G) (nilpotent G).
Proof.
apply: (iffP (lcnP G)) ⇒ [] [n /eqP clGn];
  by n; apply/eqP; rewrite ucn_lcnP in clGn ×.
Qed.

Lemma ucn_nil_classP n G :
  nilpotent Greflect ('Z_n(G) = G) (nil_class G n).
Proof.
movenilG; 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; 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 Df @* 'L_n(G) = 'L_n(f @* G).
Proof.
movesHG; case: n ⇒ //; elim⇒ // n IHn.
by rewrite !lcnSn -IHn morphimR // (subset_trans _ sHG) // lcn_sub.
Qed.

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

Lemma morphim_nil G : nilpotent Gnilpotent (f @* G).
Proof.
case/ucnPn ZnG; apply/ucnP; n; apply/eqP.
by rewrite eqEsubset ucn_sub /= -{1}ZnG morphim_ucn.
Qed.

Lemma injm_nil G : 'injm fG \subset Dnilpotent (f @* G) = nilpotent G.
Proof.
moveinjf sGD; apply/idP/idP; last exact: morphim_nil.
case/ucnPn; rewrite -injm_ucn // ⇒ /injm_morphim_inj defZ.
by apply/ucnP; n; rewrite defZ ?(subset_trans (ucn_sub n G)).
Qed.

Lemma nil_class_morphim G : nilpotent Gnil_class (f @* G) nil_class G.
Proof.
movenilG; 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 fG \subset Dnil_class (f @* G) = nil_class G.
Proof.
moveinjf 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/setPZx; 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 Lnilpotent G = nilpotent L.
Proof. by case/isogPf injf <-; rewrite injm_nil. Qed.

Lemma isog_nil_class rT G (L : {group rT}) :
  G \isog Lnil_class G = nil_class L.
Proof. by case/isogPf injf <-; rewrite nil_class_injm. Qed.

Lemma quotient_nil G H : nilpotent Gnilpotent (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/ucnPc nilGq; apply/ucnP; 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.
movenilG; 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 GH \subset G'N_G(H) \subset HG :=: H.
Proof.
movenilG sHG sNH; apply/eqP; rewrite eqEsubset sHG andbT; apply/negPnsGH.
have{nsGH} [i sZH []]: exists2 i, 'Z_i(G) \subset H & ¬ 'Z_i.+1(G) \subset H.
  case/ucnP: nilGn 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); [ 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 GH \proper GH \proper 'N_G(H).
Proof.
movenilG; 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 GH \subset GH <|<| G.
Proof.
movenilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) ⇒ // m IHm H.
rewrite ltnSleGHm 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 GH <| GH :&: 'Z(G) = 1 → H :=: 1.
Proof.
movenilG /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 GH <| GH :!=: 1 → H :&: 'Z(G) != 1.
Proof. by movenilG nsHG; apply: contraNneq ⇒ /TI_center_nil→. Qed.

Lemma center_nil_eq1 G : nilpotent G('Z(G) == 1) = (G :==: 1).
Proof.
movenilG; 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 Gcyclic (G / G^`(1)) → cyclic G.
Proof.
movenG; 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 Gsolvable G.
Proof.
movenilG; apply/forall_inPH /subsetIP[sHG sHH'].
by rewrite (forall_inP nilG) // subsetI sHG (subset_trans sHH') ?commgS.
Qed.

Lemma abelian_sol G : abelian Gsolvable 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 Gsolvable Gsolvable H.
Proof.
movesHG solG; apply/forall_inPK /subsetIP[sKH sKK'].
by rewrite (forall_inP solG) // subsetI (subset_trans sKH).
Qed.

Lemma sol_der1_proper G H :
  solvable GH \subset GH :!=: 1 → H^`(1) \proper H.
Proof.
movesolG sHG ntH; rewrite properE comm_subG //; apply: implyP ntH.
by have:= forallP solG H; rewrite subsetI sHG implybNN.
Qed.

Lemma derivedP G : reflect ( n, G^`(n) = 1) (solvable G).
Proof.
apply: (iffP idP) ⇒ [solG | [n solGn]]; last first.
  apply/forall_inPH /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 #|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 Gsolvable (f @* G).
Proof.
move/(solvableS (subsetIr D G)); case/derivedPn Gn1; apply/derivedP.
by n; rewrite /= -morphimIdom -morphim_der ?subsetIl // Gn1 morphim1.
Qed.

Lemma injm_sol : 'injm fG \subset Dsolvable (f @* G) = solvable G.
Proof.
moveinjf sGD; apply/idP/idP; last exact: morphim_sol.
case/derivedPn Gn1; apply/derivedP; 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 Lsolvable G = solvable L.
Proof. by case/isogPf injf <-; rewrite injm_sol. Qed.

Lemma quotient_sol G H : solvable Gsolvable (G / H).
Proof. exact: morphim_sol. Qed.

Lemma series_sol G H : H <| Gsolvable G = solvable H && solvable (G / H).
Proof.
case/andPsHG nHG; apply/idP/andP⇒ [solG | [solH solGH]].
  by rewrite quotient_sol // (solvableS sHG).
apply/forall_inPK /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 Gsolvable G.
Proof.
case/metacyclicPK [cycK nsKG cycGq].
by rewrite (series_sol nsKG) !abelian_sol ?cyclic_abelian.
Qed.

End QuotientSol.