The category of sheaves of modules is abelian #
In this file, it is shown that the category of sheaves of modules over
a sheaf of rings R is an abelian category. More precisely,
if J is a Grothendieck topology on a category C and R : Sheaf J RingCat.{u},
then SheafOfModules.{v} R is abelian if the conditions HasSheafify J AddCommGrp.{v}]
and J.WEqualsLocallyBijective AddCommGrp.{v} are satisfied.
In particular, if u = v and C : Type u is a small category,
then SheafOfModules.{u} R is abelian: this instance shall be
found automatically if this file and Algebra.Category.Grp.FilteredColimits
are imported.
noncomputable instance
SheafOfModules.instAbelian
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
[CategoryTheory.HasSheafify J AddCommGrp]
[J.WEqualsLocallyBijective AddCommGrp]
:
Equations
- One or more equations did not get rendered due to their size.