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]
: