feat(CategoryTheory/Limits): Some infrastructure for the preservation…

… of finite (co)limits (#17156)

Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

@@ -84,6 +84,11 @@ def compPreservesFiniteLimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteLimits
     [PreservesFiniteLimits G] : PreservesFiniteLimits (F ⋙ G) :=
   ⟨fun _ _ _ => inferInstance⟩
 
+/-- Transfer preservation of finite limits along a natural isomorphism in the functor. -/
+def preservesFiniteLimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesFiniteLimits F] :
+    PreservesFiniteLimits G where
+  preservesFiniteLimits _ _ _ := preservesLimitsOfShapeOfNatIso h
+
 /- Porting note: adding this class because quantified classes don't behave well
 [#2764](https://github.com/leanprover-community/mathlib4/pull/2764) -/
 /-- A functor `F` preserves finite products if it preserves all from `Discrete J`
@@ -225,6 +230,11 @@ def compPreservesFiniteColimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteColi
     [PreservesFiniteColimits G] : PreservesFiniteColimits (F ⋙ G) :=
   ⟨fun _ _ _ => inferInstance⟩
 
+/-- Transfer preservation of finite colimits along a natural isomorphism in the functor. -/
+def preservesFiniteColimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesFiniteColimits F] :
+    PreservesFiniteColimits G where
+  preservesFiniteColimits _ _ _ := preservesColimitsOfShapeOfNatIso h
+
 /- Porting note: adding this class because quantified classes don't behave well
 [#2764](https://github.com/leanprover-community/mathlib4/pull/2764) -/
 /-- A functor `F` preserves finite products if it preserves all from `Discrete J`
@@ -248,7 +258,6 @@ noncomputable instance compPreservesFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E)
 noncomputable instance (F : C ⥤ D) [PreservesFiniteColimits F] : PreservesFiniteCoproducts F where
   preserves _ _ := inferInstance
 
-
 /--
 A functor is said to reflect finite colimits, if it reflects all colimits of shape `J`,
 where `J : Type` is a finite category.

Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.Limits.Presheaf
 
@@ -104,4 +105,16 @@ noncomputable def preservesLimitOfLanPreservesLimit {C D : Type u} [SmallCategor
   apply @preservesLimitsOfShapeOfReflectsOfPreserves _ _ _ _ _ _ _ _ F yoneda ?_
   exact preservesLimitsOfShapeOfNatIso (Presheaf.compYonedaIsoYonedaCompLan F).symm
 
+/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`. -/
+def preservesFiniteLimitsOfEvaluation {D : Type*} [Category D] {E : Type*} [Category E]
+    (F : C ⥤ D ⥤ E) (h : ∀ d : D, PreservesFiniteLimits (F ⋙ (evaluation D E).obj d)) :
+    PreservesFiniteLimits F :=
+  ⟨fun J _ _ => preservesLimitsOfShapeOfEvaluation F J fun k => (h k).preservesFiniteLimits _⟩
+
+/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`. -/
+def preservesFiniteColimitsOfEvaluation {D : Type*} [Category D] {E : Type*} [Category E]
+    (F : C ⥤ D ⥤ E) (h : ∀ d : D, PreservesFiniteColimits (F ⋙ (evaluation D E).obj d)) :
+    PreservesFiniteColimits F :=
+  ⟨fun J _ _ => preservesColimitsOfShapeOfEvaluation F J fun k => (h k).preservesFiniteColimits _⟩
+
 end CategoryTheory