Module-valued stalks over a topological space

For a ring presheaf R on X, the stalk of a presheaf of R-modules is a module over the ring stalk. The functor uses Mathlib's module-colimit construction; its underlying module is linearly equivalent to the usual germ stalk. A commutative-ring specialization retains the scalar presentation used by scheme stalks.

Main definitions

• PresheafOfModules.stalkRingCocone and PresheafOfModules.stalkRingIsColimit lift the ring-stalk colimit through the forgetful functor to rings.
• PresheafOfModules.stalkFunctorOfIsColimit takes module stalks using a chosen colimit cocone of the neighborhood ring diagram.
• PresheafOfModules.neighborhoodStalkFunctor takes the module colimit on open neighborhoods over a general ring presheaf.
• PresheafOfModules.stalkFunctor first restricts a module presheaf to neighborhoods.
• PresheafOfModules.stalkLinearEquiv identifies its value with the usual germ stalk.
• PresheafOfModules.stalkRingComparisonIso compares the general and commutative stalk rings; PresheafOfModules.commStalkAddEquiv compares their module objects.

Main results

PresheafOfModules.stalkLinearEquiv identifies the bundled module stalk with the usual germ stalk as modules over an arbitrary ring stalk, with no sheaf or scheme hypothesis.

Implementation notes

The ring stalk is a colimit in rings. For a commutative-ring presheaf, forgetting commutativity preserves this colimit and yields the scheme-compatible cocone. The two colimit points are canonically isomorphic. The linear comparisons check scalar multiplication on germ representatives using the corresponding germ scalar lemma.

References

Mathlib's PresheafOfModules.colimitFunctor, PresheafOfModules.pushforward₀, and TopCat.Presheaf.stalkFunctor provide the constructions used here.

Tags

module presheaf, stalk, germs, colimit

noncomputable def PresheafOfModules.stalkRingCocone (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat)))

Forgetting commutativity makes the ring-stalk cocone available to Mathlib's module-colimit construction.

Equations

• PresheafOfModules.stalkRingCocone X R x = (CategoryTheory.forget₂ CommRingCat RingCat).mapCocone (CategoryTheory.Limits.colimit.cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp R))

noncomputable def PresheafOfModules.stalkRingIsColimit (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) : CategoryTheory.Limits.IsColimit (stalkRingCocone X R x)

Forgetting commutativity preserves this filtered colimit, supplying the witness needed by PresheafOfModules.colimitFunctor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PresheafOfModules.stalkRingComparisonIso (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) : (have this := CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat); this).stalk x ≅ (CategoryTheory.forget₂ CommRingCat RingCat).obj (R.stalk x)

The general-ring stalk and the underlying ring of the commutative stalk are the two colimit points of the same neighborhood diagram.

Equations

• One or more equations did not get rendered due to their size.

theorem PresheafOfModules.stalkRingComparisonIso_hom_germ (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(R.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (stalkRingComparisonIso X R x).hom) ((CategoryTheory.ConcreteCategory.hom ((have this := CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat); this).germ U x hx)) r) = (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r

The scalar-ring comparison sends a general-ring germ to the same germ in the commutative-ring stalk.

noncomputable def PresheafOfModules.stalkFunctorOfIsColimit (X : TopCat) (S : TopCat.Presheaf RingCat X) (x : ↑X) {c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp S)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Functor (PresheafOfModules S) (ModuleCat ↑c.pt)

Restrict module presheaves to neighborhoods and take their colimit over a chosen colimit cocone of rings. Both the ordinary ring stalk and the commutative-ring stalk presentation specialize this construction.

Equations

• PresheafOfModules.stalkFunctorOfIsColimit X S x hc = (PresheafOfModules.pushforward₀ (TopologicalSpace.OpenNhds.inclusion x) S).comp (PresheafOfModules.colimitFunctor hc)

noncomputable def PresheafOfModules.neighborhoodStalkFunctor (X : TopCat) (S : TopCat.Presheaf RingCat X) (x : ↑X) : CategoryTheory.Functor (PresheafOfModules ((TopologicalSpace.OpenNhds.inclusion x).op.comp S)) (ModuleCat ↑(S.stalk x))

Module colimit on neighborhoods of a point over an arbitrary ring presheaf.

Equations

• PresheafOfModules.neighborhoodStalkFunctor X S x = PresheafOfModules.colimitFunctor (CategoryTheory.Limits.colimit.isColimit ((TopologicalSpace.OpenNhds.inclusion x).op.comp S))

noncomputable def PresheafOfModules.stalkFunctor (X : TopCat) (S : TopCat.Presheaf RingCat X) (x : ↑X) : CategoryTheory.Functor (PresheafOfModules S) (ModuleCat ↑(S.stalk x))

For a ring presheaf, restrict modules to neighborhoods and take their colimit over the ring stalk.

Equations

• PresheafOfModules.stalkFunctor X S x = PresheafOfModules.stalkFunctorOfIsColimit X S x (CategoryTheory.Limits.colimit.isColimit ((TopologicalSpace.OpenNhds.inclusion x).op.comp S))

def PresheafOfModules.stalkLinearEquiv (X : TopCat) (S : TopCat.Presheaf RingCat X) (x : ↑X) (M : PresheafOfModules S) : ↑((stalkFunctor X S x).obj M) ≃ₗ[↑(S.stalk x)] ↑(TopCat.Presheaf.stalk M.presheaf x)

The bundled module stalk and the germ stalk have the same elements and scalar action.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PresheafOfModules.commNeighborhoodStalkFunctor (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) : CategoryTheory.Functor (PresheafOfModules ((TopologicalSpace.OpenNhds.inclusion x).op.comp (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat)))) (ModuleCat ↑(R.stalk x))

Module colimit over neighborhoods in the commutative stalk-ring presentation.

Equations

• PresheafOfModules.commNeighborhoodStalkFunctor X R x = PresheafOfModules.colimitFunctor (PresheafOfModules.stalkRingIsColimit X R x)

noncomputable def PresheafOfModules.commStalkFunctor (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) : CategoryTheory.Functor (PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) (ModuleCat ↑(R.stalk x))

The commutative stalk-ring presentation, used by scheme stalks.

Equations

• One or more equations did not get rendered due to their size.

def PresheafOfModules.commStalkLinearEquiv (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) : ↑((commStalkFunctor X R x).obj M) ≃ₗ[↑(R.stalk x)] ↑(TopCat.Presheaf.stalk M.presheaf x)

Identity on germs identifies the commutative stalk-ring presentation with the ordinary germ stalk as modules over the commutative-ring stalk.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PresheafOfModules.commStalkAddEquiv (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) : ↑((commStalkFunctor X R x).obj M) ≃+ ↑((stalkFunctor X (have this := CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat); this) x).obj M)

The two module-colimit presentations have the same germ elements. This objectwise additive comparison complements PresheafOfModules.stalkRingComparisonIso on scalars.

Equations

• One or more equations did not get rendered due to their size.

theorem PresheafOfModules.commStalkAddEquiv_symm_smul (X : TopCat) (R : TopCat.Presheaf CommRingCat X) (x : ↑X) (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) (r : ↑((have this := CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat); this).stalk x)) (m : ↑((stalkFunctor X (have this := CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat); this) x).obj M)) : (commStalkAddEquiv X R x M).symm (r • m) = (CategoryTheory.ConcreteCategory.hom (stalkRingComparisonIso X R x).hom) r • (commStalkAddEquiv X R x M).symm m

The additive comparison respects scalar multiplication through the canonical ring-stalk isomorphism.