localizationToStalk — Mathlib

English

The canonical localization to stalk construction sends a localized fraction to the corresponding stalk element.

Русский

Каноническая локализация в локальный стек отправляет локализованную дробь к соответствующему элементу стека.

LaTeX

$$$ localizationToStalk\\_R x (IsLocalization.mk' (Localization AtPrime x.asIdeal) f s) = toStalk R x f $$$

Lean4

/-- The canonical ring homomorphism from the localization of `R` at `p` to the stalk
of the structure sheaf at the point `p`. -/
def localizationToStalk (x : PrimeSpectrum.Top R) :
    CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ (structureSheaf R).presheaf.stalk x :=
  CommRingCat.ofHom <| show Localization.AtPrime x.asIdeal →+* _ from IsLocalization.lift (isUnit_toStalk R x)

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