quotQuotToQuotSup — Mathlib

English

Let I ≤ J be ideals. Then comap (Quotient.mk I) (map (Quotient.mk I) J) = J.

Русский

Пусть I ≤ J — идеалы. Тогда comap (Quotient.mk I) (map (Quotient.mk I) J) = J.

LaTeX

$$$\\mathrm{Ideal.comap}\\big(\\mathrm{Ideal.Quotient.mk } I\\big)\\big(\\mathrm{Ideal.map}(\\mathrm{Ideal.Quotient.mk } I) J\\big) = J$$$

Lean4

/-- The ring homomorphism `(R/I)/J' -> R/(I ⊔ J)` induced by `quotLeftToQuotSup` where `J'`
  is the image of `J` in `R/I` -/
def quotQuotToQuotSup : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) →+* R ⧸ I ⊔ J :=
  Ideal.Quotient.lift (J.map (Ideal.Quotient.mk I)) (quotLeftToQuotSup I J) (ker_quotLeftToQuotSup I J).symm.le

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