(Co)limits in subcategories of comma categories defined by morphism properties

noncomputable def CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitOfClosed {T : Type u_1} [Category.{u_5, u_1} T] (P : MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [Category.{u_6, u_2} A] [Category.{u_7, u_3} B] [Category.{u_8, u_4} J] {L : Functor A T} {R : Functor B T} (D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤)) (h : Limits.ClosedUnderLimitsOfShape J fun (f : Comma L R) => P f.hom) [Limits.HasLimit (D.comp (forget L R P ⊤ ⊤))] : CreatesLimit D (forget L R P ⊤ ⊤)

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 CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed {T : Type u_1} [Category.{u_5, u_1} T] (P : MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [Category.{u_6, u_2} A] [Category.{u_7, u_3} B] [Category.{u_8, u_4} J] {L : Functor A T} {R : Functor B T} [Limits.HasLimitsOfShape J (Comma L R)] (h : Limits.ClosedUnderLimitsOfShape J fun (f : Comma L R) => P f.hom) : CreatesLimitsOfShape J (forget L R P ⊤ ⊤)

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.

theorem CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape {T : Type u_1} [Category.{u_8, u_1} T] (P : MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [Category.{u_6, u_2} A] [Category.{u_7, u_3} B] [Category.{u_5, u_4} J] {L : Functor A T} {R : Functor B T} (D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤)) (h : Limits.ClosedUnderLimitsOfShape J fun (f : Comma L R) => P f.hom) [Limits.HasLimit (D.comp (forget L R P ⊤ ⊤))] : Limits.HasLimit D

theorem CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape {T : Type u_1} [Category.{u_8, u_1} T] (P : MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [Category.{u_6, u_2} A] [Category.{u_7, u_3} B] [Category.{u_5, u_4} J] {L : Functor A T} {R : Functor B T} [Limits.HasLimitsOfShape J (Comma L R)] (h : Limits.ClosedUnderLimitsOfShape J fun (f : Comma L R) => P f.hom) : Limits.HasLimitsOfShape J (MorphismProperty.Comma L R P ⊤ ⊤)

theorem CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty {T : Type u_1} [Category.{u_4, u_1} T] (P : MorphismProperty T) {A : Type u_2} [Category.{u_3, u_2} A] {L : Functor A T} [L.Faithful] [L.Full] {Y : A} [P.ContainsIdentities] [P.RespectsIso] : Limits.ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) fun (f : CostructuredArrow L (L.obj Y)) => P f.hom

theorem CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) {X : T} [P.ContainsIdentities] [P.RespectsIso] : Limits.ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) fun (f : Over X) => P f.hom

theorem CategoryTheory.Over.closedUnderLimitsOfShape_pullback {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) {X : T} [Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] : Limits.ClosedUnderLimitsOfShape Limits.WalkingCospan fun (f : Over X) => P f.hom

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.

noncomputable instance CategoryTheory.MorphismProperty.Over.instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) (X : T) [P.ContainsIdentities] [P.RespectsIso] : CreatesLimitsOfShape (Discrete PEmpty.{1}) (Over.forget P ⊤ X)

instance CategoryTheory.MorphismProperty.Over.instUniqueHomTopMkId {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) {X : T} [P.ContainsIdentities] (Y : P.Over ⊤ X) : Unique (Y ⟶ Over.mk ⊤ (CategoryStruct.id X) ⋯)

def CategoryTheory.MorphismProperty.Over.mkIdTerminal {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) (X : T) [P.ContainsIdentities] : Limits.IsTerminal (Over.mk ⊤ (CategoryStruct.id X) ⋯)

X ⟶ X is the terminal object of P.Over ⊤ X.

instance CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) (X : T) [P.ContainsIdentities] : Limits.HasTerminal (P.Over ⊤ X)

noncomputable instance CategoryTheory.MorphismProperty.Over.createsLimitsOfShape_walkingCospan {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) (X : T) [Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] : CreatesLimitsOfShape Limits.WalkingCospan (Over.forget P ⊤ X)

If P is stable under composition, base change and satisfies post-cancellation, Over.forget P ⊤ X creates pullbacks.

@[instance 900]

instance CategoryTheory.MorphismProperty.Over.hasPullbacks {T : Type u_1} [Category.{u_2, u_1} T] (P : MorphismProperty T) (X : T) [Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] : Limits.HasPullbacks (P.Over ⊤ X)

If P is stable under composition, base change and satisfies post-cancellation, P.Over ⊤ X has pullbacks