feat(CategoryTheory/Comma): limit properties of subcategories defined…

… by morphism properties (#18134)

We show that under suitable assumptions on `P` the full subcategory of `Over X` defined by `P` has terminal objects and pullbacks.

Mathlib.lean

@@ -1712,6 +1712,7 @@ import Mathlib.CategoryTheory.Limits.IsConnected
 import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Limits.Lattice
 import Mathlib.CategoryTheory.Limits.MonoCoprod
+import Mathlib.CategoryTheory.Limits.MorphismProperty
 import Mathlib.CategoryTheory.Limits.Opposites
 import Mathlib.CategoryTheory.Limits.Over
 import Mathlib.CategoryTheory.Limits.Pi

Mathlib/CategoryTheory/Comma/Basic.lean

@@ -163,7 +163,7 @@ theorem eqToHom_right (X Y : Comma L R) (H : X = Y) :
 
 section
 
-variable {X Y : Comma L R} (e : X ⟶ Y)
+variable {L R} {X Y : Comma L R} (e : X ⟶ Y)
 
 instance [IsIso e] : IsIso e.left :=
   (Comma.fst L R).map_isIso e

Mathlib/CategoryTheory/IsConnected.lean

@@ -42,7 +42,7 @@ category is preserved by the functor `(X × -)`. This appears in `CategoryTheory
 -/
 
 
-universe v₁ v₂ u₁ u₂
+universe w₁ w₂ v₁ v₂ u₁ u₂
 
 noncomputable section
 
@@ -419,9 +419,7 @@ def discreteIsConnectedEquivPUnit {α : Type u₁} [IsConnected (Discrete α)] :
       unitIso := isoConstant _ (Classical.arbitrary _)
       counitIso := Functor.punitExt _ _ }
 
-universe v u
-
-variable {C : Type u} [Category.{v} C]
+variable {C : Type w₂} [Category.{w₁} C]
 
 /-- For objects `X Y : C`, any natural transformation `α : const X ⟶ const Y` from a connected
 category must be constant.

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Comma.Arrow
-import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
+import Mathlib.CategoryTheory.Comma.Over
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 import Mathlib.CategoryTheory.Limits.Creates
 import Mathlib.CategoryTheory.Limits.Unit
@@ -225,6 +225,10 @@ namespace CostructuredArrow
 
 variable {G : A ⥤ T} {X : T} (F : J ⥤ CostructuredArrow G X)
 
+instance hasTerminal [G.Faithful] [G.Full] {Y : A} :
+    HasTerminal (CostructuredArrow G (G.obj Y)) :=
+  CostructuredArrow.mkIdTerminal.hasTerminal
+
 instance hasColimit [i₁ : HasColimit (F ⋙ proj G X)] [i₂ : PreservesColimit (F ⋙ proj G X) G] :
     HasColimit F := by
   haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
@@ -262,4 +266,10 @@ theorem epi_iff_epi_left [HasPushouts A] [PreservesColimitsOfShape WalkingSpan G
 
 end CostructuredArrow
 
+namespace Over
+
+instance {X : T} : HasTerminal (Over X) := CostructuredArrow.hasTerminal
+
+end Over
+
 end CategoryTheory

Mathlib/CategoryTheory/Limits/MorphismProperty.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.Limits.Comma
+import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
+import Mathlib.CategoryTheory.Limits.FullSubcategory
+import Mathlib.CategoryTheory.MorphismProperty.Comma
+import Mathlib.CategoryTheory.MorphismProperty.Limits
+
+/-!
+# (Co)limits in subcategories of comma categories defined by morphism properties
+
+-/
+
+namespace CategoryTheory
+
+open Limits MorphismProperty.Comma
+
+variable {T : Type*} [Category T] (P : MorphismProperty T)
+
+namespace MorphismProperty.Comma
+
+variable {A B J : Type*} [Category A] [Category B] [Category J] {L : A ⥤ T} {R : B ⥤ T}
+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))
+    [HasLimit (D ⋙ forget L R P ⊤ ⊤)] :
+    CreatesLimit D (forget L R P ⊤ ⊤) :=
+  createsLimitOfFullyFaithfulOfIso
+    (⟨limit (D ⋙ forget L R P ⊤ ⊤), h.limit fun j ↦ (D.obj j).prop⟩)
+    (Iso.refl _)
+
+/-- 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)) :
+    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))
+    [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)) :
+    HasLimitsOfShape J (P.Comma L R ⊤ ⊤) where
+  has_limit _ := hasLimit_of_closedUnderLimitsOfShape _ _ h
+
+end MorphismProperty.Comma
+
+section
+
+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
+  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]
+  simpa using P.id_mem (L.obj Y)
+
+end
+
+section
+
+variable {X : T}
+
+lemma Over.closedUnderLimitsOfShape_discrete_empty [P.ContainsIdentities] [P.RespectsIso] :
+    ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) (fun f : Over X ↦ P f.hom) :=
+  CostructuredArrow.closedUnderLimitsOfShape_discrete_empty P
+
+/-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
+the subcategory of `Over X` defined by `P` is closed under pullbacks.
+
+Without the cancellation property, this does not in general. Consider for example
+`P = Function.Surjective` on `Type`. -/
+lemma Over.closedUnderLimitsOfShape_pullback [HasPullbacks T]
+    [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    ClosedUnderLimitsOfShape WalkingCospan (fun f : Over X ↦ P f.hom) := 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]
+  apply P.comp_mem _ _ (hP h.flip ?_) (hf _)
+  exact of_postcomp (D.obj WalkingCospan.one).hom (hf .one) (by simpa using hf .right)
+
+end
+
+namespace MorphismProperty.Over
+
+variable (X : T)
+
+noncomputable instance [P.ContainsIdentities] [P.RespectsIso] :
+    CreatesLimitsOfShape (Discrete PEmpty.{1}) (Over.forget P ⊤ X) :=
+  haveI : HasLimitsOfShape (Discrete PEmpty.{1}) (Comma (𝟭 T) (Functor.fromPUnit X)) := by
+    show HasLimitsOfShape _ (Over X)
+    infer_instance
+  forgetCreatesLimitsOfShapeOfClosed P
+    (Over.closedUnderLimitsOfShape_discrete_empty _)
+
+variable {X} in
+instance [P.ContainsIdentities] (Y : P.Over ⊤ X) :
+    Unique (Y ⟶ Over.mk ⊤ (𝟙 X) (P.id_mem X)) where
+  default := Over.homMk Y.hom
+  uniq a := by
+    ext
+    · simp only [mk_left, Hom.hom_left, homMk_hom, Over.homMk_left]
+      rw [← Over.w a.hom]
+      simp only [mk_left, Functor.const_obj_obj, Hom.hom_left, mk_hom, Category.comp_id]
+    · rfl
+
+/-- `X ⟶ X` is the terminal object of `P.Over ⊤ X`. -/
+def mkIdTerminal [P.ContainsIdentities] :
+    IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) :=
+  IsTerminal.ofUnique _
+
+instance [P.ContainsIdentities] : HasTerminal (P.Over ⊤ X) :=
+  let h : IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) := Over.mkIdTerminal P X
+  h.hasTerminal
+
+/-- If `P` is stable under composition, base change and satisfies post-cancellation,
+`Over.forget P ⊤ X` creates pullbacks. -/
+noncomputable def createsLimitsOfShape_walkingCospan [HasPullbacks T]
+    [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    CreatesLimitsOfShape WalkingCospan (Over.forget P ⊤ X) :=
+  haveI : HasLimitsOfShape WalkingCospan (Comma (𝟭 T) (Functor.fromPUnit X)) :=
+    inferInstanceAs <| HasLimitsOfShape WalkingCospan (Over X)
+  forgetCreatesLimitsOfShapeOfClosed P
+    (Over.closedUnderLimitsOfShape_pullback P hP of_postcomp)
+
+/-- If `P` is stable under composition, base change and satisfies post-cancellation,
+`P.Over ⊤ X` has pullbacks -/
+lemma hasPullbacks [HasPullbacks T] [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    HasPullbacks (P.Over ⊤ X) :=
+  haveI : HasLimitsOfShape WalkingCospan (Comma (𝟭 T) (Functor.fromPUnit X)) :=
+    inferInstanceAs <| HasLimitsOfShape WalkingCospan (Over X)
+  hasLimitsOfShape_of_closedUnderLimitsOfShape P
+    (Over.closedUnderLimitsOfShape_pullback P hP of_postcomp)
+
+end MorphismProperty.Over
+
+end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

@@ -228,6 +228,13 @@ theorem of_isLimit' (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :
     IsPullback fst snd f g :=
   of_isLimit h
 
+/-- Variant of `of_isLimit` for an arbitrary cone on a diagram `WalkingCospan ⥤ C`. -/
+lemma of_isLimit_cone {D : WalkingCospan ⥤ C} {c : Cone D} (hc : IsLimit c) :
+    IsPullback (c.π.app .left) (c.π.app .right) (D.map WalkingCospan.Hom.inl)
+      (D.map WalkingCospan.Hom.inr) where
+  w := by simp_rw [Cone.w]
+  isLimit' := ⟨IsLimit.equivOfNatIsoOfIso _ _ _ (PullbackCone.isoMk c) hc⟩
+
 /-- The pullback provided by `HasPullback f g` fits into an `IsPullback`. -/
 theorem of_hasPullback (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
     IsPullback (pullback.fst f g) (pullback.snd f g) f g :=
@@ -428,6 +435,13 @@ theorem of_isColimit' (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :
     IsPushout f g inl inr :=
   of_isColimit h
 
+/-- Variant of `of_isColimit` for an arbitrary cocone on a diagram `WalkingSpan ⥤ C`. -/
+lemma of_isColimit_cocone {D : WalkingSpan ⥤ C} {c : Cocone D} (hc : IsColimit c) :
+    IsPushout (D.map WalkingSpan.Hom.fst) (D.map WalkingSpan.Hom.snd)
+      (c.ι.app .left) (c.ι.app .right) where
+  w := by simp_rw [Cocone.w]
+  isColimit' := ⟨IsColimit.equivOfNatIsoOfIso _ _ _ (PushoutCocone.isoMk c) hc⟩
+
 /-- The pushout provided by `HasPushout f g` fits into an `IsPushout`. -/
 theorem of_hasPushout (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g] :
     IsPushout f g (pushout.inl f g) (pushout.inr f g) :=

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Comma.Arrow
-import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.Order.CompleteBooleanAlgebra
 
 /-!
@@ -196,10 +195,14 @@ theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P
     (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f :=
   ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩
 
+lemma comma_iso_iff (P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B]
+    {L : A ⥤ C} {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) :
+    P f.hom ↔ P g.hom := by
+  simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]
+
 theorem arrow_iso_iff (P : MorphismProperty C) [RespectsIso P] {f g : Arrow C}
-    (e : f ≅ g) : P f.hom ↔ P g.hom := by
-  simp [← Arrow.inv_left_hom_right e.hom, cancel_left_of_respectsIso,
-    cancel_right_of_respectsIso]
+    (e : f ≅ g) : P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
 
 theorem arrow_mk_iso_iff (P : MorphismProperty C) [RespectsIso P] {W X Y Z : C}
     {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g :=