English
For a local ring R and any morphism f, the germ at the top open of Spec R composed with the isomorphism stalkClosedPointIso R is equal to the canonical global sections map ΓSpecIso R; i.e., the germ-map compatibility with the closed-point–stalk isomorphism agrees with the Gamma construction.
Русский
Для локального кольца R и любой морфизм f, композиция герма над открытым верхом Spec R с изоморфизмом stalkClosedPointIso R равна каноническому отображению глобальных секций ΓSpecIso R; т.е. совместимость герма с изоморфизмом замкнутой точки стежки совпадает с построением Γ.
LaTeX
$$$ (\\mathrm{Spec}\\, R).\\mathrm{presheaf}.\\mathrm{germ}\\;\\top\\;(\\mathrm{closedPoint}\\;R)\\;\\mathrm{trivial} \\;\\gg \\, (\\mathrm{stalkClosedPointIso}\\;R).{\\mathrm hom} = (\\mathrm{Scheme}.\\GammaSpecIso\\;R).{\\mathrm hom} $$$
Lean4
@[reassoc (attr := simp)]
theorem germ_stalkClosedPointIso_hom :
(Spec R).presheaf.germ ⊤ (closedPoint _) trivial ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom := by
rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]
