feat(Algebra/Homology) the single complex functor preserves (co)limits (

#13875)

In this PR, it is shown that the single functors `C ⥤ HomologicalComplex C c` preserves limits and colimits.



Co-authored-by: Joël Riou <[email protected]>

Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

@@ -3,7 +3,7 @@ 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.HomologicalComplex
+import Mathlib.Algebra.Homology.Single
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
 
@@ -193,4 +193,28 @@ def preservesColimitsOfShapeOfEval {D : Type*} [Category D]
   ⟨fun {_} => ⟨fun hs ↦ isColimitOfEval _ _
     (fun i => isColimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩
 
+section
+
+variable [HasZeroObject C] [DecidableEq ι] (i : ι)
+
+noncomputable instance : PreservesLimitsOfShape J (single C c i) :=
+  preservesLimitsOfShapeOfEval _ (fun j => by
+    by_cases h : j = i
+    · subst h
+      exact preservesLimitsOfShapeOfNatIso (singleCompEvalIsoSelf C c j).symm
+    · exact Functor.preservesLimitsOfShapeOfIsZero _ (isZero_single_comp_eval C c _ _ h) _)
+
+noncomputable instance : PreservesColimitsOfShape J (single C c i) :=
+  preservesColimitsOfShapeOfEval _ (fun j => by
+    by_cases h : j = i
+    · subst h
+      exact preservesColimitsOfShapeOfNatIso (singleCompEvalIsoSelf C c j).symm
+    · exact Functor.preservesColimitsOfShapeOfIsZero _ (isZero_single_comp_eval C c _ _ h) _)
+
+noncomputable instance : PreservesFiniteLimits (single C c i) := ⟨by intros; infer_instance⟩
+
+noncomputable instance : PreservesFiniteColimits (single C c i) := ⟨by intros; infer_instance⟩
+
+end
+
 end HomologicalComplex

Mathlib/Algebra/Homology/Single.lean

@@ -96,6 +96,18 @@ theorem single_map_f_self (j : ι) {A B : V} (f : A ⟶ B) :
   rfl
 #align homological_complex.single_map_f_self HomologicalComplex.single_map_f_self
 
+variable (V)
+
+/-- The natural isomorphism `single V c j ⋙ eval V c j ≅ 𝟭 V`. -/
+@[simps!]
+noncomputable def singleCompEvalIsoSelf (j : ι) : single V c j ⋙ eval V c j ≅ 𝟭 V :=
+  NatIso.ofComponents (singleObjXSelf c j) (fun {A B} f => by simp [single_map_f_self])
+
+lemma isZero_single_comp_eval (j i : ι) (hi : i ≠ j) : IsZero (single V c j ⋙ eval V c i) :=
+  Functor.isZero _ (fun _ ↦ isZero_single_obj_X c _ _ _ hi)
+
+variable {V c}
+
 @[ext]
 lemma from_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
     {f g : (single V c j).obj A ⟶ K} (hfg : f.f j = g.f j) : f = g := by
@@ -126,8 +138,6 @@ instance (j : ι) : (single V c j).Full where
       ext
       simp [single_map_f_self]⟩
 
-variable {c}
-
 /-- Constructor for morphisms to a single homological complex. -/
 noncomputable def mkHomToSingle {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A)
     (hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0) :

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

@@ -25,7 +25,7 @@ We provide the following results:
 -/
 
 
-universe v₁ v₂ v₃ u₁ u₂ u₃
+universe v u v₁ v₂ v₃ u₁ u₂ u₃
 
 noncomputable section
 
@@ -180,4 +180,31 @@ def preservesInitialObjectOfPreservesZeroMorphisms [PreservesZeroMorphisms F] :
 
 end ZeroObject
 
+section
+
+variable [HasZeroObject D] [HasZeroMorphisms D]
+  (G : C ⥤ D) (hG : IsZero G) (J : Type*) [Category J]
+
+/-- A zero functor preserves limits. -/
+def preservesLimitsOfShapeOfIsZero : PreservesLimitsOfShape J G where
+  preservesLimit {K} := ⟨fun hc => by
+    rw [Functor.isZero_iff] at hG
+    exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩
+
+/-- A zero functor preserves colimits. -/
+def preservesColimitsOfShapeOfIsZero : PreservesColimitsOfShape J G where
+  preservesColimit {K} := ⟨fun hc => by
+    rw [Functor.isZero_iff] at hG
+    exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩
+
+/-- A zero functor preserves limits. -/
+def preservesLimitsOfSizeOfIsZero : PreservesLimitsOfSize.{v, u} G where
+  preservesLimitsOfShape := G.preservesLimitsOfShapeOfIsZero hG _
+
+/-- A zero functor preserves colimits. -/
+def preservesColimitsOfSizeOfIsZero : PreservesColimitsOfSize.{v, u} G where
+  preservesColimitsOfShape := G.preservesColimitsOfShapeOfIsZero hG _
+
+end
+
 end CategoryTheory.Functor

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -665,4 +665,31 @@ instance isSplitEpi_prod_snd [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)
   IsSplitEpi.mk' { section_ := prod.lift 0 (𝟙 Y) }
 #align category_theory.limits.is_split_epi_prod_snd CategoryTheory.Limits.isSplitEpi_prod_snd
 
+
+section
+
+variable [HasZeroMorphisms C] [HasZeroObject C] {F : D ⥤ C}
+
+/-- If a functor `F` is zero, then any cone for `F` with a zero point is limit. -/
+def IsLimit.ofIsZero (c : Cone F) (hF : IsZero F) (hc : IsZero c.pt) : IsLimit c where
+  lift _ := 0
+  fac _ j := (F.isZero_iff.1 hF j).eq_of_tgt _ _
+  uniq _ _ _ := hc.eq_of_tgt _ _
+
+/-- If a functor `F` is zero, then any cocone for `F` with a zero point is colimit. -/
+def IsColimit.ofIsZero (c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) : IsColimit c where
+  desc _ := 0
+  fac _ j := (F.isZero_iff.1 hF j).eq_of_src _ _
+  uniq _ _ _ := hc.eq_of_src _ _
+
+lemma IsLimit.isZero_pt {c : Cone F} (hc : IsLimit c) (hF : IsZero F) : IsZero c.pt :=
+  (isZero_zero C).of_iso (IsLimit.conePointUniqueUpToIso hc
+    (IsLimit.ofIsZero (Cone.mk 0 0) hF (isZero_zero C)))
+
+lemma IsColimit.isZero_pt {c : Cocone F} (hc : IsColimit c) (hF : IsZero F) : IsZero c.pt :=
+  (isZero_zero C).of_iso (IsColimit.coconePointUniqueUpToIso hc
+    (IsColimit.ofIsZero (Cocone.mk 0 0) hF (isZero_zero C)))
+
+end
+
 end CategoryTheory.Limits