English
Under a group isomorphism e: H ≃* G, the nth upper central term is preserved via the comap/pullback: comap_e(upperCentralSeries(G,n)) = upperCentralSeries(H,n).
Русский
При изоморфизме групп e: H ≃* G н-ая ступень верхней центральной серии сохраняется через образ-обратное отображение: comap_e(upperCentralSeries(G,n)) = upperCentralSeries(H,n).
LaTeX
$$$\forall n,\ (\mathrm{upperCentralSeries}(G,n))^{e}=\mathrm{upperCentralSeries}(H,n).$$$
Lean4
@[simp]
theorem comap_upperCentralSeries {H : Type*} [Group H] (e : H ≃* G) :
∀ n, (upperCentralSeries G n).comap e = upperCentralSeries H n
| 0 => by simpa [MonoidHom.ker_eq_bot_iff] using e.injective
| n + 1 => by
ext
simp [mem_upperCentralSeries_succ_iff, ← comap_upperCentralSeries e n, ← e.toEquiv.forall_congr_right]
