English
The morphism awayToΓ equals the composite of awayToSection with the structure sheaf's map via the gamma adjunction; i.e., the global sections map from the away-localization to the structure sheaf coincides with the gamma adjunction.
Русский
awayToΓ равен композиции awayToSection с отображением структуры sheaf через гамма-адъюнкцию; глобальные сечения соответствуют гамма-адъюнкции.
LaTeX
$$$awayToΓ 𝒜 f = awayToSection 𝒜 f ≫ (Proj.structureSheaf 𝒜).1.map (homOfLE (Opens.isOpenEmbedding_obj_top _).le).op$$$
Lean4
/-- The ring homomorphism from the stalk of the structure sheaf of `Proj` at a point corresponding
to a homogeneous prime ideal `x` to the *homogeneous localization* at `x`,
formed by gluing the `openToLocalization` maps. -/
def stalkToFiberRingHom (x : ProjectiveSpectrum.top 𝒜) :
(Proj.structureSheaf 𝒜).presheaf.stalk x ⟶ CommRingCat.of (at x) :=
Limits.colimit.desc ((OpenNhds.inclusion x).op ⋙ (Proj.structureSheaf 𝒜).1)
{ pt := _
ι := { app := fun U => openToLocalization 𝒜 ((OpenNhds.inclusion _).obj U.unop) x U.unop.2 } }
