mathlib3 documentation


Category of sheaves is abelian #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 (Sheaf_is_abelian).

Hence, presheaf_to_Sheaf is an additive functor (presheaf_to_Sheaf_additive).