Exact colimits of sheaves of modules

Colimits of sheaves of modules of a shape K are exact when colimits of that shape are exact in abelian groups: the sheafification adjunction has a fully faithful right adjoint and a left adjoint preserving finite limits, so exactness descends from presheaves of modules by Mathlib's Adjunction.hasExactColimitsOfShape. In particular sheaves of modules on a ringed site satisfy AB4 and AB5 in the universes where abelian groups do, the input to coproducts in their derived category.

Main results

• SheafOfModules.hasExactColimitsOfShape: the per-shape instance.
• SheafOfModules.ab4OfSize, SheafOfModules.ab5OfSize: the Grothendieck axioms.

instance SheafOfModules.hasExactColimitsOfShape {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (K : Type w) [CategoryTheory.Category.{w', w} K] [CategoryTheory.Limits.HasColimitsOfShape K AddCommGrpCat] [CategoryTheory.HasExactColimitsOfShape K AddCommGrpCat] : CategoryTheory.HasExactColimitsOfShape K (SheafOfModules R)

Colimits of shape K of sheaves of modules are exact when they are in abelian groups, through the sheafification adjunction: its right adjoint is fully faithful and its left adjoint preserves finite limits, which is what Adjunction.hasExactColimitsOfShape needs. HasSheafify (not merely HasWeakSheafify) is required because Mathlib proves PreservesFiniteLimits (sheafification α) and Abelian (SheafOfModules R) only under it.

instance SheafOfModules.hasFilteredColimitsOfSize {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.HasFilteredColimitsOfSize.{w', w, v, v + 1} AddCommGrpCat] : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)

instance SheafOfModules.ab4OfSize {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.HasCoproducts AddCommGrpCat] [CategoryTheory.AB4OfSize.{w, v, v + 1} AddCommGrpCat] : CategoryTheory.AB4OfSize.{w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)

Sheaves of modules satisfy AB4 when abelian groups do.

instance SheafOfModules.ab5OfSize {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.HasFilteredColimitsOfSize.{w', w, v, v + 1} AddCommGrpCat] [CategoryTheory.AB5OfSize.{w', w, v, v + 1} AddCommGrpCat] : CategoryTheory.AB5OfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)

Sheaves of modules satisfy AB5 when abelian groups do.