English
For J ≤ I ≤ R and K ≤ J, the two ways of pulling back along factor maps agree: (I.map(mk J)).comap (factor K) = I.map (mk K).
Русский
При J ≤ I и K ≤ J обе траектории отображения обратно по точечным картам факторизации дают одно и то же множество: (I.map(mk J)).comap (factor K) = I.map (mk K).
LaTeX
$$$(I.map (mk J)).comap (factor K) = I.map (mk K)$, при условиях $J \le I$ и $K \le J$.$$
Lean4
theorem map_mk_comap_factor [J.IsTwoSided] [K.IsTwoSided] (hIJ : J ≤ I) (hJK : K ≤ J) :
(I.map (mk J)).comap (factor hJK) = I.map (mk K) := by
ext x
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rcases mem_image_of_mem_map_of_surjective (mk J) Quotient.mk_surjective h with ⟨r, hr, eq⟩
have : x - ((mk K) r) ∈ J.map (mk K) := by simp [← factor_ker hJK, ← eq]
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective this with ⟨s, hs, eq'⟩
rw [← add_sub_cancel ((mk K) r) x, ← eq', ← map_add]
exact mem_map_of_mem (mk K) (Submodule.add_mem _ hr (hIJ hs))
· rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective h with ⟨r, hr, eq⟩
simpa only [← eq] using mem_map_of_mem (mk J) hr
