English
If f: G →* H is surjective, then f maps the nth term of the upper central series of G into the nth term of the upper central series of H for all n.
Русский
Пусть f: G →* H сюръективно; тогда f отображает n-ю ступень верхней центральной серии G в n-ю ступень верхней центральной серии H для всех n.
LaTeX
$$$\\text{Surjective}(f) \\Rightarrow \\forall n, \\operatorname{map}(f, \\text{upperCentralSeries}(G,n)) \\le \\text{upperCentralSeries}(H,n)$$$
Lean4
theorem map {H : Type*} [Group H] {f : G →* H} (h : Function.Surjective f) (n : ℕ) :
Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n := by
induction n with
| zero => simp
| succ d hd =>
rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
rcases h y' with ⟨y, rfl⟩
simpa using hd (mem_map_of_mem f (hx y))
