localizationToStalk_of — Mathlib

English

More explicit isomorphism describing the localization to stalk for mk' with AtPrime localizations.

Русский

Более явное описание изоморфизма локализации в локальный столб mk' с локализациями AtPrime.

LaTeX

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

Lean4

@[simp]
theorem localizationToStalk_of (x : PrimeSpectrum.Top R) (f : R) :
    localizationToStalk R x (algebraMap _ (Localization _) f) = toStalk R x f :=
  IsLocalization.lift_eq (S := Localization x.asIdeal.primeCompl) _ f

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