The category of ind-objects is abelian

We show that if C is a small abelian category, then Ind C is an abelian category.

In the file Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean, we show that in this situation Ind C is in fact Grothendieck abelian.

instance CategoryTheory.instIsIsoIndCoimageImageComparison {C : Type v} [SmallCategory C] [Abelian C] {X Y : Ind C} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f)

noncomputable instance CategoryTheory.instAbelianInd {C : Type v} [SmallCategory C] [Abelian C] : Abelian (Ind C)

Equations

• CategoryTheory.instAbelianInd = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso