quotientInfToPiQuotient — Mathlib

English

Injectivity of the canonical map from R/(⋂ i, I_i) to ∏ i R/I_i when all I_i are two‑sided and pairwise coprime.

Русский

Инъективность канонического отображения из R/(⋂ I_i) в ∏ R/I_i при попарно взаимно простых идeалах I_i.

LaTeX

$$$\text{Injective}(\operatorname{quotientInfToPiQuotient} I)$$$

Lean4

/-- The homomorphism from `R/(⋂ i, f i)` to `∏ i, (R / f i)` featured in the Chinese
  Remainder Theorem. It is bijective if the ideals `f i` are coprime. -/
def quotientInfToPiQuotient (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] : (R ⧸ ⨅ i, I i) →+* ∀ i, R ⧸ I i :=
  Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])

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