English
The image of a nilpotent group under a surjective homomorphism is nilpotent.
Русский
Образ нильпотентной группы при сюръективном одоморфизме остаётся нильпотентным.
LaTeX
$$$IsNilpotent(G) \\Rightarrow IsNilpotent(G')$ for surjective f: G →* G'$$
Lean4
/-- The range of a surjective homomorphism from a nilpotent group is nilpotent -/
theorem nilpotent_of_surjective {G' : Type*} [Group G'] [h : IsNilpotent G] (f : G →* G') (hf : Function.Surjective f) :
IsNilpotent G' := by
rcases h with ⟨n, hn⟩
use n
apply eq_top_iff.mpr
calc
⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
_ = Subgroup.map f ⊤ := (MonoidHom.range_eq_map _)
_ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
_ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n
