Documentation

Mathlib.Topology.Sheaves.Abelian

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.