feat(CategoryTheory/Triangulated): homological functors (#11759)

A functor `F : C ⥤ A` from a pretriangulated category to an abelian category is homological iff it sends distinguished triangles in `C` to exact sequences in `A`. In this PR, we define the corresponding type class `F.IsHomological`. If `F` is a homological functor, we introduce the strictly full triangulated subcategory `F.homologicalKernel`.

Author: joelriou

Mathlib.lean

@@ -1555,6 +1555,7 @@ import Mathlib.CategoryTheory.Sums.Basic
 import Mathlib.CategoryTheory.Thin
 import Mathlib.CategoryTheory.Triangulated.Basic
 import Mathlib.CategoryTheory.Triangulated.Functor
+import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
 import Mathlib.CategoryTheory.Triangulated.Opposite
 import Mathlib.CategoryTheory.Triangulated.Pretriangulated
 import Mathlib.CategoryTheory.Triangulated.Rotate

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

@@ -25,7 +25,7 @@ We provide the following results:
 -/
 
 
-universe v₁ v₂ u₁ u₂
+universe v₁ v₂ v₃ u₁ u₂ u₃
 
 noncomputable section
 
@@ -36,10 +36,11 @@ open CategoryTheory.Limits
 namespace CategoryTheory.Functor
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+    {E : Type u₃} [Category.{v₃} E]
 
 section ZeroMorphisms
 
-variable [HasZeroMorphisms C] [HasZeroMorphisms D]
+variable [HasZeroMorphisms C] [HasZeroMorphisms D] [HasZeroMorphisms E]
 
 /-- A functor preserves zero morphisms if it sends zero morphisms to zero morphisms. -/
 class PreservesZeroMorphisms (F : C ⥤ D) : Prop where
@@ -105,6 +106,15 @@ instance (priority := 100) preservesZeroMorphisms_of_full (F : C ⥤ D) [Full F]
       _ = 0 := by rw [F.map_comp, F.map_preimage, comp_zero]
 #align category_theory.functor.preserves_zero_morphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_full
 
+instance preservesZeroMorphisms_comp (F : C ⥤ D) (G : D ⥤ E)
+    [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] :
+    (F ⋙ G).PreservesZeroMorphisms := ⟨by simp⟩
+
+lemma preservesZeroMorphisms_of_iso {F₁ F₂ : C ⥤ D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) :
+    F₂.PreservesZeroMorphisms where
+  map_zero X Y := by simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality,
+    F₁.map_zero, zero_comp, comp_zero]
+
 instance preservesZeroMorphisms_evaluation_obj (j : D) :
     PreservesZeroMorphisms ((evaluation D C).obj j) where
 

Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

@@ -178,6 +178,13 @@ theorem additive_of_preservesBinaryBiproducts [HasBinaryBiproducts C] [Preserves
       biprod.add_eq_lift_id_desc]
 #align category_theory.functor.additive_of_preserves_binary_biproducts CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
 
+lemma additive_of_preserves_binary_products
+    [HasBinaryProducts C] [PreservesLimitsOfShape (Discrete WalkingPair) F]
+    [F.PreservesZeroMorphisms] : F.Additive := by
+  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
+  have := preservesBinaryBiproductsOfPreservesBinaryProducts F
+  exact Functor.additive_of_preservesBinaryBiproducts F
+
 end
 
 end

Mathlib/CategoryTheory/Triangulated/Functor.lean

@@ -116,6 +116,25 @@ lemma map_distinguished [F.IsTriangulated] (T : Triangle C) (hT : T ∈ distTria
     F.mapTriangle.obj T ∈ distTriang D :=
   IsTriangulated.map_distinguished _ hT
 
+namespace IsTriangulated
+
+open ZeroObject
+
+variable [F.IsTriangulated]
+
+instance (priority := 100) : PreservesZeroMorphisms F where
+  map_zero X Y := by
+    have h₁ : (0 : X ⟶ Y) = 0 ≫ 𝟙 0 ≫ 0 := by simp
+    have h₂ : 𝟙 (F.obj 0) = 0 := by
+      rw [← IsZero.iff_id_eq_zero]
+      apply Triangle.isZero₃_of_isIso₁ _
+        (F.map_distinguished _ (contractible_distinguished (0 : C)))
+      dsimp
+      infer_instance
+    rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
+
+end IsTriangulated
+
 end Functor
 
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.ShortComplex.Exact
+import Mathlib.CategoryTheory.Abelian.Basic
+import Mathlib.CategoryTheory.Shift.ShiftSequence
+import Mathlib.CategoryTheory.Triangulated.Functor
+import Mathlib.CategoryTheory.Triangulated.Subcategory
+
+/-! # Homological functors
+
+In this file, given a functor `F : C ⥤ A` from a pretriangulated category to
+an abelian category, we define the type class `F.IsHomological`, which is the property
+that `F` sends distinguished triangles in `C` to exact sequences in `A`.
+
+If `F` is a homological functor, we define the strictly full triangulated subcategory
+`F.homologicalKernel`.
+
+Note: depending on the sources, homological functors are sometimes
+called cohomological functors, while certain authors use "cohomological functors"
+for "contravariant" functors (i.e. functors `Cᵒᵖ ⥤ A`).
+
+## TODO
+
+* The long exact sequence in homology attached to an homological functor.
+
+## References
+* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996]
+
+-/
+
+namespace CategoryTheory
+
+open Category Limits Pretriangulated ZeroObject Preadditive
+
+variable {C D A : Type*} [Category C] [HasZeroObject C] [HasShift C ℤ] [Preadditive C]
+  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [Pretriangulated C]
+  [Category D] [HasZeroObject D] [HasShift D ℤ] [Preadditive D]
+  [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [Pretriangulated D]
+  [Category A] [Abelian A]
+
+namespace Functor
+
+variable (F : C ⥤ A)
+
+/-- A functor from a pretriangulated category to an abelian category is an homological functor
+if it sends distinguished triangles to exact sequences. -/
+class IsHomological extends F.PreservesZeroMorphisms : Prop where
+  exact (T : Triangle C) (hT : T ∈ distTriang C) :
+    ((shortComplexOfDistTriangle T hT).map F).Exact
+
+lemma map_distinguished_exact [F.IsHomological] (T : Triangle C) (hT : T ∈ distTriang C) :
+    ((shortComplexOfDistTriangle T hT).map F).Exact :=
+  IsHomological.exact _ hT
+
+instance (L : C ⥤ D) (F : D ⥤ A) [L.CommShift ℤ] [L.IsTriangulated] [F.IsHomological] :
+    (L ⋙ F).IsHomological where
+  exact T hT := F.map_distinguished_exact _ (L.map_distinguished T hT)
+
+lemma IsHomological.mk' [F.PreservesZeroMorphisms]
+    (hF : ∀ (T : Pretriangulated.Triangle C) (hT : T ∈ distTriang C),
+      ∃ (T' : Pretriangulated.Triangle C) (e : T ≅ T'),
+      ((shortComplexOfDistTriangle T' (isomorphic_distinguished _ hT _ e.symm)).map F).Exact) :
+    F.IsHomological where
+  exact T hT := by
+    obtain ⟨T', e, h'⟩ := hF T hT
+    exact (ShortComplex.exact_iff_of_iso
+      (F.mapShortComplex.mapIso ((shortComplexOfDistTriangleIsoOfIso e hT)))).2 h'
+
+variable [F.IsHomological]
+
+lemma IsHomological.of_iso {F₁ F₂ : C ⥤ A} [F₁.IsHomological] (e : F₁ ≅ F₂) :
+    F₂.IsHomological :=
+  have := preservesZeroMorphisms_of_iso e
+  ⟨fun T hT => ShortComplex.exact_of_iso (ShortComplex.mapNatIso _ e)
+    (F₁.map_distinguished_exact T hT)⟩
+
+/-- The kernel of a homological functor `F : C ⥤ A` is the strictly full
+triangulated subcategory consisting of objects `X` such that
+for all `n : ℤ`, `F.obj (X⟦n⟧)` is zero. -/
+def homologicalKernel [F.IsHomological] :
+    Triangulated.Subcategory C := Triangulated.Subcategory.mk'
+  (fun X => ∀ (n : ℤ), IsZero (F.obj (X⟦n⟧)))
+  (fun n => by
+    rw [IsZero.iff_id_eq_zero, ← F.map_id, ← Functor.map_id,
+      id_zero, Functor.map_zero, Functor.map_zero])
+  (fun X a hX b => IsZero.of_iso (hX (a + b)) (F.mapIso ((shiftFunctorAdd C a b).app X).symm))
+  (fun T hT h₁ h₃ n => (F.map_distinguished_exact _
+    (Triangle.shift_distinguished T hT n)).isZero_of_both_zeros
+      (IsZero.eq_of_src (h₁ n) _ _) (IsZero.eq_of_tgt (h₃ n) _ _))
+
+instance [F.IsHomological] : ClosedUnderIsomorphisms F.homologicalKernel.P := by
+  dsimp only [homologicalKernel]
+  infer_instance
+
+lemma mem_homologicalKernel_iff [F.IsHomological] [F.ShiftSequence ℤ] (X : C) :
+    F.homologicalKernel.P X ↔ ∀ (n : ℤ), IsZero ((F.shift n).obj X) := by
+  simp only [← fun (n : ℤ) => Iso.isZero_iff ((F.isoShift n).app X)]
+  rfl
+
+noncomputable instance (priority := 100) [F.IsHomological] :
+    PreservesLimitsOfShape (Discrete WalkingPair) F := by
+  suffices ∀ (X₁ X₂ : C), PreservesLimit (pair X₁ X₂) F from
+    ⟨fun {X} => preservesLimitOfIsoDiagram F (diagramIsoPair X).symm⟩
+  intro X₁ X₂
+  have : HasBinaryBiproduct (F.obj X₁) (F.obj X₂) := HasBinaryBiproducts.has_binary_biproduct _ _
+  have : Mono (F.biprodComparison X₁ X₂) := by
+    rw [mono_iff_cancel_zero]
+    intro Z f hf
+    let S := (ShortComplex.mk _ _ (biprod.inl_snd (X := X₁) (Y := X₂))).map F
+    have : Mono S.f := by dsimp [S]; infer_instance
+    have ex : S.Exact := F.map_distinguished_exact _ (binaryBiproductTriangle_distinguished X₁ X₂)
+    obtain ⟨g, rfl⟩ := ex.lift' f (by simpa using hf =≫ biprod.snd)
+    dsimp [S] at hf ⊢
+    replace hf := hf =≫ biprod.fst
+    simp only [assoc, biprodComparison_fst, zero_comp, ← F.map_comp, biprod.inl_fst,
+      F.map_id, comp_id] at hf
+    rw [hf, zero_comp]
+  have : PreservesBinaryBiproduct X₁ X₂ F := preservesBinaryBiproductOfMonoBiprodComparison _
+  apply Limits.preservesBinaryProductOfPreservesBinaryBiproduct
+
+instance (priority := 100) [F.IsHomological] : F.Additive :=
+  F.additive_of_preserves_binary_products
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

@@ -3,8 +3,9 @@ Copyright (c) 2021 Luke Kershaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Kershaw, Joël Riou
 -/
-import Mathlib.CategoryTheory.Triangulated.TriangleShift
+import Mathlib.Algebra.Homology.ShortComplex.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
+import Mathlib.CategoryTheory.Triangulated.TriangleShift
 
 #align_import category_theory.triangulated.pretriangulated from "leanprover-community/mathlib"@"6876fa15e3158ff3e4a4e2af1fb6e1945c6e8803"
 
@@ -158,6 +159,19 @@ theorem comp_distTriang_mor_zero₃₁ (T : Triangle C) (H : T ∈ distTriang C)
   simpa using comp_distTriang_mor_zero₁₂ T.rotate.rotate H₂
 #align category_theory.pretriangulated.comp_dist_triangle_mor_zero₃₁ CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁
 
+/-- The short complex `T.obj₁ ⟶ T.obj₂ ⟶ T.obj₃` attached to a distinguished triangle. -/
+@[simps]
+def shortComplexOfDistTriangle (T : Triangle C) (hT : T ∈ distTriang C) : ShortComplex C :=
+  ShortComplex.mk T.mor₁ T.mor₂ (comp_distTriang_mor_zero₁₂ _ hT)
+
+/-- The isomorphism between the short complex attached to
+two isomorphic distinguished triangles. -/
+@[simps!]
+def shortComplexOfDistTriangleIsoOfIso {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distTriang C) :
+    shortComplexOfDistTriangle T hT ≅ shortComplexOfDistTriangle T'
+      (isomorphic_distinguished _ hT _ e.symm) :=
+  ShortComplex.isoMk (Triangle.π₁.mapIso e) (Triangle.π₂.mapIso e) (Triangle.π₃.mapIso e)
+
 /-- Any morphism `Y ⟶ Z` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` -/
 lemma distinguished_cocone_triangle₁ {Y Z : C} (g : Y ⟶ Z) :
     ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk f g h ∈ distTriang C := by