[Merged by Bors] - feat: the homological functor on the homotopy category of cochain complexes in an abelian category

Mathlib.lean

@@ -268,6 +268,7 @@ import Mathlib.Algebra.Homology.ExactSequence
 import Mathlib.Algebra.Homology.Functor
 import Mathlib.Algebra.Homology.HomologicalBicomplex
 import Mathlib.Algebra.Homology.HomologicalComplex
+import Mathlib.Algebra.Homology.HomologicalComplexAbelian
 import Mathlib.Algebra.Homology.HomologicalComplexBiprod
 import Mathlib.Algebra.Homology.HomologicalComplexLimits
 import Mathlib.Algebra.Homology.Homology
@@ -277,6 +278,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
 import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
 import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
+import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
 import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
 import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
 import Mathlib.Algebra.Homology.HomotopyCategory.Shift

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -332,6 +332,20 @@ theorem congr_hom {C D : HomologicalComplex V c} {f g : C ⟶ D} (w : f = g) (i
   congr_fun (congr_arg Hom.f w) i
 #align homological_complex.congr_hom HomologicalComplex.congr_hom
 
+lemma mono_of_mono_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
+    (hφ : ∀ i, Mono (φ.f i)) : Mono φ where
+  right_cancellation g h eq := by
+    ext i
+    rw [← cancel_mono (φ.f i)]
+    exact congr_hom eq i
+
+lemma epi_of_epi_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
+    (hφ : ∀ i, Epi (φ.f i)) : Epi φ where
+  left_cancellation g h eq := by
+    ext i
+    rw [← cancel_epi (φ.f i)]
+    exact congr_hom eq i
+
 section
 
 variable (V c)

Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2023 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.Additive
+import Mathlib.Algebra.Homology.HomologicalComplexLimits
+import Mathlib.Algebra.Homology.ShortComplex.ShortExact
+
+/-! # THe category of homological complexes is abelian
+
+If `C` is an abelian category, then `HomologicalComplex C c` is an abelian
+category for any complex shape `c : ComplexShape ι`.
+
+We also obtain that a short complex in `HomologicalComplex C c`
+is exact (resp. short exact) iff degreewise it is so.
+
+-/
+
+open CategoryTheory Category Limits
+
+namespace HomologicalComplex
+
+variable {C ι : Type*} {c : ComplexShape ι} [Category C] [Abelian C]
+
+noncomputable instance : NormalEpiCategory (HomologicalComplex C c) := ⟨fun p _ =>
+  NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
+    (isColimitOfEval _ _ (fun _ =>
+      Abelian.isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi _ _))⟩
+
+noncomputable instance : NormalMonoCategory (HomologicalComplex C c) := ⟨fun p _ =>
+  NormalMono.mk _ (cokernel.π p) (cokernel.condition _)
+    (isLimitOfEval _ _ (fun _ =>
+      Abelian.isLimitMapConeOfKernelForkOfιCokernelConditionOfMono _ _))⟩
+
+noncomputable instance : Abelian (HomologicalComplex C c) where
+
+variable (S : ShortComplex (HomologicalComplex C c))
+
+lemma exact_of_degreewise_exact (hS : ∀ (i : ι), (S.map (eval C c i)).Exact) :
+    S.Exact := by
+  simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
+  rw [IsZero.iff_id_eq_zero]
+  ext i
+  apply (IsZero.of_iso (hS i) (S.mapHomologyIso (eval C c i)).symm).eq_of_src
+
+lemma shortExact_of_degreewise_shortExact
+    (hS : ∀ (i : ι), (S.map (eval C c i)).ShortExact) :
+    S.ShortExact where
+  mono_f := mono_of_mono_f _ (fun i => (hS i).mono_f)
+  epi_g := epi_of_epi_f _ (fun i => (hS i).epi_g)
+  exact := exact_of_degreewise_exact S (fun i => (hS i).exact)
+
+lemma exact_iff_degreewise_exact :
+    S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact := by
+  constructor
+  · intro hS i
+    exact hS.map (eval C c i)
+  · exact exact_of_degreewise_exact S
+
+lemma shortExact_iff_degreewise_shortExact :
+    S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact := by
+  constructor
+  · intro hS i
+    have := hS.mono_f
+    have := hS.epi_g
+    exact hS.map (eval C c i)
+  · exact shortExact_of_degreewise_shortExact S
+
+end HomologicalComplex

Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean

@@ -0,0 +1,37 @@
+/-
+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.HomologicalComplexAbelian
+import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
+import Mathlib.Algebra.Homology.HomologySequence
+import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
+
+/-! The homological functor
+
+In this file, it is shown that if `C` is an abelian category,
+then `homologyFunctor C (ComplexShape.up ℤ) n` is a homological functor
+`HomotopyCategory C (ComplexShape.up ℤ) ⥤ C`. As distinguished triangles
+in the homotopy category can be characterized in terms of degreewise split
+short exact sequences of cochain complexes, this follows from the homology
+sequence of a short exact sequences of homological complexes.
+
+-/
+
+open CategoryTheory
+
+variable {C : Type*} [Category C] [Abelian C]
+
+namespace HomotopyCategory
+
+instance (n : ℤ) : (homologyFunctor C (ComplexShape.up ℤ) n).IsHomological :=
+  Functor.IsHomological.mk' _ (fun T hT => by
+    rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT
+    obtain ⟨S, σ, ⟨e⟩⟩ := hT
+    have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S
+      (fun n => (σ n).shortExact)
+    exact ⟨_, e, (ShortComplex.exact_iff_of_iso
+      (S.mapNatIso (homologyFunctorFactors C (ComplexShape.up ℤ) n))).2 (hS.homology_exact₂ n)⟩)
+
+end HomotopyCategory

Mathlib/CategoryTheory/Abelian/Basic.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel, Johan Commelin, Scott Morrison
 -/
 import Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
 import Mathlib.CategoryTheory.Preadditive.Biproducts
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.Images
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 import Mathlib.CategoryTheory.Abelian.NonPreadditive
@@ -498,6 +499,44 @@ theorem monoLift_comp [Mono f] {T : C} (g : T ⟶ Y) (hg : g ≫ cokernel.π f =
     WalkingParallelPair.zero
 #align category_theory.abelian.mono_lift_comp CategoryTheory.Abelian.monoLift_comp
 
+section
+
+variable {D : Type*} [Category D] [HasZeroMorphisms D]
+
+/-- If `F : D ⥤ C` is a functor to an abelian category, `i : X ⟶ Y` is a morphism
+admitting a cokernel such that `F` preserves this cokernel and `F.map i` is a mono,
+then `F.map X` identifies to the kernel of `F.map (cokernel.π i)`. -/
+noncomputable def isLimitMapConeOfKernelForkOfιCokernelConditionOfMono
+    {X Y : D} (i : X ⟶ Y) [HasCokernel i] (F : D ⥤ C)
+    [F.PreservesZeroMorphisms] [Mono (F.map i)]
+    [PreservesColimit (parallelPair i 0) F] :
+    IsLimit (F.mapCone (KernelFork.ofι i (cokernel.condition i))) := by
+  let e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
+    parallelPair.ext (Iso.refl _) (asIso (cokernelComparison i F)) (by simp) (by simp)
+  refine' IsLimit.postcomposeInvEquiv e _ _
+  let hi := Abelian.monoIsKernelOfCokernel _ (cokernelIsCokernel (F.map i))
+  refine' IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) _)
+  change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
+  rw [Category.comp_id, Category.id_comp]
+
+/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphisms
+admitting a kernel such that `F` preserves this kernel and `F.map p` is an epi,
+then `F.map Y` identifies to the cokernel of `F.map (kernel.ι p)`. -/
+noncomputable def isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi
+    {X Y : D} (p : X ⟶ Y) [HasKernel p] (F : D ⥤ C)
+    [F.PreservesZeroMorphisms] [Epi (F.map p)]
+    [PreservesLimit (parallelPair p 0) F] :
+    IsColimit (F.mapCocone (CokernelCofork.ofπ p (kernel.condition p))) := by
+  let e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
+    parallelPair.ext (asIso (kernelComparison p F)) (Iso.refl _) (by simp) (by simp)
+  refine' IsColimit.precomposeInvEquiv e _ _
+  let hp := Abelian.epiIsCokernelOfKernel _ (kernelIsKernel (F.map p))
+  refine' IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) _)
+  change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p
+  rw [Category.comp_id, Category.id_comp]
+
+end
+
 end CokernelOfKernel
 
 section