English
The stalk-to-fiber map applied to a stalk obtained from toStalk is equal to a canonical localization map, i.e., the fiber over a point is the localization of the module at that point.
Русский
Отображение stalkToFiberLinearMap, применённое к стэку из toStalk, равно каноническому отображению локализации; волокно над точкой есть локализация модуля в этой точке.
LaTeX
$$$(stalkToFiberLinearMap\,M\,x).hom (toStalk\,M\,x\,m) = LocalizedModule.mk m 1$$$
Lean4
@[reassoc (attr := simp), elementwise (attr := simp)]
theorem toOpen_germ (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) :
toOpen M U ≫ M.tildeInModuleCat.germ U x hx = toStalk M x := by
rw [← toOpen_res M ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]; rfl
