feat(CategoryTheory): the category of ind-objects is Grothendieck abe…

…lian (#21606)

- If `C` is small and additive, then `Ind C` is preadditive (which implies that it is additive using existing results)
- If `C` is small and abelian, then `Ind C` is Grothendieck abelian



Co-authored-by: Markus Himmel <[email protected]>

Mathlib.lean

@@ -1712,6 +1712,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Oppos
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
 import Mathlib.CategoryTheory.Abelian.Images
+import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Abelian.Injective.Basic
 import Mathlib.CategoryTheory.Abelian.Injective.Resolution
 import Mathlib.CategoryTheory.Abelian.LeftDerived
@@ -2222,6 +2223,7 @@ import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
 import Mathlib.CategoryTheory.Preadditive.EndoFunctor
 import Mathlib.CategoryTheory.Preadditive.FunctorCategory
 import Mathlib.CategoryTheory.Preadditive.HomOrthogonal
+import Mathlib.CategoryTheory.Preadditive.Indization
 import Mathlib.CategoryTheory.Preadditive.Injective.Basic
 import Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
 import Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean

@@ -5,18 +5,24 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
+import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Generator.Indization
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 
 /-!
 # AB axioms in the category of ind-objects
 
-We show that `Ind C` satisfies Grothendieck's axiom AB5 if `C` has finite limits.
+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.
 -/
 
 universe v u
 
 namespace CategoryTheory.Limits
 
+section
+
 variable {C : Type u} [Category.{v} C]
 
 instance {J : Type v} [SmallCategory J] [IsFiltered J] [HasFiniteLimits C] :
@@ -26,4 +32,15 @@ instance {J : Type v} [SmallCategory J] [IsFiltered J] [HasFiniteLimits C] :
 instance [HasFiniteLimits C] : AB5 (Ind C) where
   ofShape _ _ _ := inferInstance
 
+end
+
+section
+
+variable {C : Type u} [SmallCategory C] [Abelian C]
+
+instance isGrothendieckAbelian_ind : IsGrothendieckAbelian.{u} (Ind C) where
+  hasSeparator := ⟨⟨_, Ind.isSeparator_range_yoneda⟩⟩
+
+end
+
 end CategoryTheory.Limits

Mathlib/CategoryTheory/Abelian/Indization.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Preadditive.Indization
+import Mathlib.CategoryTheory.Abelian.FunctorCategory
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
+
+/-!
+# 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 `CategoryTheory.Abelian.GrothendieckAxioms.Indization`, we show that in this situation
+`Ind C` is in fact Grothendieck abelian.
+-/
+
+universe v
+
+open CategoryTheory.Abelian
+
+namespace CategoryTheory
+
+variable {C : Type v} [SmallCategory C] [Abelian C]
+
+instance {X Y : Ind C} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f) := by
+  obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)
+  let i' := coimageImageComparisonFunctor.mapIso i
+  dsimp only [coimageImageComparisonFunctor_obj, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom] at i'
+  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom,
+    Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
+  infer_instance
+
+noncomputable instance : Abelian (Ind C) :=
+  .ofCoimageImageComparisonIsIso
+
+end CategoryTheory

Mathlib/CategoryTheory/Generator/Indization.lean

@@ -5,16 +5,13 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Generator.Basic
 import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Preadditive.Indization
 
 /-!
 # Separating set in the category of ind-objects
 
-We construct a separating set in the category of ind-objects.
-
-## Future work
-
-Once we have constructed zero morphisms in the category of ind-objects, we will be able to show
-that under sufficient conditions, the category of ind-objects has a separating object.
+We construct a separating set in the category of ind-objects and conclude that if `C` is small
+and additive, then `Ind C` has a separator.
 
 -/
 
@@ -34,4 +31,13 @@ theorem Ind.isSeparating_range_yoneda : IsSeparating (Set.range (Ind.yoneda : C
 
 end
 
+section
+
+variable {C : Type u} [SmallCategory C] [Preadditive C] [HasFiniteColimits C]
+
+theorem Ind.isSeparator_range_yoneda : IsSeparator (∐ (Ind.yoneda : C ⥤ _).obj) :=
+  Ind.isSeparating_range_yoneda.isSeparator_coproduct
+
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/Preadditive/Indization.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Preadditive.Transfer
+import Mathlib.CategoryTheory.Preadditive.Opposite
+import Mathlib.Algebra.Category.Grp.LeftExactFunctor
+
+/-!
+# The category of ind-objects is preadditive
+-/
+
+universe v u
+
+open CategoryTheory Limits
+
+namespace CategoryTheory
+
+variable {C : Type u} [SmallCategory C] [Preadditive C] [HasFiniteColimits C]
+
+attribute [local instance] HasFiniteBiproducts.of_hasFiniteCoproducts in
+noncomputable instance : Preadditive (Ind C) :=
+  .ofFullyFaithful (((Ind.leftExactFunctorEquivalence C).trans
+    (AddCommGrp.leftExactFunctorForgetEquivalence _).symm).fullyFaithfulFunctor.comp
+      (fullyFaithfulFullSubcategoryInclusion _))
+
+instance : HasFiniteBiproducts (Ind C) :=
+  HasFiniteBiproducts.of_hasFiniteCoproducts
+
+end CategoryTheory