Commit 2025-01-02 12:06 04bf741e

feat(CategoryTheory/Sites): categories of sheaves are Grothendieck abelian (#19986) If J is a Grothendieck topology on a small category C : Type v, and A : Type u₁ (with Category.{v} A) is a Grothendieck abelian category, then Sheaf J A is a Grothendieck abelian category.