(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 (commaObj L R P))
[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 (commaObj L R P))
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 (commaObj L R P))
[Limits.HasLimit (D.comp (forget L R P ⊤ ⊤))]
:
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 (commaObj L R P))
:
Limits.HasLimitsOfShape J (MorphismProperty.Comma L R P ⊤ ⊤)
noncomputable def
CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitOfClosed
{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.ClosedUnderColimitsOfShape J (commaObj L R P))
[Limits.HasColimit (D.comp (forget L R P ⊤ ⊤))]
:
CreatesColimit D (forget L R P ⊤ ⊤)
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitsOfShapeOfClosed
{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.HasColimitsOfShape J (Comma L R)]
(h : Limits.ClosedUnderColimitsOfShape J (commaObj L R P))
:
CreatesColimitsOfShape J (forget L R P ⊤ ⊤)
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape
{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.ClosedUnderColimitsOfShape J (commaObj L R P))
[Limits.HasColimit (D.comp (forget L R P ⊤ ⊤))]
:
theorem
CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape
{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.HasColimitsOfShape J (Comma L R)]
(h : Limits.ClosedUnderColimitsOfShape J (commaObj L R P))
:
Limits.HasColimitsOfShape 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]
:
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]
:
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]
:
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]
:
Equations
- One or more equations did not get rendered due to their size.
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) ⋯)
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}
[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.
Equations
Instances For
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]
:
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