English
The upper central series step is the preimage under the canonical projection of the center of the quotient G/H; equivalently, it is the set of elements x in G such that for all y, the commutator lies in H.
Русский
Верхняя центральная ступень равна предобразу центра относительного множества G/H под каноническим отображением; эквиваленто это множество элементов x в G, для которых при любом y коммутатор лежит в H.
LaTeX
$$$\\operatorname{upperCentralSeriesStep}(H) = \\operatorname{comap}(\\mathrm{mk'}(H), \\operatorname{center}(G/H))$$$
Lean4
/-- The proof that `upperCentralSeriesStep H` is the preimage of the centre of `G/H` under
the canonical surjection. -/
theorem upperCentralSeriesStep_eq_comap_center : upperCentralSeriesStep H = Subgroup.comap (mk' H) (center (G ⧸ H)) :=
by
ext
rw [mem_comap, mem_center_iff, forall_mk]
apply forall_congr'
intro y
rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem, div_eq_mul_inv, mul_inv_rev,
mul_assoc]
