English
If f: G →* G' is surjective and G is nilpotent, then the nilpotency class of G' is at most the nilpotency class of G.
Русский
Если f: G →* G' сюръективно и G нильпотентна, то класс нильпотентности G' не превышает класс G.
LaTeX
$$Group.nilpotencyClass (hG := nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G$$
Lean4
/-- The nilpotency class of the range of a surjective homomorphism from a
nilpotent group is less or equal the nilpotency class of the domain -/
theorem nilpotencyClass_le_of_surjective {G' : Type*} [Group G'] (f : G →* G') (hf : Function.Surjective f)
[h : IsNilpotent G] : Group.nilpotencyClass (hG := nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G :=
by
classical apply Nat.find_mono
intro n hn
rw [eq_top_iff]
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
