quotientMap_algebraMap — Mathlib

English

The kernel of the quotient map after mapping through mk is equal to the image of the kernel under mk.

Русский

Ядро отображения частного после отображения через mk равно образу ядра под mk.

LaTeX

$$$\ker (\text{quotientMap } (J.map _) (\operatorname{Quotient.mk I}) le\_comap\_map) = I.map (\operatorname{Quotient.mk J})$$$

Lean4

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

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