English
There is a canonical isomorphism between the stalk-to-fiber map and the localization map on stalks, expressing that evaluating a section at a point corresponds to taking its localization at that point.
Русский
Существует каноническое изоморфизм между стэково-файберным отображением и локализационным отображением на стэках, выражающий, что вычисление секции в точке эквивалентно взятию её локализации в этой точке.
LaTeX
$$$\forall x,\; (stalkToFiberLinearMap\,M\,x) = (toStalk\,M\,x)^{\ast}$$$
Lean4
/-- If `U` is an open subset of `Spec R`, this is the morphism of `R`-modules from `M` to
`M^~(U)`.
-/
noncomputable def toOpen (U : Opens (PrimeSpectrum.Top R)) : ModuleCat.of R M ⟶ (tildeInModuleCat M).obj (op U) :=
-- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(Y := ...)`
-- This suggests `restrictScalars` needs to be redesigned.
ModuleCat.ofHom (Y := (tildeInModuleCat M).obj (op U))
{ toFun := fun f =>
⟨fun x ↦ LocalizedModule.mkLinearMap _ _ f, fun x ↦
⟨U, x.2, 𝟙 _, f, 1, fun y ↦ ⟨(Ideal.ne_top_iff_one _).1 y.1.2.1, by simp⟩⟩⟩
map_add' := fun f g => Subtype.eq <| funext fun x ↦ LinearMap.map_add _ _ _
map_smul' := fun r m =>
by
simp only [isLocallyFraction_pred, LocalizedModule.mkLinearMap_apply, LinearMapClass.map_smul, RingHom.id_apply]
rfl }
