feat: preserves colimit if colimit.post is iso (#11421)

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -11,7 +11,7 @@ import Mathlib.CategoryTheory.Limits.HasLimits
 # Preservation and reflection of (co)limits.
 
 There are various distinct notions of "preserving limits". The one we
-aim to capture here is: A functor F : C → D "preserves limits" if it
+aim to capture here is: A functor F : C ⥤ D "preserves limits" if it
 sends every limit cone in C to a limit cone in D. Informally, F
 preserves all the limits which exist in C.
 
@@ -186,6 +186,13 @@ instance idPreservesColimits : PreservesColimitsOfSize.{w', w} (𝟭 C) where
               exact h.uniq _ m w⟩⟩ }
 #align category_theory.limits.id_preserves_colimits CategoryTheory.Limits.idPreservesColimits
 
+instance [HasLimit K] {F : C ⥤ D} [PreservesLimit K F] : HasLimit (K ⋙ F) where
+  exists_limit := ⟨⟨F.mapCone (limit.cone K), PreservesLimit.preserves (limit.isLimit K)⟩⟩
+
+instance [HasColimit K] {F : C ⥤ D} [PreservesColimit K F] : HasColimit (K ⋙ F) where
+  exists_colimit :=
+    ⟨⟨F.mapCocone (colimit.cocone K), PreservesColimit.preserves (colimit.isColimit K)⟩⟩
+
 section
 
 variable {E : Type u₃} [ℰ : Category.{v₃} E]

Mathlib/CategoryTheory/Limits/Preserves/Limits.lean

@@ -48,7 +48,7 @@ theorem preserves_lift_mapCone (c₁ c₂ : Cone F) (t : IsLimit c₁) :
   ((PreservesLimit.preserves t).uniq (G.mapCone c₂) _ (by simp [← G.map_comp])).symm
 #align category_theory.preserves_lift_map_cone CategoryTheory.preserves_lift_mapCone
 
-variable [HasLimit F] [HasLimit (F ⋙ G)]
+variable [HasLimit F]
 
 /-- If `G` preserves limits, we have an isomorphism from the image of the limit of a functor `F`
 to the limit of the functor `F ⋙ G`.
@@ -77,6 +77,9 @@ theorem lift_comp_preservesLimitsIso_hom (t : Cone F) :
   simp [← G.map_comp]
 #align category_theory.lift_comp_preserves_limits_iso_hom CategoryTheory.lift_comp_preservesLimitsIso_hom
 
+instance : IsIso (limit.post F G) :=
+  show IsIso (preservesLimitIso G F).hom from inferInstance
+
 variable [PreservesLimitsOfShape J G] [HasLimitsOfShape J D] [HasLimitsOfShape J C]
 
 /-- If `C, D` has all limits of shape `J`, and `G` preserves them, then `preservesLimitsIso` is
@@ -96,6 +99,19 @@ end
 
 section
 
+variable [HasLimit F] [HasLimit (F ⋙ G)]
+
+/-- If the comparison morphism `G.obj (limit F) ⟶ limit (F ⋙ G)` is an isomorphism, then `G`
+    preserves limits of `F`. -/
+def preservesLimitOfIsIsoPost [IsIso (limit.post F G)] : PreservesLimit F G :=
+  preservesLimitOfPreservesLimitCone (limit.isLimit F) (by
+    convert IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
+    assumption)
+
+end
+
+section
+
 variable [PreservesColimit F G]
 
 @[simp]
@@ -104,7 +120,7 @@ theorem preserves_desc_mapCocone (c₁ c₂ : Cocone F) (t : IsColimit c₁) :
   ((PreservesColimit.preserves t).uniq (G.mapCocone _) _ (by simp [← G.map_comp])).symm
 #align category_theory.preserves_desc_map_cocone CategoryTheory.preserves_desc_mapCocone
 
-variable [HasColimit F] [HasColimit (F ⋙ G)]
+variable [HasColimit F]
 
 -- TODO: think about swapping the order here
 /-- If `G` preserves colimits, we have an isomorphism from the image of the colimit of a functor `F`
@@ -134,6 +150,9 @@ theorem preservesColimitsIso_inv_comp_desc (t : Cocone F) :
   simp [← G.map_comp]
 #align category_theory.preserves_colimits_iso_inv_comp_desc CategoryTheory.preservesColimitsIso_inv_comp_desc
 
+instance : IsIso (colimit.post F G) :=
+  show IsIso (preservesColimitIso G F).inv from inferInstance
+
 variable [PreservesColimitsOfShape J G] [HasColimitsOfShape J D] [HasColimitsOfShape J C]
 
 /-- If `C, D` has all colimits of shape `J`, and `G` preserves them, then `preservesColimitIso`
@@ -154,4 +173,17 @@ def preservesColimitNatIso : colim ⋙ G ≅ (whiskeringRight J C D).obj G ⋙ c
 
 end
 
+section
+
+variable [HasColimit F] [HasColimit (F ⋙ G)]
+
+/-- If the comparison morphism `colimit (F ⋙ G) ⟶ G.obj (colimit F)` is an isomorphism, then `G`
+    preserves colimits of `F`. -/
+def preservesColimitOfIsIsoPost [IsIso (colimit.post F G)] : PreservesColimit F G :=
+  preservesColimitOfPreservesColimitCocone (colimit.isColimit F) (by
+    convert IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))
+    assumption)
+
+end
+
 end CategoryTheory