English
The composed map from the stalk map to Spec factors through the isomorphisms of the local rings, giving a consistent description of stalk maps under the restriction from Proj to Spec.
Русский
Состыковка отображения stalkMap к Spec проходит через изоморфизмы локальных колец, обеспечивая согласованное описание stalkMap при ограничении Proj к Spec.
LaTeX
$$$$\text{toStalk\_stalkMap\_toSpec: } \mathcal{O}_{Proj} \to \mathcal{O}_{Spec}$$$$
Lean4
theorem stalkMap_toSpec (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
(toSpec 𝒜 f).stalkMap x =
(specStalkEquiv 𝒜 f x f_deg hm).hom ≫
(«Proj».stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
((«Proj».toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.isOpenEmbedding _) x).inv :=
CommRingCat.hom_ext <|
IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).base x).asIdeal.primeCompl (S :=
(«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) <|
CommRingCat.hom_ext_iff.mp <|
(toStalk_stalkMap_toSpec _ _ _).trans <| by rw [awayToΓ_ΓToStalk, ← toStalk_specStalkEquiv, Category.assoc]; rfl
