English
The composition of two quotient maps along a compatible commutative square equals another quotient map.
Русский
Составление двух отображений частного вдоль совместного квадрата равно другому отображению частного.
LaTeX
$$$(quotientMap I g' \circ quotientMap (I.comap g') f) = (quotientMap I f' \circ quotientMap (I.comap f') g)$$$
Lean4
/-- Commutativity of a square is preserved when taking quotients by an ideal. -/
theorem comp_quotientMap_eq_of_comp_eq {R' S' : Type*} [Ring R'] [Ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'}
{g' : S →+* S'} (hfg : f'.comp g = g'.comp f) (I : Ideal S') [I.IsTwoSided] :
let leq := le_of_eq (_root_.trans (comap_comap f g') (hfg ▸ comap_comap g f'))
(quotientMap I g' le_rfl).comp (quotientMap (I.comap g') f le_rfl) =
(quotientMap I f' le_rfl).comp (quotientMap (I.comap f') g leq) :=
by
refine RingHom.ext fun a => ?_
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
simp only [RingHom.comp_apply, quotientMap_mk]
exact (Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm (hfg ▸ f'.comp_apply g r))
