Colimits in categories of sheaves of modules #
In this file, we show that colimits of shape J exists in a category
of sheaves of modules if it exists in the corresponding category
of presheaves of modules.
instance
SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesValRingCat
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
[CategoryTheory.HasWeakSheafify J AddCommGrp]
[J.WEqualsLocallyBijective AddCommGrp]
(K : Type w)
[CategoryTheory.Category.{w', w} K]
[CategoryTheory.Limits.HasColimitsOfShape K (PresheafOfModules R.val)]
:
Equations
- ⋯ = ⋯