Module structures on stalks of sheaves of modules #
The stalk of a sheaf of modules over a sheaf of rings is a module over the ring stalk.
For commutative coefficient rings, it also retains the module action
of the original commutative ring stalk when the coefficient sheaf forgets commutativity.
The instance SheafOfModules.stalkModule exposes Mathlib's commutative presheaf stalk module
structure independently of the internal Hom construction. For ordinary ring coefficients,
Mathlib's presheaf stalk instance applies directly to the underlying presheaf of modules.
The linear equivalence PresheafOfModules.sheafificationStalkEquiv identifies a module
presheaf stalk with its sheafification stalk, preserving the original commutative-ring
stalk as coefficient ring. Its forward and inverse maps are characterized on germs.
If finitely many sections generate the restriction of a sheaf of modules to a neighbourhood of
x, their germs span the stalk at x over the ring stalk
(SheafOfModules.GeneratingSections.span_germ_eq_top). Thus a linear map out of the stalk of a
sheaf of finite type is determined by its values on the germs of local generators.
The stalk of a sheaf of modules carries Mathlib's module structure over the stalk of the original commutative-ring sheaf. The carrier and action are unchanged by forgetting commutativity in the coefficient sheaf.
Equations
- P.stalkModule x = { smul := SheafOfModules.stalkModule._aux_1 P x, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
Sheafification preserves module stalks, linearly over the original commutative-ring stalk. The equivalence is induced by the unit of the sheafification adjunction.
Equations
Instances For
The sheafification stalk equivalence sends a germ to the germ of its unit image.
The inverse equivalence sends the germ of a unit image back to its original germ.
If finitely many sections generate the restriction of M to a neighbourhood U of x,
their germs span the stalk of M at x over the ring stalk.