feat(CategoryTheory/Limits/MorphismProperty): dualise lemmas on limits (#30127)

We also add the object properties induced by morphism properties for `Comma`, `CostructuredArrow` and `StructuredArrow` and use them accordingly.

Author: chrisflav

Mathlib/CategoryTheory/Limits/MorphismProperty.lean

@@ -28,7 +28,7 @@ variable (D : J ⥤ P.Comma L R ⊤ ⊤)
 /-- If `P` is closed under limits of shape `J` in `Comma L R`, then when `D` has
 a limit in `Comma L R`, the forgetful functor creates this limit. -/
 noncomputable def forgetCreatesLimitOfClosed
-    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom))
+    (h : ClosedUnderLimitsOfShape J (P.commaObj L R))
     [HasLimit (D ⋙ forget L R P ⊤ ⊤)] :
     CreatesLimit D (forget L R P ⊤ ⊤) :=
   createsLimitOfFullyFaithfulOfIso
@@ -38,22 +38,51 @@ noncomputable def forgetCreatesLimitOfClosed
 /-- If `Comma L R` has limits of shape `J` and `Comma L R` is closed under limits of shape
 `J`, then `forget L R P ⊤ ⊤` creates limits of shape `J`. -/
 noncomputable def forgetCreatesLimitsOfShapeOfClosed [HasLimitsOfShape J (Comma L R)]
-    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom)) :
+    (h : ClosedUnderLimitsOfShape J (P.commaObj L R)) :
     CreatesLimitsOfShape J (forget L R P ⊤ ⊤) where
   CreatesLimit := forgetCreatesLimitOfClosed _ _ h
 
 lemma hasLimit_of_closedUnderLimitsOfShape
-    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom))
+    (h : ClosedUnderLimitsOfShape J (P.commaObj L R))
     [HasLimit (D ⋙ forget L R P ⊤ ⊤)] :
     HasLimit D :=
   haveI : CreatesLimit D (forget L R P ⊤ ⊤) := forgetCreatesLimitOfClosed _ D h
   hasLimit_of_created D (forget L R P ⊤ ⊤)
 
 lemma hasLimitsOfShape_of_closedUnderLimitsOfShape [HasLimitsOfShape J (Comma L R)]
-    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom)) :
+    (h : ClosedUnderLimitsOfShape J (P.commaObj L R)) :
     HasLimitsOfShape J (P.Comma L R ⊤ ⊤) where
   has_limit _ := hasLimit_of_closedUnderLimitsOfShape _ _ h
 
+/-- If `P` is closed under colimits of shape `J` in `Comma L R`, then when `D` has
+a colimit in `Comma L R`, the forgetful functor creates this colimit. -/
+noncomputable def forgetCreatesColimitOfClosed
+    (h : ClosedUnderColimitsOfShape J (P.commaObj L R))
+    [HasColimit (D ⋙ forget L R P ⊤ ⊤)] :
+    CreatesColimit D (forget L R P ⊤ ⊤) :=
+  createsColimitOfFullyFaithfulOfIso
+    (⟨colimit (D ⋙ forget L R P ⊤ ⊤), h.colimit fun j ↦ (D.obj j).prop⟩)
+    (Iso.refl _)
+
+/-- If `Comma L R` has colimits of shape `J` and `Comma L R` is closed under colimits of shape
+`J`, then `forget L R P ⊤ ⊤` creates colimits of shape `J`. -/
+noncomputable def forgetCreatesColimitsOfShapeOfClosed [HasColimitsOfShape J (Comma L R)]
+    (h : ClosedUnderColimitsOfShape J (P.commaObj L R)) :
+    CreatesColimitsOfShape J (forget L R P ⊤ ⊤) where
+  CreatesColimit := forgetCreatesColimitOfClosed _ _ h
+
+lemma hasColimit_of_closedUnderColimitsOfShape
+    (h : ClosedUnderColimitsOfShape J (P.commaObj L R))
+    [HasColimit (D ⋙ forget L R P ⊤ ⊤)] :
+    HasColimit D :=
+  haveI : CreatesColimit D (forget L R P ⊤ ⊤) := forgetCreatesColimitOfClosed _ D h
+  hasColimit_of_created D (forget L R P ⊤ ⊤)
+
+lemma hasColimitsOfShape_of_closedUnderColimitsOfShape [HasColimitsOfShape J (Comma L R)]
+    (h : ClosedUnderColimitsOfShape J (P.commaObj L R)) :
+    HasColimitsOfShape J (P.Comma L R ⊤ ⊤) where
+  has_colimit _ := hasColimit_of_closedUnderColimitsOfShape _ _ h
+
 end MorphismProperty.Comma
 
 section
@@ -63,13 +92,13 @@ variable {A : Type*} [Category A] {L : A ⥤ T}
 lemma CostructuredArrow.closedUnderLimitsOfShape_discrete_empty [L.Faithful] [L.Full] {Y : A}
     [P.ContainsIdentities] [P.RespectsIso] :
     ClosedUnderLimitsOfShape (Discrete PEmpty.{1})
-      (fun f : CostructuredArrow L (L.obj Y) ↦ P f.hom) := by
+      (P.costructuredArrowObj L (X := L.obj Y)) := by
   rintro D c hc -
   have : D = Functor.empty _ := Functor.empty_ext' _ _
   subst this
   let e : c.pt ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) :=
     hc.conePointUniqueUpToIso CostructuredArrow.mkIdTerminal
-  rw [P.costructuredArrow_iso_iff e]
+  rw [P.costructuredArrowObj_iff, P.costructuredArrow_iso_iff e]
   simpa using P.id_mem (L.obj Y)
 
 end
@@ -79,7 +108,7 @@ section
 variable {X : T}
 
 lemma Over.closedUnderLimitsOfShape_discrete_empty [P.ContainsIdentities] [P.RespectsIso] :
-    ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) (fun f : Over X ↦ P f.hom) :=
+    ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) (P.overObj (X := X)) :=
   CostructuredArrow.closedUnderLimitsOfShape_discrete_empty P
 
 /-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
@@ -89,12 +118,12 @@ Without the cancellation property, this does not in general. Consider for exampl
 `P = Function.Surjective` on `Type`. -/
 lemma Over.closedUnderLimitsOfShape_pullback [HasPullbacks T]
     [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] :
-    ClosedUnderLimitsOfShape WalkingCospan (fun f : Over X ↦ P f.hom) := by
+    ClosedUnderLimitsOfShape WalkingCospan (P.overObj (X := X)) := by
   intro D c hc hf
   have h : IsPullback (c.π.app .left).left (c.π.app .right).left (D.map WalkingCospan.Hom.inl).left
         (D.map WalkingCospan.Hom.inr).left := IsPullback.of_isLimit_cone <|
     Limits.isLimitOfPreserves (CategoryTheory.Over.forget X) hc
-  rw [show c.pt.hom = (c.π.app .left).left ≫ (D.obj .left).hom by simp]
+  rw [P.overObj_iff, show c.pt.hom = (c.π.app .left).left ≫ (D.obj .left).hom by simp]
   apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hf _)
   exact P.of_postcomp _ (D.obj WalkingCospan.one).hom (hf .one) (by simpa using hf .right)
 

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

@@ -54,6 +54,37 @@ section
 
 variable {W : MorphismProperty T} {X : T}
 
+/-- The object property on `Comma L R` induced by a morphism property. -/
+def commaObj (W : MorphismProperty T) : ObjectProperty (Comma L R) :=
+  fun f ↦ W f.hom
+
+@[simp] lemma commaObj_iff (Y : Comma L R) : W.commaObj L R Y ↔ W Y.hom := .rfl
+
+instance [W.RespectsIso] : (W.commaObj L R).IsClosedUnderIsomorphisms where
+  of_iso {X Y} e h := by
+    rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
+      W.cancel_right_of_respectsIso]
+
+/-- The object property on `CostructuredArrow L X` induced by a morphism property. -/
+def costructuredArrowObj (W : MorphismProperty T) : ObjectProperty (CostructuredArrow L X) :=
+  fun f ↦ W f.hom
+
+@[simp] lemma costructuredArrowObj_iff (Y : CostructuredArrow L X) :
+    W.costructuredArrowObj L Y ↔ W Y.hom := .rfl
+
+instance [W.RespectsIso] : (W.costructuredArrowObj L (X := X)).IsClosedUnderIsomorphisms :=
+  inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms
+
+/-- The object property on `StructuredArrow X R` induced by a morphism property. -/
+def structuredArrowObj (W : MorphismProperty T) : ObjectProperty (StructuredArrow X R) :=
+  fun f ↦ W f.hom
+
+@[simp] lemma structuredArrowObj_iff (Y : StructuredArrow X R) :
+    W.structuredArrowObj R Y ↔ W Y.hom := .rfl
+
+instance [W.RespectsIso] : (W.structuredArrowObj L (X := X)).IsClosedUnderIsomorphisms :=
+  inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms
+
 /-- The morphism property on `Over X` induced by a morphism property on `C`. -/
 def over (W : MorphismProperty T) {X : T} : MorphismProperty (Over X) := fun _ _ f ↦ W f.left
 
@@ -69,11 +100,17 @@ def overObj (W : MorphismProperty T) {X : T} : ObjectProperty (Over X) := fun f
 
 @[simp] lemma overObj_iff (Y : Over X) : W.overObj Y ↔ W Y.hom := .rfl
 
+instance [W.RespectsIso] : (W.overObj (X := X)).IsClosedUnderIsomorphisms :=
+  inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms
+
 /-- The object property on `Under X` induced by a morphism property. -/
 def underObj (W : MorphismProperty T) {X : T} : ObjectProperty (Under X) := fun f ↦ W f.hom
 
 @[simp] lemma underObj_iff (Y : Under X) : W.underObj Y ↔ W Y.hom := .rfl
 
+instance [W.RespectsIso] : (W.underObj (X := X)).IsClosedUnderIsomorphisms :=
+  inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms
+
 end
 
 variable (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B)