English
For a graded algebra 𝒜, the stalk of Proj 𝒜 at a point is canonically isomorphic to the degree zero part of the corresponding homogeneous localization at the homogeneous prime ideal of that point.
Русский
Стержень Proj 𝒜 в точке эквивалентен нулевой степени локализации по одноимённому идеалу.
LaTeX
$$$\\text{stalkIso} 𝒜 : (\\Proj 𝒜).presheaf.stalk x \\cong \\mathsf{CommRing}.of(\\HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)$$$
Lean4
/-- The ring homomorphism that takes a section of the structure sheaf of `Proj` on the open set `U`,
implemented as a subtype of dependent functions to localizations at homogeneous prime ideals, and
evaluates the section on the point corresponding to a given homogeneous prime ideal. -/
def openToLocalization (U : Opens (ProjectiveSpectrum.top 𝒜)) (x : ProjectiveSpectrum.top 𝒜) (hx : x ∈ U) :
(Proj.structureSheaf 𝒜).1.obj (op U) ⟶ CommRingCat.of (at x) :=
CommRingCat.ofHom
{ toFun s := (s.1 ⟨x, hx⟩ :)
map_one' := rfl
map_mul' _ _ := rfl
map_zero' := rfl
map_add' _ _ := rfl }
