Module stalks and sheafification

Module sheafification preserves stalks over a sheaf of rings. The comparison is natural in the presheaf of modules. A chosen colimit cocone gives the same construction for ordinary ring and commutative-ring stalk presentations.

Main definitions

• PresheafOfModules.stalkRingSheaf packages the ring sheaf.
• PresheafOfModules.sheafStalkFunctor takes stalks of module sheaves.
• PresheafOfModules.stalkSheafificationApp is the stalk of the unit.

Main results

• PresheafOfModules.stalkSheafificationApp_isIso proves the unit is an isomorphism on module stalks.
• PresheafOfModules.stalkSheafificationIso bundles the natural isomorphism.

Implementation notes

The underlying additive comparison is the usual stalk map from a presheaf to its sheafification. The forgetful functor from modules to additive groups reflects the isomorphism; naturality follows from the sheafification unit.

References

Mathlib's TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso supplies the underlying stalk isomorphism.

Tags

module sheaf, sheafification, stalk, natural isomorphism

@[reducible, inline]

abbrev PresheafOfModules.stalkRingSheaf (X : TopCat) (R : TopCat.Presheaf RingCat X) (hR : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) R) : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat

Package a ring presheaf with its sheaf property.

Equations

• PresheafOfModules.stalkRingSheaf X R hR = { obj := R, property := hR }

noncomputable def PresheafOfModules.sheafStalkFunctor (X : TopCat) (R : TopCat.Presheaf RingCat X) (x : ↑X) {c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp R)} (hc : CategoryTheory.Limits.IsColimit c) (hR : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) R) : CategoryTheory.Functor (SheafOfModules (stalkRingSheaf X R hR)) (ModuleCat ↑c.pt)

The module-valued stalk functor on sheaves over the ring sheaf.

Equations

• PresheafOfModules.sheafStalkFunctor X R x hc hR = (SheafOfModules.forget (PresheafOfModules.stalkRingSheaf X R hR)).comp (PresheafOfModules.stalkFunctorOfIsColimit X R x hc)

noncomputable def PresheafOfModules.stalkSheafificationApp (X : TopCat) (R : TopCat.Presheaf RingCat X) (x : ↑X) {c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp R)} (hc : CategoryTheory.Limits.IsColimit c) (hR : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) R) (M : PresheafOfModules R) : (stalkFunctorOfIsColimit X R x hc).obj M ⟶ (sheafStalkFunctor X R x hc hR).obj ((sheafification (CategoryTheory.CategoryStruct.id R)).obj M)

Apply the stalk functor to the unit of module sheafification.

Equations

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

theorem PresheafOfModules.stalkSheafificationApp_isIso (X : TopCat) (R : TopCat.Presheaf RingCat X) (x : ↑X) {c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp R)} (hc : CategoryTheory.Limits.IsColimit c) (hR : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) R) (M : PresheafOfModules R) : CategoryTheory.IsIso (stalkSheafificationApp X R x hc hR M)

The sheafification unit is an isomorphism on every module stalk because its underlying additive stalk map is an isomorphism.

noncomputable def PresheafOfModules.stalkSheafificationIso (X : TopCat) (R : TopCat.Presheaf RingCat X) (x : ↑X) {c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp R)} (hc : CategoryTheory.Limits.IsColimit c) (hR : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) R) : stalkFunctorOfIsColimit X R x hc ≅ (sheafification (CategoryTheory.CategoryStruct.id R)).comp (sheafStalkFunctor X R x hc hR)

Taking module stalks commutes naturally with module sheafification.

Equations

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