feat(Algebra/Homology): the homology functor is accessible

Mathlib.lean

@@ -696,6 +696,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 public import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
 public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
 public import Mathlib.Algebra.Homology.ShortComplex.Homology
+public import Mathlib.Algebra.Homology.ShortComplex.HomologyCofork
 public import Mathlib.Algebra.Homology.ShortComplex.LeftHomology
 public import Mathlib.Algebra.Homology.ShortComplex.Limits
 public import Mathlib.Algebra.Homology.ShortComplex.Linear
@@ -2548,6 +2549,7 @@ public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
+public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HomologyFunctorAccessible
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
 public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Homology.Additive
 public import Mathlib.Algebra.Homology.ShortComplex.Exact
 public import Mathlib.Algebra.Homology.ShortComplex.Preadditive
+public import Mathlib.Algebra.Homology.HomologicalComplexLimits
 public import Mathlib.Tactic.NormNum
 
 /-!
@@ -28,6 +29,8 @@ abbreviated as `K.sc i`.
 
 open CategoryTheory Category Limits
 
+universe w₁ w₂
+
 namespace HomologicalComplex
 
 variable (C : Type*) [Category* C] [HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι)
@@ -42,12 +45,44 @@ def shortComplexFunctor' (i j k : ι) : HomologicalComplex C c ⥤ ShortComplex
       τ₂ := f.f j
       τ₃ := f.f k }
 
+instance (J : Type*) [Category* J] [HasColimitsOfShape J C] (i j k : ι) :
+    PreservesColimitsOfShape J (shortComplexFunctor' C c i j k) where
+  preservesColimit {F} := ⟨fun h ↦ ⟨by
+    apply ShortComplex.isColimitOfIsColimitπ
+    all_goals exact isColimitOfPreserves (HomologicalComplex.eval C _ _) h⟩⟩
+
+instance (J : Type*) [Category* J] [HasLimitsOfShape J C] (i j k : ι) :
+    PreservesLimitsOfShape J (shortComplexFunctor' C c i j k) where
+  preservesLimit {F} := ⟨fun h ↦ ⟨by
+    apply ShortComplex.isLimitOfIsLimitπ
+    all_goals exact isLimitOfPreserves (HomologicalComplex.eval C _ _) h⟩⟩
+
+instance [HasColimitsOfSize.{w₁, w₂} C] (i j k : ι) :
+    PreservesColimitsOfSize.{w₁, w₂} (shortComplexFunctor' C c i j k) where
+
+instance [HasLimitsOfSize.{w₁, w₂} C] (i j k : ι) :
+    PreservesLimitsOfSize.{w₁, w₂} (shortComplexFunctor' C c i j k) where
+
 /-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
 complex `K` to the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`. -/
 @[simps!]
 noncomputable def shortComplexFunctor (i : ι) :=
   shortComplexFunctor' C c (c.prev i) i (c.next i)
 
+instance (J : Type*) [Category* J] [HasColimitsOfShape J C] (i : ι) :
+    PreservesColimitsOfShape J (shortComplexFunctor C c i) :=
+  inferInstanceAs (PreservesColimitsOfShape J (shortComplexFunctor' C c _ i _))
+
+instance (J : Type*) [Category* J] [HasLimitsOfShape J C] (i : ι) :
+    PreservesLimitsOfShape J (shortComplexFunctor C c i) :=
+  inferInstanceAs (PreservesLimitsOfShape J (shortComplexFunctor' C c _ i _))
+
+instance [HasColimitsOfSize.{w₁, w₂} C] (i : ι) :
+    PreservesColimitsOfSize.{w₁, w₂} (shortComplexFunctor C c i) where
+
+instance [HasLimitsOfSize.{w₁, w₂} C] (i : ι) :
+    PreservesLimitsOfSize.{w₁, w₂} (shortComplexFunctor C c i) where
+
 set_option backward.isDefEq.respectTransparency.types false in
 set_option backward.defeqAttrib.useBackward true in
 /-- The natural isomorphism `shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k`

Mathlib/Algebra/Homology/ShortComplex/Homology.lean

@@ -821,6 +821,12 @@ attribute [instance] CategoryWithHomology.hasHomology
 instance [CategoryWithHomology C] : CategoryWithHomology Cᵒᵖ :=
   ⟨fun S => HasHomology.mk' S.unop.homologyData.op⟩
 
+instance (priority := low) [CategoryWithHomology C] : HasKernels C where
+  has_limit {X Y} f := ⟨_, (ShortComplex.mk (0 : X ⟶ X) f).cyclesIsKernel⟩
+
+instance (priority := low) [CategoryWithHomology C] : HasCokernels C where
+  has_colimit {X Y} f := ⟨_, (ShortComplex.mk f (0 : Y ⟶ Y)).opcyclesIsCokernel⟩
+
 /-- The homology functor `ShortComplex C ⥤ C` for a category `C` with homology. -/
 @[simps]
 noncomputable def homologyFunctor [CategoryWithHomology C] :
@@ -953,6 +959,24 @@ lemma homologyι_naturality (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHom
     rightHomologyIso_hom_comp_homologyι, rightHomologyι_naturality]
   simp only [homologyι, assoc, Iso.hom_inv_id_assoc]
 
+variable (C) in
+/-- The morphism `S.homologyπ : S.cycles ⟶ S.homology` for any `S : Shortcomplex C`,
+as a natural transformation`. -/
+@[simps]
+noncomputable def homologyπNatTrans [CategoryWithHomology C] :
+    cyclesFunctor C ⟶ homologyFunctor C where
+  app S := S.homologyπ
+  naturality _ _ f := (homologyπ_naturality f).symm
+
+variable (C) in
+/-- The morphism `S.homologyπ : S.cycles ⟶ S.homology` for any `S : Shortcomplex C`,
+as a natural transformation`. -/
+@[simps]
+noncomputable def homologyιNatTrans [CategoryWithHomology C] :
+    homologyFunctor C ⟶ opcyclesFunctor C where
+  app S := S.homologyι
+  naturality _ _ f := homologyι_naturality f
+
 @[reassoc (attr := simp)]
 lemma homology_π_ι :
     S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles := by

Mathlib/Algebra/Homology/ShortComplex/HomologyCofork.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ShortComplex.Homology
+public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
+public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
+
+/-!
+# The homology functor as a cokernel and as a kernel
+
+In this file, we show that in the category of functors `ShortComplex C ⥤ C`,
+- the functor `cyclesFunctor C` is the kernel of `π₂ ⟶ π₃`;
+- the functor `opcyclesFunctor C` is the cokernel of `π₁ ⟶ π₂`;
+- the functor `homologyFunctor C` is the cokernel of `π₁ ⟶ cyclesFunctor C`;
+- the functor `homologyFunctor C` is the kernel of `opcyclesFunctor C ⟶ π₃`.
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Limits
+
+variable (C : Type*) [Category* C]
+
+namespace ShortComplex
+
+section
+
+variable [HasZeroMorphisms C] [HasKernels C] [HasCokernels C]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The limit kernel fork expressing `cyclesFunctor C : ShortComplex C ⥤ C`
+as the kernel of `π₂Toπ₃ : π₂ ⟶ π₃`. -/
+@[implicit_reducible]
+noncomputable def cyclesFunctorFork :
+    KernelFork (ShortComplex.π₂Toπ₃ (C := C)) :=
+  KernelFork.ofι (iCyclesNatTrans C) (by cat_disch)
+
+/-- The functor `cyclesFunctor C : ShortComplex C ⥤ C` is the kernel of `π₂Toπ₃ : π₂ ⟶ π₃`. -/
+@[no_expose]
+noncomputable def isLimitCyclesFunctorFork :
+    IsLimit (cyclesFunctorFork C) :=
+  evaluationJointlyReflectsLimits _
+    (fun S ↦ (KernelFork.isLimitMapConeEquiv _ _).2 S.cyclesIsKernel)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The colimit cokernel cofork expressing `opcyclesFunctor C : ShortComplex C ⥤ C`
+as the cokernel of `π₁Toπ₂ : π₁ ⟶ π₂`. -/
+@[implicit_reducible]
+noncomputable def opcyclesFunctorCofork :
+    CokernelCofork (ShortComplex.π₁Toπ₂ (C := C)) :=
+  CokernelCofork.ofπ (pOpcyclesNatTrans C) (by cat_disch)
+
+/-- The functor `opcyclesFunctor C : ShortComplex C ⥤ C` is the cokernel of `π₁Toπ₂ : π₁ ⟶ π₂`. -/
+@[no_expose]
+noncomputable def isColimitOpcyclesFunctorCofork :
+    IsColimit (opcyclesFunctorCofork C) :=
+  evaluationJointlyReflectsColimits _
+    (fun S ↦ (CokernelCofork.isColimitMapCoconeEquiv _ _).2 S.opcyclesIsCokernel)
+
+end
+
+section
+
+variable [HasZeroMorphisms C] [CategoryWithHomology C]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The colimit cokernel cofork expressing `homologyFunctor C : ShortComplex C ⥤ C`
+as the cokernel of `toCyclesNatTrans C : π₁ ⟶ cyclesFunctor C`. -/
+@[implicit_reducible]
+noncomputable def homologyFunctorCofork : CokernelCofork (toCyclesNatTrans C) :=
+  CokernelCofork.ofπ (homologyπNatTrans C) (by cat_disch)
+
+/-- The functor `homologyFunctor C : ShortComplex C ⥤ C` is
+the cokernel of `toCyclesNatTrans C : π₁ ⟶ cyclesFunctor C`. -/
+@[no_expose]
+noncomputable def isColimitHomologyFunctorCofork :
+    IsColimit (homologyFunctorCofork C) :=
+  evaluationJointlyReflectsColimits _
+    (fun S ↦ (CokernelCofork.isColimitMapCoconeEquiv _ _).2 S.homologyIsCokernel)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The limit kernel fork expressing `homologyFunctor C : ShortComplex C ⥤ C`
+as the kernel of `fromOpcyclesNatTrans C : opcyclesFunctor C ⟶ π₃`. -/
+@[implicit_reducible]
+noncomputable def homologyFunctorFork : KernelFork (fromOpcyclesNatTrans C) :=
+  KernelFork.ofι (homologyιNatTrans C) (by cat_disch)
+
+/-- The functor `homologyFunctor C : ShortComplex C ⥤ C` is
+the kernel of `fromOpcyclesNatTrans C : opcyclesFunctor C ⟶ π₃`. -/
+@[no_expose]
+noncomputable def isLimitHomologyFunctorFork :
+    IsLimit (homologyFunctorFork C) :=
+  evaluationJointlyReflectsLimits _
+    (fun S ↦ (KernelFork.isLimitMapConeEquiv _ _).2 S.homologyIsKernel)
+
+end
+
+end ShortComplex
+
+end CategoryTheory

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/HomologyFunctorAccessible.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+public import Mathlib.Algebra.Homology.ShortComplex.HomologyCofork
+public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
+public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
+public import Mathlib.CategoryTheory.Presentable.Basic
+
+/-!
+# The homology functor on a Grothendieck abelian category is accessible
+
+In this file, we show that if `C` is a Grothendieck abelian category,
+then the homology functors `ShortComplex C ⥤ C` and `HomologicalComplex C c ⥤ C`
+are ℵ₀-accessible (i.e. preserve filtered colimits).
+
+-/
+
+public section
+
+universe w
+
+attribute [local instance] Cardinal.fact_isRegular_aleph0
+
+open CategoryTheory Limits
+
+variable {C : Type*} [Category* C] [Abelian C]
+
+namespace CategoryTheory.ShortComplex
+
+section
+
+variable {J : Type*} [Category* J]
+  [HasColimitsOfShape J C] [HasExactColimitsOfShape J C]
+
+open ObjectProperty
+
+instance : PreservesColimitsOfShape J (ShortComplex.cyclesFunctor C) :=
+  (preservesColimitsOfShape J).prop_of_isLimit
+    (ShortComplex.isLimitCyclesFunctorFork C) (by
+      rintro (_ | _)
+      all_goals
+        dsimp
+        infer_instance)
+
+instance : PreservesColimitsOfShape J (ShortComplex.opcyclesFunctor C) :=
+  (preservesColimitsOfShape J).prop_of_isColimit
+    (ShortComplex.isColimitOpcyclesFunctorCofork C) (by
+      rintro (_ | _)
+      all_goals
+        dsimp
+        infer_instance)
+
+instance : PreservesColimitsOfShape J (ShortComplex.homologyFunctor C) :=
+  (preservesColimitsOfShape J).prop_of_isColimit
+    (ShortComplex.isColimitHomologyFunctorCofork C) (by
+      rintro (_ | _)
+      all_goals
+        dsimp
+        infer_instance)
+
+end
+
+section
+
+variable [IsGrothendieckAbelian.{w} C]
+
+instance : Functor.IsCardinalAccessible.{w} (ShortComplex.cyclesFunctor C) .aleph0 where
+  preservesColimitOfShape J _ _ := by
+    have : IsFiltered J := isFiltered_of_isCardinalFiltered J Cardinal.aleph0
+    infer_instance
+
+instance : Functor.IsCardinalAccessible.{w} (ShortComplex.opcyclesFunctor C) .aleph0 where
+  preservesColimitOfShape J _ _ := by
+    have : IsFiltered J := isFiltered_of_isCardinalFiltered J Cardinal.aleph0
+    infer_instance
+
+instance : Functor.IsCardinalAccessible.{w} (ShortComplex.homologyFunctor C) .aleph0 where
+  preservesColimitOfShape J _ _ := by
+    have : IsFiltered J := isFiltered_of_isCardinalFiltered J Cardinal.aleph0
+    infer_instance
+
+end
+
+end CategoryTheory.ShortComplex
+
+namespace HomologicalComplex
+
+variable [IsGrothendieckAbelian.{w} C] {ι : Type*} {c : ComplexShape ι} (i : ι)
+
+instance : Functor.IsCardinalAccessible.{w} (cyclesFunctor C c i) .aleph0 :=
+  inferInstanceAs (Functor.IsCardinalAccessible (shortComplexFunctor C c i ⋙
+    ShortComplex.cyclesFunctor C) _)
+
+instance : Functor.IsCardinalAccessible.{w} (opcyclesFunctor C c i) .aleph0 :=
+  inferInstanceAs (Functor.IsCardinalAccessible (shortComplexFunctor C c i ⋙
+    ShortComplex.opcyclesFunctor C) _)
+
+instance : Functor.IsCardinalAccessible.{w} (homologyFunctor C c i) .aleph0 :=
+  inferInstanceAs (Functor.IsCardinalAccessible (shortComplexFunctor C c i ⋙
+    ShortComplex.homologyFunctor C) _)
+
+end HomologicalComplex