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}
[CategoryTheory.Category.{v, u} C]
{D : Type w}
[CategoryTheory.Category.{w', w} D]
[CategoryTheory.Abelian D]
{J : CategoryTheory.GrothendieckTopology C}
[CategoryTheory.HasSheafify J D]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.presheafToSheaf_additive
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type w}
[CategoryTheory.Category.{w', w} D]
[CategoryTheory.Abelian D]
{J : CategoryTheory.GrothendieckTopology C}
[CategoryTheory.HasSheafify J D]
:
(CategoryTheory.presheafToSheaf J D).Additive