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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

theorem CategoryTheory.Over.closedUnderLimitsOfShape_pullback {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T} [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange) (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (CategoryTheory.CategoryStruct.comp f g) → P f) : CategoryTheory.Limits.ClosedUnderLimitsOfShape CategoryTheory.Limits.WalkingCospan fun (f : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] [P.RespectsIso] : CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.MorphismProperty.Over.instUniqueHomTopMkId P Y = { default := CategoryTheory.MorphismProperty.Over.homMk Y.hom ⋯ True.intro, uniq := ⋯ }

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

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

Equations

• CategoryTheory.MorphismProperty.Over.mkIdTerminal P X = CategoryTheory.Limits.IsTerminal.ofUnique (CategoryTheory.MorphismProperty.Over.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.MorphismProperty.Over.createsLimitsOfShape_walkingCospan {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange) (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (CategoryTheory.CategoryStruct.comp f g) → P f) : CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)

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

Equations

• CategoryTheory.MorphismProperty.Over.createsLimitsOfShape_walkingCospan P X hP of_postcomp = CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed P ⋯

theorem CategoryTheory.MorphismProperty.Over.hasPullbacks {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange) (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (CategoryTheory.CategoryStruct.comp f g) → P f) : CategoryTheory.Limits.HasPullbacks (P.Over ⊤ X)

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