feat: the category of short complexes has colimits (#6324)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib/Algebra/Homology/ShortComplex/Limits.lean

@@ -155,6 +155,144 @@ instance preservesMonomorphisms_π₃ :
 
 end
 
+/-- If a cocone with values in `ShortComplex C` is such that it becomes colimit
+when we apply the three projections `ShortComplex C ⥤ C`, then it is colimit. -/
+def isColimitOfIsColimitπ (c : Cocone F)
+    (h₁ : IsColimit (π₁.mapCocone c)) (h₂ : IsColimit (π₂.mapCocone c))
+    (h₃ : IsColimit (π₃.mapCocone c)) : IsColimit c where
+  desc s :=
+    { τ₁ := h₁.desc (π₁.mapCocone s)
+      τ₂ := h₂.desc (π₂.mapCocone s)
+      τ₃ := h₃.desc (π₃.mapCocone s)
+      comm₁₂ := h₁.hom_ext (fun j => by
+        have eq₁ := h₁.fac (π₁.mapCocone s)
+        have eq₂ := h₂.fac (π₂.mapCocone s)
+        have eq₁₂ := fun j => (c.ι.app j).comm₁₂
+        have eq₁₂' := fun j => (s.ι.app j).comm₁₂
+        dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
+        rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂])
+      comm₂₃ := h₂.hom_ext (fun j => by
+        have eq₂ := h₂.fac (π₂.mapCocone s)
+        have eq₃ := h₃.fac (π₃.mapCocone s)
+        have eq₂₃ := fun j => (c.ι.app j).comm₂₃
+        have eq₂₃' := fun j => (s.ι.app j).comm₂₃
+        dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
+        rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]) }
+  fac s j := by
+    ext
+    · apply IsColimit.fac h₁
+    · apply IsColimit.fac h₂
+    · apply IsColimit.fac h₃
+  uniq s m hm := by
+    ext
+    · exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))
+    · exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))
+    · exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))
+
+section
+
+variable (F) [HasColimit (F ⋙ π₁)] [HasColimit (F ⋙ π₂)] [HasColimit (F ⋙ π₃)]
+
+/-- Construction of a colimit cocone for a functor `J ⥤ ShortComplex C` using the colimits
+of the three components `J ⥤ C`. -/
+noncomputable def colimitCocone : Cocone F :=
+  Cocone.mk (ShortComplex.mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
+      (by aesop_cat))
+    { app := fun j => Hom.mk (colimit.ι (F ⋙ π₁) _) (colimit.ι (F ⋙ π₂) _)
+        (colimit.ι (F ⋙ π₃) _) (by aesop_cat) (by aesop_cat)
+      naturality := fun _ _ f => by
+        ext
+        · dsimp; erw [comp_id, colimit.w (F ⋙ π₁)]
+        · dsimp; erw [comp_id, colimit.w (F ⋙ π₂)]
+        · dsimp; erw [comp_id, colimit.w (F ⋙ π₃)] }
+
+/-- `colimitCocone F` becomes colimit after the application of `π₁ : ShortComplex C ⥤ C`. -/
+noncomputable def isColimitπ₁MapCoconeColimitCocone :
+    IsColimit (π₁.mapCocone (colimitCocone F)) :=
+  (IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Iso.refl _) (by aesop_cat)))
+
+/-- `colimitCocone F` becomes colimit after the application of `π₂ : ShortComplex C ⥤ C`. -/
+noncomputable def isColimitπ₂MapCoconeColimitCocone :
+    IsColimit (π₂.mapCocone (colimitCocone F)) :=
+  (IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Iso.refl _) (by aesop_cat)))
+
+/-- `colimitCocone F` becomes colimit after the application of `π₃ : ShortComplex C ⥤ C`. -/
+noncomputable def isColimitπ₃MapCoconeColimitCocone :
+    IsColimit (π₃.mapCocone (colimitCocone F)) :=
+  (IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Iso.refl _) (by aesop_cat)))
+
+/-- `colimitCocone F` is colimit. -/
+noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) :=
+  isColimitOfIsColimitπ _ (isColimitπ₁MapCoconeColimitCocone F)
+    (isColimitπ₂MapCoconeColimitCocone F) (isColimitπ₃MapCoconeColimitCocone F)
+
+instance hasColimit_of_hasColimitπ : HasColimit F := ⟨⟨⟨_, isColimitColimitCocone _⟩⟩⟩
+
+noncomputable instance : PreservesColimit F π₁ :=
+  preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F)
+    (isColimitπ₁MapCoconeColimitCocone F)
+
+noncomputable instance : PreservesColimit F π₂ :=
+  preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F)
+    (isColimitπ₂MapCoconeColimitCocone F)
+
+noncomputable instance : PreservesColimit F π₃ :=
+  preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F)
+    (isColimitπ₃MapCoconeColimitCocone F)
+
+end
+
+section
+
+variable [HasColimitsOfShape J C]
+
+instance hasColimitsOfShape :
+    HasColimitsOfShape J (ShortComplex C) where
+
+noncomputable instance : PreservesColimitsOfShape J (π₁ : _ ⥤ C) where
+
+noncomputable instance : PreservesColimitsOfShape J (π₂ : _ ⥤ C) where
+
+noncomputable instance : PreservesColimitsOfShape J (π₃ : _ ⥤ C) where
+
+end
+
+section
+
+variable [HasFiniteColimits C]
+
+instance hasFiniteColimits : HasFiniteColimits (ShortComplex C) :=
+  ⟨fun _ _ _ => inferInstance⟩
+
+noncomputable instance : PreservesFiniteColimits (π₁ : _ ⥤ C) :=
+  ⟨fun _ _ _ => inferInstance⟩
+
+noncomputable instance : PreservesFiniteColimits (π₂ : _ ⥤ C) :=
+  ⟨fun _ _ _ => inferInstance⟩
+
+noncomputable instance : PreservesFiniteColimits (π₃ : _ ⥤ C) :=
+  ⟨fun _ _ _ => inferInstance⟩
+
+end
+
+section
+
+variable [HasColimitsOfShape WalkingSpan C]
+
+instance preservesEpimorphisms_π₁ :
+    Functor.PreservesEpimorphisms (π₁ : _ ⥤ C) :=
+  CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _
+
+instance preservesEpimorphisms_π₂ :
+    Functor.PreservesEpimorphisms (π₂ : _ ⥤ C) :=
+  CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _
+
+instance preservesEpimorphisms_π₃ :
+    Functor.PreservesEpimorphisms (π₃ : _ ⥤ C) :=
+  CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _
+
+end
+
 end ShortComplex
 
 end CategoryTheory