Category of sheaves is abelian #
Let C, D be categories and J be a grothendieck topology on C, when D is abelian and
sheafification is possible in C, Sheaf J D is abelian as well (sheafIsAbelian).
Hence, presheafToSheaf is an additive functor (presheafToSheaf_additive).
instance
CategoryTheory.sheafIsAbelian
{C : Type u}
[Category.{v, u} C]
{D : Type w}
[Category.{w', w} D]
[Abelian D]
{J : GrothendieckTopology C}
[HasSheafify J D]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.presheafToSheaf_additive
{C : Type u}
[Category.{v, u} C]
{D : Type w}
[Category.{w', w} D]
[Abelian D]
{J : GrothendieckTopology C}
[HasSheafify J D]
:
(presheafToSheaf J D).Additive