English
For the nth term of the upper central series of the quotient G/Z(G), its preimage under the natural projection equals the (n+1)st term of the upper central series of G.
Русский
Для n-го члена верхней центральной последовательности тождественного прообраза G/Z(G) его прообразом по естественному отображению равен (n+1)-й член верхней центральной последовательности G.
LaTeX
$$$\\operatorname{comap}(\\pi, Z(G))\\bigl(Z_n(G/Z(G))\\bigr) = Z_{n+1}(G)$$$
Lean4
theorem comap_upperCentralSeries_quotient_center (n : ℕ) :
comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ := by
induction n with
| zero => simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk', (upperCentralSeries_one G).symm]
| succ n ih =>
let Hn := upperCentralSeries (G ⧸ center G) n
calc
comap (mk' (center G)) (upperCentralSeriesStep Hn) =
comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) :=
by rw [upperCentralSeriesStep_eq_comap_center]
_ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
QuotientGroup.comap_comap_center
_ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
(comap_center_subst ih)
_ = upperCentralSeriesStep (upperCentralSeries G n.succ) := symm (upperCentralSeriesStep_eq_comap_center _)
