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).

TODO: This file should be moved to CategoryTheory/Sites.

instance CategoryTheory.hasFiniteProductsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.Abelian D] {J : CategoryTheory.GrothendieckTopology C} : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D))

instance CategoryTheory.sheafIsAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.Abelian D] {J : CategoryTheory.GrothendieckTopology C} [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Abelian (CategoryTheory.Sheaf 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.{max v u, w} D] [CategoryTheory.Abelian D] {J : CategoryTheory.GrothendieckTopology C} [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.Functor.Additive (CategoryTheory.presheafToSheaf J D)

Equations

• (_ : CategoryTheory.Functor.Additive (CategoryTheory.presheafToSheaf J D)) = (_ : CategoryTheory.Functor.Additive (CategoryTheory.presheafToSheaf J D))