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_reducible]

noncomputable 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] : Abelian (Sheaf 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

instance CategoryTheory.instAdditiveFunctorOppositeConst {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{w', w} D] [Abelian D] : (Functor.const Cᵒᵖ).Additive

instance CategoryTheory.instAdditiveSheafConstantSheaf {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{w', w} D] [Abelian D] {J : GrothendieckTopology C} [HasSheafify J D] : (constantSheaf J D).Additive