AB axioms in the category of ind-objects #
We show that Ind C satisfies Grothendieck's axiom AB5 if C has finite limits and deduce that
Ind C is Grothendieck abelian if C is small and abelian.
instance CategoryTheory.Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits {C : Type u} [Category.{v, u} C] {J : Type v} [SmallCategory J] [IsFiltered J] [HasFiniteLimits C] :
HasExactColimitsOfShape J (Ind C)
instance CategoryTheory.Limits.instAB5IndOfHasFiniteLimits {C : Type u} [Category.{v, u} C] [HasFiniteLimits C] :
instance CategoryTheory.Limits.isGrothendieckAbelian_ind {C : Type u} [SmallCategory C] [Abelian C] :