English
If f: G →* H has kernel contained in the center and H is nilpotent, then nilpotency class of G is bounded by nilpotency class of H plus 1.
Русский
Если ядро f ⊆ Z(G) и H нильпотентна, то класс нильпотентности G ≤ klass(H) + 1.
LaTeX
$$Group.nilpotencyClass (hG := isNilpotent_of_ker_le_center f hf1 hH) ≤ Group.nilpotencyClass H + 1$$
Lean4
theorem nilpotencyClass_le_of_ker_le_center {H : Type*} [Group H] (f : G →* H) (hf1 : f.ker ≤ center G)
(hH : IsNilpotent H) :
Group.nilpotencyClass (hG := isNilpotent_of_ker_le_center f hf1 hH) ≤ Group.nilpotencyClass H + 1 :=
by
haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
classical apply Nat.find_min'
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
rw [eq_bot_iff]
apply le_trans (lowerCentralSeries.map f _)
simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]
