quotientMap_comp_mk — Mathlib

English

If J = I.map f then there is an alg equivalence (A/ I) ≃ₐ B/ J induced by an algebra equivalence f.

Русский

Если J = I.map f, существует алгебраическое эквивалентное отображение (A/I) ≃ₐ B/J, индуцированное алгебра-эквивалентом f.

LaTeX

$$$\text{quotientEquivAlg } f : (A/ I) \simeq_A (B/ J)$ with $J = I.map f$$$

Lean4

theorem quotientMap_comp_mk {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S}
    (H : J ≤ I.comap f) : (quotientMap I f H).comp (Quotient.mk J) = (Quotient.mk I).comp f :=
  RingHom.ext fun x => by simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

Похожие утверждения