English
If f: G →* H has kernel contained in the center of G and H is nilpotent, then G is nilpotent.
Русский
Если ядро f лежит в центре G и H нильпотентна, то G нильпотентна.
LaTeX
$$IsNilpotent(H) \\Rightarrow IsNilpotent(G) given f with f.ker ≤ center G$$
Lean4
/-- The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained
in the center -/
theorem isNilpotent_of_ker_le_center {H : Type*} [Group H] (f : G →* H) (hf1 : f.ker ≤ center G) (hH : IsNilpotent H) :
IsNilpotent G := by
rw [nilpotent_iff_lowerCentralSeries] at *
rcases hH with ⟨n, hn⟩
use n + 1
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)
