From 0b48570313b9f65b71eae00f767821bf804e2502 Mon Sep 17 00:00:00 2001
From: ineswright <ineswright7@gmail.com>
Date: Sat, 28 Aug 2021 17:56:07 +0000
Subject: [PATCH] feat(group_theory/nilpotent): add subgroups of nilpotent
 group are nilpotent (#8854)

Co-authored-by: ineswright <52750254+ineswright@users.noreply.github.com>
---
 src/group_theory/nilpotent.lean | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/group_theory/nilpotent.lean b/src/group_theory/nilpotent.lean
index aad568bffcd41..22783cbf0b622 100644
--- a/src/group_theory/nilpotent.lean
+++ b/src/group_theory/nilpotent.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kevin Buzzard
+Authors: Kevin Buzzard, Ines Wright
 -/
 
 import group_theory.general_commutator
@@ -265,6 +265,11 @@ lemma mem_lower_central_series_succ_iff (n : ℕ) (q : G) :
   q ∈ closure {x | ∃ (p ∈ lower_central_series G n) (q ∈ (⊤ : subgroup G)), p * q * p⁻¹ * q⁻¹ = x}
 := iff.rfl
 
+lemma lower_central_series_succ (n : ℕ) :
+  lower_central_series G (n + 1) =
+  closure {x | ∃ (p ∈ lower_central_series G n) (q ∈ (⊤ : subgroup G)), p * q * p⁻¹ * q⁻¹ = x} :=
+rfl
+
 instance (n : ℕ) : normal (lower_central_series G n) :=
 begin
   induction n with d hd,
@@ -308,6 +313,28 @@ begin
     use [lower_central_series G, lower_central_series_is_descending_central_series, h] },
 end
 
+lemma lower_central_series_map_subtype_le (H : subgroup G) (n : ℕ) :
+  (lower_central_series H n).map H.subtype ≤ lower_central_series G n :=
+begin
+  induction n with d hd,
+  { simp },
+  { rw [lower_central_series_succ, lower_central_series_succ, monoid_hom.map_closure],
+    apply subgroup.closure_mono,
+    rintros x1 ⟨x2, ⟨x3, hx3, x4, hx4, rfl⟩, rfl⟩,
+    exact ⟨x3, (hd (mem_map.mpr ⟨x3, hx3, rfl⟩)), x4, by simp⟩ }
+end
+
+instance subgroup.is_nilpotent (H : subgroup G) [hG : is_nilpotent G] :
+  is_nilpotent H :=
+begin
+  rw nilpotent_iff_lower_central_series at *,
+  rcases hG with ⟨n, hG⟩,
+  use n,
+  have := lower_central_series_map_subtype_le H n,
+  simp only [hG, set_like.le_def, mem_map, forall_apply_eq_imp_iff₂, exists_imp_distrib] at this,
+  exact eq_bot_iff.mpr (λ x hx, subtype.ext (this x hx)),
+end
+
 @[priority 100]
 instance is_nilpotent_of_subsingleton [subsingleton G] : is_nilpotent G :=
 nilpotent_iff_lower_central_series.2 ⟨0, subsingleton.elim ⊤ ⊥⟩