English
The germ of a section followed by the stalk-to-fiber map equals the open-to-localization map; i.e., the germ map factors through the localization that assigns an element to its image at the stalk, consistent with the open localization.
Русский
Ограничение секции через зерно и затем переход со стержня к модулю локализации совпадает с отображением в локализацию; соответствие открытым локализациям.
LaTeX
$$$\\text{germ}_{U,x} \\circ (\\text{stalkToFiberRingHom } 𝒜\\ x) = (\\text{openToLocalization } 𝒜\\ U\\ x\\ hx)$$$
Lean4
/-- The ring map from `A⁰_ f` to the global sections of the structure sheaf of the projective spectrum
of `A` restricted to the basic open set `D(f)`.
Mathematically, the map is the same as `awayToSection`.
-/
def awayToΓ (f) : CommRingCat.of (A⁰_ f) ⟶ LocallyRingedSpace.Γ.obj (op <| Proj| pbo f) :=
awayToSection 𝒜 f ≫ (ProjectiveSpectrum.Proj.structureSheaf 𝒜).1.map (homOfLE (Opens.isOpenEmbedding_obj_top _).le).op
