(Co)limits in subcategories of comma categories defined by morphism properties #
noncomputable def
CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitOfClosed
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
(D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤))
[(commaObj L R P).IsClosedUnderLimitsOfShape J]
[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.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
[Limits.HasLimitsOfShape J (Comma L R)]
[(commaObj L R P).IsClosedUnderLimitsOfShape J]
:
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.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
(D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤))
[(commaObj L R P).IsClosedUnderLimitsOfShape J]
[Limits.HasLimit (D.comp (forget L R P ⊤ ⊤))]
:
instance
CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
[Limits.HasLimitsOfShape J (Comma L R)]
[(commaObj L R P).IsClosedUnderLimitsOfShape J]
:
Limits.HasLimitsOfShape J (MorphismProperty.Comma L R P ⊤ ⊤)
noncomputable def
CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitOfClosed
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
(D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤))
[(commaObj L R P).IsClosedUnderColimitsOfShape J]
[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.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
(J : Type u_4)
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
[Limits.HasColimitsOfShape J (Comma L R)]
[(commaObj L R P).IsClosedUnderColimitsOfShape J]
:
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.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
(D : Functor J (MorphismProperty.Comma L R P ⊤ ⊤))
[(commaObj L R P).IsClosedUnderColimitsOfShape J]
[Limits.HasColimit (D.comp (forget L R P ⊤ ⊤))]
:
instance
CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
{B : Type u_3}
{J : Type u_4}
[Category.{v_2, u_2} A]
[Category.{v_3, u_3} B]
[Category.{v_4, u_4} J]
{L : Functor A T}
{R : Functor B T}
[Limits.HasColimitsOfShape J (Comma L R)]
[(commaObj L R P).IsClosedUnderColimitsOfShape J]
:
Limits.HasColimitsOfShape J (MorphismProperty.Comma L R P ⊤ ⊤)
instance
CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{A : Type u_2}
[Category.{v_2, u_2} A]
{L : Functor A T}
[L.Faithful]
[L.Full]
{Y : A}
[P.ContainsIdentities]
[P.RespectsIso]
:
theorem
CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape
{T : Type u_1}
[Category.{v_1, u_1} T]
{A : Type u_2}
[Category.{v_2, u_2} A]
{L : Functor A T}
{J : Type u_3}
[Category.{v_3, u_3} J]
{P : MorphismProperty T}
[P.RespectsIso]
[Limits.PreservesColimitsOfShape J L]
[Limits.HasColimitsOfShape J A]
(c : (D : Functor J T) → [Limits.HasColimit D] → Limits.Cocone D)
(hc : (D : Functor J T) → [inst : Limits.HasColimit D] → Limits.IsColimit (c D))
(H :
∀ (D : Functor J T) [inst : Limits.HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
(∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s }))
(X : T)
:
instance
CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty
{T : Type u_1}
[Category.{v_1, u_1} T]
(P : MorphismProperty T)
{X : T}
[P.ContainsIdentities]
[P.RespectsIso]
:
instance
CategoryTheory.Over.closedUnderLimitsOfShape_pullback
{T : Type u_1}
[Category.{v_1, 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.{v_1, 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.{v_1, u_1} T]
(P : MorphismProperty T)
{X : T}
[P.ContainsIdentities]
(Y : P.Over ⊤ X)
:
Unique (Y ⟶ Over.mk ⊤ (CategoryStruct.id X) ⋯)
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.MorphismProperty.Over.mkIdTerminal
{T : Type u_1}
[Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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