English
Compositions of center after successive comaps along mk' maps behave compatibly under multiple steps in the quotient lattice.
Русский
Составления центра после последовательных сопоставлений через mk' отображения ведут себя совместимо в цепи квотирования.
LaTeX
$$$((\\mathrm{Subgroup.center}\\;((G/ H_1) / H_2)).comap (\\mathrm{mk}' H_2)).comap (\\mathrm{mk}' H_1) = (\\mathrm{Subgroup.center}\\; (G / (H_2.comap (\\mathrm{mk}' H_1)))).comap (\\mathrm{mk}' (H_2.comap (\\mathrm{mk}' H_1)))$$$
Lean4
@[to_additive]
theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] :
((Subgroup.center ((G ⧸ H₁) ⧸ H₂)).comap (mk' H₂)).comap (mk' H₁) =
(Subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) :=
by
ext x
simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul, eq_iff_div_mem, mk_div]
