refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape (#29881)

This PR renames `ClosedUnderLimitsOfShape` as `ObjectProperty.IsClosedUnderLimitsOfShape`, and make it a typeclass.

The stability condition of a property `P` by (co)limits of shape `J` is now expressed as `P.colimitsOfShape J ≤ P`. This facilitates the connection with the relatively new API `ColimitPresentation` #29382 (and the related `ObjectProperty.ColimitOfShape`).

By using a typeclass for the stability condition, it will be possible to add instances `HasLimitsOfShape` instances for fullsubcategories.

This also makes the design more parallel to what we have for the stability under (co)limits of `MorphismProperty`.

Author: joelriou

Mathlib/CategoryTheory/Limits/FullSubcategory.lean

@@ -3,14 +3,14 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.CategoryTheory.Limits.Creates
-import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
+import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
 
 /-!
 # Limits in full subcategories
 
-We introduce the notion of a property closed under taking limits and show that if `P` is closed
-under taking limits, then limits in `FullSubcategory P` can be constructed from limits in `C`.
+If a property of objects `P` is closed under taking limits,
+then limits in `FullSubcategory P` can be constructed from limits in `C`.
 More precisely, the inclusion creates such limits.
 
 -/
@@ -24,46 +24,6 @@ open CategoryTheory
 
 namespace CategoryTheory.Limits
 
-/-- We say that a property is closed under limits of shape `J` if whenever all objects in a
-    `J`-shaped diagram have the property, any limit of this diagram also has the property. -/
-def ClosedUnderLimitsOfShape {C : Type u} [Category.{v} C] (J : Type w) [Category.{w'} J]
-    (P : ObjectProperty C) : Prop :=
-  ∀ ⦃F : J ⥤ C⦄ ⦃c : Cone F⦄ (_hc : IsLimit c), (∀ j, P (F.obj j)) → P c.pt
-
-/-- We say that a property is closed under colimits of shape `J` if whenever all objects in a
-    `J`-shaped diagram have the property, any colimit of this diagram also has the property. -/
-def ClosedUnderColimitsOfShape {C : Type u} [Category.{v} C] (J : Type w) [Category.{w'} J]
-    (P : ObjectProperty C) : Prop :=
-  ∀ ⦃F : J ⥤ C⦄ ⦃c : Cocone F⦄ (_hc : IsColimit c), (∀ j, P (F.obj j)) → P c.pt
-
-section
-
-variable {C : Type u} [Category.{v} C] {J : Type w} [Category.{w'} J] {P : ObjectProperty C}
-
-theorem closedUnderLimitsOfShape_of_limit [P.IsClosedUnderIsomorphisms]
-    (h : ∀ {F : J ⥤ C} [HasLimit F], (∀ j, P (F.obj j)) → P (limit F)) :
-    ClosedUnderLimitsOfShape J P := by
-  intro F c hc hF
-  have : HasLimit F := ⟨_, hc⟩
-  exact P.prop_of_iso ((limit.isLimit _).conePointUniqueUpToIso hc) (h hF)
-
-theorem closedUnderColimitsOfShape_of_colimit [P.IsClosedUnderIsomorphisms]
-    (h : ∀ {F : J ⥤ C} [HasColimit F], (∀ j, P (F.obj j)) → P (colimit F)) :
-    ClosedUnderColimitsOfShape J P := by
-  intro F c hc hF
-  have : HasColimit F := ⟨_, hc⟩
-  exact P.prop_of_iso ((colimit.isColimit _).coconePointUniqueUpToIso hc) (h hF)
-
-protected lemma ClosedUnderLimitsOfShape.limit (h : ClosedUnderLimitsOfShape J P) {F : J ⥤ C}
-    [HasLimit F] : (∀ j, P (F.obj j)) → P (limit F) :=
-  h (limit.isLimit _)
-
-protected lemma ClosedUnderColimitsOfShape.colimit (h : ClosedUnderColimitsOfShape J P) {F : J ⥤ C}
-    [HasColimit F] : (∀ j, P (F.obj j)) → P (colimit F) :=
-  h (colimit.isColimit _)
-
-end
-
 section
 
 variable {J : Type w} [Category.{w'} J] {C : Type u} [Category.{v} C] {P : ObjectProperty C}
@@ -97,47 +57,49 @@ def createsColimitFullSubcategoryInclusion (F : J ⥤ P.FullSubcategory)
     CreatesColimit F P.ι :=
   createsColimitFullSubcategoryInclusion' F (colimit.isColimit _) h
 
+variable (P J)
+
 /-- If `P` is closed under limits of shape `J`, then the inclusion creates such limits. -/
-def createsLimitFullSubcategoryInclusionOfClosed (h : ClosedUnderLimitsOfShape J P)
+def createsLimitFullSubcategoryInclusionOfClosed [P.IsClosedUnderLimitsOfShape J]
     (F : J ⥤ P.FullSubcategory) [HasLimit (F ⋙ P.ι)] :
     CreatesLimit F P.ι :=
-  createsLimitFullSubcategoryInclusion F (h.limit fun j => (F.obj j).property)
+  createsLimitFullSubcategoryInclusion F (P.prop_limit _ fun j => (F.obj j).property)
 
 /-- If `P` is closed under limits of shape `J`, then the inclusion creates such limits. -/
-def createsLimitsOfShapeFullSubcategoryInclusion (h : ClosedUnderLimitsOfShape J P)
+instance createsLimitsOfShapeFullSubcategoryInclusion [P.IsClosedUnderLimitsOfShape J]
     [HasLimitsOfShape J C] : CreatesLimitsOfShape J P.ι where
-  CreatesLimit := @fun F => createsLimitFullSubcategoryInclusionOfClosed h F
+  CreatesLimit := @fun F => createsLimitFullSubcategoryInclusionOfClosed J P F
 
-theorem hasLimit_of_closedUnderLimits (h : ClosedUnderLimitsOfShape J P)
+theorem hasLimit_of_closedUnderLimits [P.IsClosedUnderLimitsOfShape J]
     (F : J ⥤ P.FullSubcategory) [HasLimit (F ⋙ P.ι)] : HasLimit F :=
   have : CreatesLimit F P.ι :=
-    createsLimitFullSubcategoryInclusionOfClosed h F
+    createsLimitFullSubcategoryInclusionOfClosed J P F
   hasLimit_of_created F P.ι
 
-theorem hasLimitsOfShape_of_closedUnderLimits (h : ClosedUnderLimitsOfShape J P)
+instance hasLimitsOfShape_of_closedUnderLimits [P.IsClosedUnderLimitsOfShape J]
     [HasLimitsOfShape J C] : HasLimitsOfShape J P.FullSubcategory :=
-  { has_limit := fun F => hasLimit_of_closedUnderLimits h F }
+  { has_limit := fun F => hasLimit_of_closedUnderLimits J P F }
 
 /-- If `P` is closed under colimits of shape `J`, then the inclusion creates such colimits. -/
-def createsColimitFullSubcategoryInclusionOfClosed (h : ClosedUnderColimitsOfShape J P)
+def createsColimitFullSubcategoryInclusionOfClosed [P.IsClosedUnderColimitsOfShape J]
     (F : J ⥤ P.FullSubcategory) [HasColimit (F ⋙ P.ι)] :
     CreatesColimit F P.ι :=
-  createsColimitFullSubcategoryInclusion F (h.colimit fun j => (F.obj j).property)
+  createsColimitFullSubcategoryInclusion F (P.prop_colimit _ fun j => (F.obj j).property)
 
 /-- If `P` is closed under colimits of shape `J`, then the inclusion creates such colimits. -/
-def createsColimitsOfShapeFullSubcategoryInclusion (h : ClosedUnderColimitsOfShape J P)
+instance createsColimitsOfShapeFullSubcategoryInclusion [P.IsClosedUnderColimitsOfShape J]
     [HasColimitsOfShape J C] : CreatesColimitsOfShape J P.ι where
-  CreatesColimit := @fun F => createsColimitFullSubcategoryInclusionOfClosed h F
+  CreatesColimit := @fun F => createsColimitFullSubcategoryInclusionOfClosed J P F
 
-theorem hasColimit_of_closedUnderColimits (h : ClosedUnderColimitsOfShape J P)
+theorem hasColimit_of_closedUnderColimits [P.IsClosedUnderColimitsOfShape J]
     (F : J ⥤ P.FullSubcategory) [HasColimit (F ⋙ P.ι)] : HasColimit F :=
   have : CreatesColimit F P.ι :=
-    createsColimitFullSubcategoryInclusionOfClosed h F
+    createsColimitFullSubcategoryInclusionOfClosed J P F
   hasColimit_of_created F P.ι
 
-theorem hasColimitsOfShape_of_closedUnderColimits (h : ClosedUnderColimitsOfShape J P)
+instance hasColimitsOfShape_of_closedUnderColimits [P.IsClosedUnderColimitsOfShape J]
     [HasColimitsOfShape J C] : HasColimitsOfShape J P.FullSubcategory :=
-  { has_colimit := fun F => hasColimit_of_closedUnderColimits h F }
+  { has_colimit := fun F => hasColimit_of_closedUnderColimits J P F }
 
 end
 
@@ -147,19 +109,23 @@ variable {D : Type u₂} [Category.{v₂} D]
 variable (F : C ⥤ D)
 
 /-- The essential image of a functor is closed under the limits it preserves. -/
-protected lemma ClosedUnderLimitsOfShape.essImage [HasLimitsOfShape J C]
-    [PreservesLimitsOfShape J F] [F.Full] [F.Faithful] :
-    ClosedUnderLimitsOfShape J F.essImage := fun G _c hc hG ↦
-  ⟨limit (Functor.essImage.liftFunctor G F hG),
-    ⟨IsLimit.conePointsIsoOfNatIso (isLimitOfPreserves F (limit.isLimit _)) hc
-      (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩
+instance [HasLimitsOfShape J C] [PreservesLimitsOfShape J F] [F.Full] [F.Faithful] :
+    F.essImage.IsClosedUnderLimitsOfShape J :=
+  .mk' (by
+    rintro _ ⟨G, hG⟩
+    exact ⟨limit (Functor.essImage.liftFunctor G F hG),
+      ⟨IsLimit.conePointsIsoOfNatIso
+        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
+        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩)
 
 /-- The essential image of a functor is closed under the colimits it preserves. -/
-protected lemma ClosedUnderColimitsOfShape.essImage [HasColimitsOfShape J C]
-    [PreservesColimitsOfShape J F] [F.Full] [F.Faithful] :
-    ClosedUnderColimitsOfShape J F.essImage := fun G _c hc hG ↦
-  ⟨colimit (Functor.essImage.liftFunctor G F hG),
-    ⟨IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves F (colimit.isColimit _)) hc
-      (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩
+instance [HasColimitsOfShape J C] [PreservesColimitsOfShape J F] [F.Full] [F.Faithful] :
+    F.essImage.IsClosedUnderColimitsOfShape J :=
+  .mk' (by
+    rintro _ ⟨G, hG⟩
+    exact ⟨colimit (Functor.essImage.liftFunctor G F hG),
+      ⟨IsColimit.coconePointsIsoOfNatIso
+        (isColimitOfPreserves F (colimit.isColimit _)) (colimit.isColimit _)
+        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩)
 
 end CategoryTheory.Limits

Mathlib/CategoryTheory/Limits/Indization/Category.lean

@@ -113,23 +113,29 @@ noncomputable def Ind.yonedaCompInclusion : Ind.yoneda ⋙ Ind.inclusion C ≅ C
   isoWhiskerLeft (ObjectProperty.lift _ _ _)
     (isoWhiskerRight (Ind.equivalence C).counitIso (ObjectProperty.ι _))
 
+noncomputable instance {J : Type v} [SmallCategory J] [IsFiltered J] :
+    ObjectProperty.IsClosedUnderColimitsOfShape (IsIndObject (C := C)) J :=
+  .mk' (by
+    rintro _ ⟨F, hF⟩
+    exact isIndObject_colimit _ _ hF)
+
 noncomputable instance {J : Type v} [SmallCategory J] [IsFiltered J] :
     CreatesColimitsOfShape J (Ind.inclusion C) :=
-  letI _ : CreatesColimitsOfShape J (ObjectProperty.ι (IsIndObject (C := C))) :=
-    createsColimitsOfShapeFullSubcategoryInclusion (closedUnderColimitsOfShape_of_colimit
-      (isIndObject_colimit _ _))
   inferInstanceAs <|
     CreatesColimitsOfShape J ((Ind.equivalence C).functor ⋙ ObjectProperty.ι _)
 
 instance : HasFilteredColimits (Ind C) where
   HasColimitsOfShape _ _ _ :=
     hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (Ind.inclusion C)
 
+noncomputable instance {J : Type v} [HasLimitsOfShape (Discrete J) C] :
+    ObjectProperty.IsClosedUnderLimitsOfShape (IsIndObject (C := C)) (Discrete J) :=
+  .mk' (by
+    rintro _ ⟨F, hF⟩
+    exact isIndObject_limit_of_discrete_of_hasLimitsOfShape _ hF)
+
 noncomputable instance {J : Type v} [HasLimitsOfShape (Discrete J) C] :
     CreatesLimitsOfShape (Discrete J) (Ind.inclusion C) :=
-  letI _ : CreatesLimitsOfShape (Discrete J) (ObjectProperty.ι (IsIndObject (C := C))) :=
-    createsLimitsOfShapeFullSubcategoryInclusion (closedUnderLimitsOfShape_of_limit
-      (isIndObject_limit_of_discrete_of_hasLimitsOfShape _))
   inferInstanceAs <|
     CreatesLimitsOfShape (Discrete J) ((Ind.equivalence C).functor ⋙ ObjectProperty.ι _)
 
@@ -139,10 +145,6 @@ instance {J : Type v} [HasLimitsOfShape (Discrete J) C] :
 
 noncomputable instance [HasLimitsOfShape WalkingParallelPair C] :
     CreatesLimitsOfShape WalkingParallelPair (Ind.inclusion C) :=
-  letI _ : CreatesLimitsOfShape WalkingParallelPair
-      (ObjectProperty.ι (IsIndObject (C := C))) :=
-    createsLimitsOfShapeFullSubcategoryInclusion
-      (closedUnderLimitsOfShape_walkingParallelPair_isIndObject)
   inferInstanceAs <|
     CreatesLimitsOfShape WalkingParallelPair
       ((Ind.equivalence C).functor ⋙ ObjectProperty.ι _)

Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
-import Mathlib.CategoryTheory.Limits.FullSubcategory
 import Mathlib.CategoryTheory.Limits.Indization.ParallelPair
+import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
 
 /-!
 # Equalizers of ind-objects
@@ -63,17 +63,21 @@ end
 
 This is Proposition 6.1.17(i) in [Kashiwara2006].
 -/
-theorem closedUnderLimitsOfShape_walkingParallelPair_isIndObject [HasEqualizers C] :
-    ClosedUnderLimitsOfShape WalkingParallelPair (IsIndObject (C := C)) := by
-  apply closedUnderLimitsOfShape_of_limit
-  intro F hF h
-  obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
-    (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
-    (F.map WalkingParallelPairHom.right)
-  exact IsIndObject.map
-    (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫
-      (diagramIsoParallelPair _).symm)).hom
-    (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ)
-      (fun i => isIndObject_limit_comp_yoneda _))
+instance isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair [HasEqualizers C] :
+    ObjectProperty.IsClosedUnderLimitsOfShape (IsIndObject (C := C)) WalkingParallelPair :=
+  .mk' (by
+    rintro _ ⟨F, h⟩
+    obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
+      (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
+      (F.map WalkingParallelPairHom.right)
+    exact IsIndObject.map
+      (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫
+        (diagramIsoParallelPair _).symm)).hom
+      (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ)
+        (fun i => isIndObject_limit_comp_yoneda _)))
+
+@[deprecated (since := "2025-09-22")]
+alias closedUnderLimitsOfShape_walkingParallelPair_isIndObject :=
+  isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
 
 end CategoryTheory.Limits