Exact colimits of presheaves of modules

Colimits of presheaves of modules of a shape K are exact when colimits of that shape are exact in abelian groups. The forgetful functor to presheaves of abelian groups preserves colimits and finite limits, and it reflects finite limits: being faithful it reflects monomorphisms and epimorphisms, so out of the balanced category of presheaves of modules it reflects isomorphisms, and a finite-limit-preserving functor that reflects isomorphisms reflects finite limits. Exactness therefore pulls back along it from the functor category, where colimits are exact objectwise (HasExactColimitsOfShape.domain_of_functor). In particular presheaves of modules satisfy AB4 and AB5 in the universes where abelian groups do.

Main results

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

instance PresheafOfModules.hasExactColimitsOfShape {C : Type u'} [CategoryTheory.Category.{v', u'} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (K : Type w) [CategoryTheory.Category.{w', w} K] [CategoryTheory.Limits.HasColimitsOfShape K AddCommGrpCat] [CategoryTheory.HasExactColimitsOfShape K AddCommGrpCat] : CategoryTheory.HasExactColimitsOfShape K (PresheafOfModules R)

Colimits of shape K of presheaves of modules are exact when they are in abelian groups, pulled back along the forgetful functor to presheaves of abelian groups.

instance PresheafOfModules.hasFilteredColimitsOfSize {C : Type u'} [CategoryTheory.Category.{v', u'} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [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'} (PresheafOfModules R)

instance PresheafOfModules.ab4OfSize {C : Type u'} [CategoryTheory.Category.{v', u'} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [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'} (PresheafOfModules R)

Presheaves of modules satisfy AB4 when abelian groups do.

instance PresheafOfModules.ab5OfSize {C : Type u'} [CategoryTheory.Category.{v', u'} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) [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'} (PresheafOfModules R)

Presheaves of modules satisfy AB5 when abelian groups do.