AB axioms in sheaf categories

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.

instance CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf {C : Type u} {A : Type u₁} {K : Type u₂} [Category.{v, u} C] [Category.{v₁, u₁} A] [Category.{v₂, u₂} K] (J : GrothendieckTopology C) [HasWeakSheafify J A] [Limits.HasFiniteLimits A] [Limits.HasColimitsOfShape K A] [HasExactColimitsOfShape K A] [Limits.PreservesColimitsOfShape K (sheafToPresheaf J A)] : HasExactColimitsOfShape K (Sheaf J A)

instance CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf {C : Type u} {A : Type u₁} {K : Type u₂} [Category.{v, u} C] [Category.{v₁, u₁} A] [Category.{v₂, u₂} K] (J : GrothendieckTopology C) [HasWeakSheafify J A] [Limits.HasFiniteColimits A] [Limits.HasLimitsOfShape K A] [HasExactLimitsOfShape K A] [Limits.PreservesFiniteColimits (sheafToPresheaf J A)] : HasExactLimitsOfShape K (Sheaf J A)

instance CategoryTheory.Sheaf.hasFilteredColimitsOfSize {C : Type u} {A : Type u₁} [Category.{v, u} C] [Category.{v₁, u₁} A] (J : GrothendieckTopology C) [HasSheafify J A] [Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A] : Limits.HasFilteredColimitsOfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (Sheaf J A)

instance CategoryTheory.Sheaf.hasExactColimitsOfShape {C : Type u} {A : Type u₁} {K : Type u₂} [Category.{v, u} C] [Category.{v₁, u₁} A] [Category.{v₂, u₂} K] (J : GrothendieckTopology C) [Limits.HasFiniteLimits A] [HasSheafify J A] [Limits.HasColimitsOfShape K A] [HasExactColimitsOfShape K A] : HasExactColimitsOfShape K (Sheaf J A)

instance CategoryTheory.Sheaf.ab5ofSize {C : Type u} {A : Type u₁} [Category.{v, u} C] [Category.{v₁, u₁} A] (J : GrothendieckTopology C) [Limits.HasFiniteLimits A] [HasSheafify J A] [Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A] [AB5OfSize.{v₂, u₂, v₁, u₁} A] : AB5OfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (Sheaf J A)

instance CategoryTheory.Sheaf.instIsGrothendieckAbelian {C : Type v} [SmallCategory C] (J : GrothendieckTopology C) (A : Type u₁) [Category.{v₁, u₁} A] [Abelian A] [IsGrothendieckAbelian.{v, v₁, u₁} A] [HasSheafify J A] : IsGrothendieckAbelian.{v, max v v₁, max (max (max u₁ v) v₁) v} (Sheaf J A)

theorem CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall {C : Type u₂} [Category.{v₂, u₂} C] [EssentiallySmall.{v, v₂, u₂} C] (J : GrothendieckTopology C) (A : Type u₁) [Category.{v₁, u₁} A] [Abelian A] [IsGrothendieckAbelian.{v, v₁, u₁} A] [∀ (X : Cᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X (equivSmallModel C).inverse.op) A] [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] : IsGrothendieckAbelian.{v, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂} (Sheaf J A)