Colimits in categories of sheaves of modules

In this file, we show that colimits of shape J exist in a category of sheaves of modules if it exists in the corresponding category of presheaves of modules.

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

instance SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (PresheafOfModules R.obj)] : CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)