Commit 2024-10-19 19:20 19e2abfd

feat (AlgebraicGeometry/Modules): stalks of the sheaf M^~ (#14247) Construct the isomorphism of $R$-modules from the stalk of the sheaf $M^{~}$ on $Spec(R)$ to the localization $M_x$ as an $R$-module, where $R$ is a commutative ring and $M$ is an $R$-module.

Main definition

• ModuleCat.tilde.stalkIso: The isomorphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal corresponding to x.

Technical note

To get the R-module structure on the stalks on M^~, we had to define ModuleCat.tildeInModuleCat, which is M^~ seen as sheaf of R-modules. We get it by applying a forgetful functor to ModuleCat.tilde M. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.