liftSupQuotQuotMk — Mathlib

English

There is a canonical lifting map from R/(I ⊔ J) to (R/I)/J'.

Русский

Существуют канонические подъемные отображения из R/(I ⊔ J) в (R/I)/J'.

LaTeX

$$$\\text{liftSupQuotQuotMk} : R \\big/ (I \\sqcup J) \\to+* (R \\!/ I) \\!/ (J \\mapsto)$$$$

Lean4

/-- The ring homomorphism `R/(I ⊔ J) → (R/I)/J' `induced by `quotQuotMk` -/
def liftSupQuotQuotMk (I J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) :=
  Ideal.Quotient.lift (I ⊔ J) (quotQuotMk I J) (ker_quotQuotMk I J).symm.le

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