The forgetful functor from sheaves of modules to abelian sheaves is exact

SheafOfModules.toSheaf R : SheafOfModules R ⥤ Sheaf J AddCommGrpCat is already known upstream to be Additive and to preserve finite limits. This file supplies the other half — it preserves finite colimits — and the two consequences the cohomology of a scheme needs: it preserves epimorphisms, and it carries a short exact sequence to a short exact sequence.

Why this is needed

Sheaf.H is Ext from the constant sheaf, so the cohomology long exact sequence of a short exact sequence of sheaves of modules is Abelian.Ext.covariantSequence_exact applied to the image of that sequence in Sheaf J AddCommGrpCat. Nothing upstream says the sequence survives the trip. Half of it does — PreservesFiniteLimits gives kernels and monomorphisms — and the missing half is exactly this file.

The argument

Both categories are built the same way, and the proof is to notice that the two constructions agree on the nose. Writing L for PresheafOfModules.sheafification α and G for its right adjoint, Mathlib gives:

• L ⋙ SheafOfModules.toSheaf R = PresheafOfModules.toPresheaf R₀ ⋙ presheafToSheaf J _ — definitionally, not merely up to isomorphism;
• PresheafOfModules.toPresheaf preserves finite colimits, and presheafToSheaf is a left adjoint, so the right-hand side preserves finite colimits;
• the counit of L ⊣ G is an isomorphism.

The last point is what makes this enough. A functor out of the reflective target is determined on colimits by its restriction along L: every diagram d there is isomorphic to (d ⋙ G) ⋙ L, so a colimit of d is the image under L of a colimit computed upstairs, and L ⋙ toSheaf preserving that colimit is the same statement as toSheaf preserving this one. That transport is Adjunction.preservesColimitsOfShape_of_comp_left, imported from the generic limit-preservation root because nothing in it is about sheaves.

Not done here

Exactness is stated as preservation of finite limits and colimits and unpacked only as far as PreservesEpimorphisms and short exactness. No homology or Ext computation happens here; that is the caller's business.

Nothing here is stated for AlgebraicGeometry.Scheme.Modules. That is deliberate — this file is Mathlib-shaped and X.Modules is a def wrapping SheafOfModules X.ringCatSheaf with its own Category instance, so Epi f for f in X.Modules is not syntactically the Epi f these instances discharge and does not transfer by haveI, even though the two are definitionally equal. Working on SheafOfModules X.ringCatSheaf directly avoids it entirely; bridging the wrapper is separate work.

References

• Stacks, Tag 01AG — sheafification is exact

theorem SheafOfModules.preservesFiniteColimits_toSheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Limits.PreservesFiniteColimits (toSheaf R)

SheafOfModules.toSheaf preserves finite colimits.

The α argument is the comparison map from a presheaf of rings whose sheafification is R; it is data of the proof, not of the statement, which is why it is explicit. Take α = 𝟙 R.obj unless there is a reason not to.

instance 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 (toSheaf R)

SheafOfModules.toSheaf preserves finite colimits. Registered at α = 𝟙 R.obj, which is the only case anyone wants; the general statement above is what the proof needs.

instance SheafOfModules.preservesEpimorphisms_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] : (toSheaf R).PreservesEpimorphisms

SheafOfModules.toSheaf preserves epimorphisms: a locally surjective map of sheaves of modules stays locally surjective when the module structure is forgotten. This is the form the cohomology long exact sequence consumes.

theorem 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 (toSheaf R)).ShortExact

A short exact sequence of sheaves of modules is short exact as a sequence of abelian sheaves. Left exactness is upstream (PreservesFiniteLimits); the content is that the epimorphism survives.

theorem SheafOfModules.epi_of_isLocallySurjective {C : Type w} [CategoryTheory.Category.{w, w} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) (h : CategoryTheory.Presheaf.IsLocallySurjective J ((toSheaf R).map f).hom) : CategoryTheory.Epi f

A map of sheaves of modules that is locally surjective is an epimorphism.

preservesEpimorphisms_toSheaf above goes the other way, and only that direction was available: it turns an epimorphism of module sheaves into one of abelian sheaves. What a locality argument produces is the opposite — local surjectivity, hence an epimorphism of abelian sheaves — and to land back in SheafOfModules the functor must reflect epimorphisms.

It does, and for a more elementary reason than preservation of cokernels: toSheaf is faithful, and reflectsEpimorphisms_of_faithful makes every faithful functor reflect epimorphisms. No exactness is involved. Both instances fire on their own; this lemma exists to assemble the chain rather than to supply a missing step, and to record that the chain is complete.

The intended use

Combined with isLocallySurjective_of_coversTop (AlgebraicGeometry/Modules/Tensor/Basic.lean), which builds the hypothesis from local surjectivity on a CoversTop family, this is the step that checks a map of module sheaves is an epimorphism chart by chart — Serre's surjection ⊕ O(-d) ↠ F being the case in view. The two are not combined into one statement here because that would make this file depend on Divisors/, which is a different subject.

instance SheafOfModules.reflectsEpimorphisms_toSheaf {C : Type w} [CategoryTheory.Category.{w, w} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} : (toSheaf R).ReflectsEpimorphisms

toSheaf reflects epimorphisms, recorded as an instance so the chain above is available to instance search as well as to explicit application.