quotientInfRingEquivPiQuotient — Mathlib

English

Under the coprimality hypothesis, the product map R → ∏ R/I_i is surjective.

Русский

При условии взаимной простоты идеалов отображение R → ∏ R/I_i сюръективно.

LaTeX

$$$\text{pi_quotient_surjective } I$$$

Lean4

/-- **Chinese Remainder Theorem**. Eisenbud Ex.2.6.
Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/
noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R) (hf : Pairwise (IsCoprime on f)) :
    (R ⧸ ⨅ i, f i) ≃+* ∀ i, R ⧸ f i :=
  { Equiv.ofBijective _ ⟨quotientInfToPiQuotient_inj f, quotientInfToPiQuotient_surj hf⟩,
    quotientInfToPiQuotient f with }

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