Commit 2024-12-24 23:17 c93dd21f

feat(CategoryTheory/Sites): categories of sheaves have a separator (#19979) In this file, we show that if J : GrothendieckTopology C and A is a preadditive category which has a separator (and suitable coproducts), then Sheaf J A has a separator. General results about generators are moved to a directory CategoryTheory.Generator. Together with #19914, we shall be able to deduce that categories of abelian sheaves are Grothendieck abelian categories (cf. #19986).