Module structures on scheme-module stalks #
The stalk of an 𝒪_X-module carries the action of the original commutative local ring
𝒪_{X,x}. This exposes Mathlib's presheaf stalk action through the scheme-module presentation.
@[instance_reducible]
noncomputable instance
AlgebraicGeometry.Scheme.Modules.stalkModule
{X : Scheme}
(M : X.Modules)
(x : ↥X)
:
The stalk of a scheme module is a module over the scheme's commutative local ring.
Equations
- M.stalkModule x = { smul := AlgebraicGeometry.Scheme.Modules.stalkModule._aux_1 M x, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
theorem
AlgebraicGeometry.Scheme.Modules.germ_smul
{X : Scheme}
(M : X.Modules)
(x : ↥X)
(U : X.Opens)
(hx : x ∈ U)
(r : ↑(X.presheaf.obj (Opposite.op U)))
(m : ↑(M.presheaf.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (M.presheaf.germ U x hx)) (r • m) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) r • (CategoryTheory.ConcreteCategory.hom (M.presheaf.germ U x hx)) m
The module germ of a scalar multiple is the local-ring germ acting on the module germ.