Forgetting the module structure of a sheaf of modules is exact

Let R be a sheaf of rings on a site (C, J). Mathlib's SheafOfModules.toSheaf R sends a sheaf of R-modules to its underlying abelian sheaf, and knows that this functor preserves and reflects finite limits. This file supplies the missing half: it preserves finite colimits as well, hence carries short exact sequences of sheaves of modules to short exact sequences of abelian sheaves.

Main declarations

• TauCeti.SheafOfModules.preservesFiniteColimits_toSheaf: SheafOfModules.toSheaf preserves finite colimits;
• TauCeti.SheafOfModules.shortExact_map_toSheaf: a short exact sequence of sheaves of modules stays short exact after forgetting the module structures.

The proof is a transfer along the sheafification of presheaves of modules. That functor is a left adjoint whose counit is an isomorphism, and composing it with SheafOfModules.toSheaf gives PresheafOfModules.toPresheaf ⋙ presheafToSheaf, which preserves finite colimits because colimits of presheaves of modules are computed sectionwise and presheafToSheaf is a left adjoint.

Exactness of SheafOfModules.toSheaf is what makes the cohomology of a sheaf of modules, which is defined through the underlying abelian sheaf, fit into a long exact sequence; see TauCeti/AlgebraicGeometry/Cohomology/LongExactSequence.lean. It is therefore Layer B infrastructure for TauCetiRoadmap/JacobianChallenge/README.md. No formalization is vendored: the ingredients are Mathlib's PresheafOfModules.sheafificationAdjunction, PresheafOfModules.sheafificationCompToSheaf and ShortComplex.ShortExact.map_of_exact.

instance TauCeti.SheafOfModules.preservesFiniteColimits_toSheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Limits.PreservesFiniteColimits (SheafOfModules.toSheaf R)

theorem TauCeti.SheafOfModules.shortExact_map_toSheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) : (S.map (SheafOfModules.toSheaf R)).ShortExact

Forgetting the module structures of a short exact sequence of sheaves of modules leaves a short exact sequence of abelian sheaves.