English
Let R be a commutative ring. For any open subset U of the prime spectrum Spec(R) and any point x ∈ U, there is a canonical ring homomorphism from the ring of sections of the structure sheaf on U to the localization of R at the prime corresponding to x. This map evaluates a section at x, yielding an element of R localized at the prime p = x.asIdeal.
Русский
Пусть R — коммутативное кольцо. Пусть U — открытое подмножество Спец(R), а точка x принадлежит U. Существует канонический кольцевой гомоморфизм из кольца секций структуры sheaf на U в локализацию R вprime идеале p = x.asIdeal. Этот отображение вычисляет секцию в точке x, получая элемент локализации R по p.
LaTeX
$$$openToLocalization(R, U, x, hx) : \\Gamma(U, \\mathcal{O}_R) \\to R_{\\mathfrak p},\\quad s \\mapsto s(x) \\in R_{\\mathfrak p},$$$
Lean4
/-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`,
implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates
the section on the point corresponding to a given prime ideal. -/
def openToLocalization (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
(structureSheaf R).1.obj (op U) ⟶ CommRingCat.of (Localization.AtPrime x.asIdeal) :=
CommRingCat.ofHom
{ toFun s := (s.1 ⟨x, hx⟩ :)
map_one' := rfl
map_mul' _ _ := rfl
map_zero' := rfl
map_add' _ _ := rfl }
