quotientMap_mk — Mathlib

English

If J ≤ I.comap f and I.comap f ≤ J, then quotientMap I f H is injective.

Русский

Если J ≤ I.comap f и I.comap f ≤ J, тогда quotientMap I f H инъективен.

LaTeX

$$$J \le I^{\mathrm{comap} f}$ and $I^{\mathrm{comap} f} \le J \Rightarrow \text{injective}(\text{quotientMap } I f H)$$$

Lean4

@[simp]
theorem quotientMap_mk {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S} {H : J ≤ I.comap f}
    {x : R} : quotientMap I f H (Quotient.mk J x) = Quotient.mk I (f x) :=
  Quotient.lift_mk J _ _

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