feat(CategoryTheory): more preservation properties of functors (#32423)

We consider the preservation of a limit or a colimit as an `ObjectProperty` in the category of functors.

Author: joelriou

Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean

@@ -24,10 +24,43 @@ namespace CategoryTheory
 
 open Limits
 
-variable {J C : Type*} (K K' : Type*) [Category K] [Category K'] [Category J] [Category C]
+variable {J J' C D : Type*} (K K' : Type*)
+  [Category K] [Category K'] [Category J] [Category J'] [Category C] [Category D]
 
 namespace ObjectProperty
 
+variable {K} in
+/-- The property of objects in the functor category `J ⥤ C`
+which preserves the limit of a functor `F : K ⥤ J`. -/
+abbrev preservesLimit (F : K ⥤ J) : ObjectProperty (J ⥤ C) := PreservesLimit F
+
+@[simp]
+lemma preservesLimit_iff (F : K ⥤ J) (G : J ⥤ C) :
+    preservesLimit F G ↔ PreservesLimit F G := Iff.rfl
+
+lemma congr_preservesLimit {F F' : K ⥤ J} (e : F ≅ F') :
+    preservesLimit (C := C) F = preservesLimit (C := C) F' := by
+  ext G
+  simp_rw [preservesLimit_iff]
+  exact ⟨fun h ↦ preservesLimit_of_iso_diagram _ e,
+    fun h ↦ preservesLimit_of_iso_diagram _ e.symm⟩
+
+variable {K} in
+/-- The property of objects in the functor category `J ⥤ C`
+which preserves the colimit of a functor `F : K ⥤ J`. -/
+abbrev preservesColimit (F : K ⥤ J) : ObjectProperty (J ⥤ C) := PreservesColimit F
+
+@[simp]
+lemma preservesColimit_iff (F : K ⥤ J) (G : J ⥤ C) :
+    preservesColimit F G ↔ PreservesColimit F G := Iff.rfl
+
+lemma congr_preservesColimit {F F' : K ⥤ J} (e : F ≅ F') :
+    preservesColimit (C := C) F = preservesColimit (C := C) F' := by
+  ext G
+  simp_rw [preservesColimit_iff]
+  exact ⟨fun h ↦ preservesColimit_of_iso_diagram _ e,
+    fun h ↦ preservesColimit_of_iso_diagram _ e.symm⟩
+
 /-- The property of objects in the functor category `J ⥤ C`
 which preserves limits of shape `K`. -/
 abbrev preservesLimitsOfShape : ObjectProperty (J ⥤ C) := PreservesLimitsOfShape K
@@ -36,6 +69,44 @@ abbrev preservesLimitsOfShape : ObjectProperty (J ⥤ C) := PreservesLimitsOfSha
 lemma preservesLimitsOfShape_iff (F : J ⥤ C) :
     preservesLimitsOfShape K F ↔ PreservesLimitsOfShape K F := Iff.rfl
 
+lemma preservesLimitsOfShape_eq_iSup :
+    preservesLimitsOfShape (J := J) (C := C) K =
+      ⨅ (F : K ⥤ J), preservesLimit F := by
+  ext G
+  simp only [preservesLimitsOfShape_iff, iInf_apply, preservesLimit_iff, iInf_Prop_eq]
+  exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩
+
+variable (J C) {K K'} in
+lemma congr_preservesLimitsOfShape (e : K ≌ K') :
+    preservesLimitsOfShape (J := J) (C := C) K = preservesLimitsOfShape K' := by
+  ext G
+  simp only [preservesLimitsOfShape_iff]
+  exact ⟨fun _ ↦ preservesLimitsOfShape_of_equiv e _,
+    fun _ ↦ preservesLimitsOfShape_of_equiv e.symm _⟩
+
+/-- The property of objects in the functor category `J ⥤ C`
+which preserves colimits of shape `K`. -/
+abbrev preservesColimitsOfShape : ObjectProperty (J ⥤ C) := PreservesColimitsOfShape K
+
+@[simp]
+lemma preservesColimitsOfShape_iff (F : J ⥤ C) :
+    preservesColimitsOfShape K F ↔ PreservesColimitsOfShape K F := Iff.rfl
+
+lemma preservesColimitsOfShape_eq_iSup :
+    preservesColimitsOfShape (J := J) (C := C) K =
+      ⨅ (F : K ⥤ J), preservesColimit F := by
+  ext G
+  simp only [preservesColimitsOfShape_iff, iInf_apply, preservesColimit_iff, iInf_Prop_eq]
+  exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩
+
+variable (J C) {K K'} in
+lemma congr_preservesColimitsOfShape (e : K ≌ K') :
+    preservesColimitsOfShape (J := J) (C := C) K = preservesColimitsOfShape K' := by
+  ext G
+  simp only [preservesColimitsOfShape_iff]
+  exact ⟨fun _ ↦ preservesColimitsOfShape_of_equiv e _,
+    fun _ ↦ preservesColimitsOfShape_of_equiv e.symm _⟩
+
 /-- The property of objects in the functor category `J ⥤ C`
 which preserves finite limits. -/
 abbrev preservesFiniteLimits : ObjectProperty (J ⥤ C) := PreservesFiniteLimits
@@ -44,6 +115,14 @@ abbrev preservesFiniteLimits : ObjectProperty (J ⥤ C) := PreservesFiniteLimits
 lemma preservesFiniteLimits_iff (F : J ⥤ C) :
     preservesFiniteLimits F ↔ PreservesFiniteLimits F := Iff.rfl
 
+/-- The property of objects in the functor category `J ⥤ C`
+which preserves finite colimits. -/
+abbrev preservesFiniteColimits : ObjectProperty (J ⥤ C) := PreservesFiniteColimits
+
+@[simp]
+lemma preservesFiniteColimits_iff (F : J ⥤ C) :
+    preservesFiniteColimits F ↔ PreservesFiniteColimits F := Iff.rfl
+
 instance [HasColimitsOfShape K' C]
     [PreservesLimitsOfShape K (colim (J := K') (C := C))] :
     (preservesLimitsOfShape K : ObjectProperty (J ⥤ C)).IsClosedUnderColimitsOfShape K' where