toPiLocalization — Mathlib

English

The canonical ring homomorphism from a commutative semiring to the product of its localizations at all maximal ideals is injective.

Русский

Каноническое кольцо-гомоморфизм от коммутативного полукольца к произведению локализаций по всем максимальным идеалам инъективен.

LaTeX

$$$R \to \prod_{\mathfrak m \in \mathrm{MaxSpec}(R)} R_{\mathfrak m} \quad\text{is injective}$$$

Lean4

/-- The canonical ring homomorphism from a commutative semiring to the product of its
localizations at all maximal ideals. It is always injective. -/
def toPiLocalization : R →+* PiLocalization R :=
  algebraMap R _

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