Limits and colimits in comma categories #
We build limits in the comma category Comma L R
provided that the two source categories have
limits and R
preserves them.
This is used to construct limits in the arrow category, structured arrow category and under
category, and show that the appropriate forgetful functors create limits.
The duals of all the above are also given.
(Implementation). An auxiliary cone which is useful in order to construct limits in the comma category.
Equations
- CategoryTheory.Comma.limitAuxiliaryCone F c₁ = (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerLeft F (CategoryTheory.Comma.natTrans L R))).obj (L.mapCone c₁)
Instances For
If R
preserves the appropriate limit, then given a cone for F ⋙ fst L R : J ⥤ L
and a
limit cone for F ⋙ snd L R : J ⥤ R
we can build a cone for F
which will turn out to be a limit
cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Provided that R
preserves the appropriate limit, then the cone in coneOfPreserves
is a
limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation). An auxiliary cocone which is useful in order to construct colimits in the comma category.
Equations
- CategoryTheory.Comma.colimitAuxiliaryCocone F c₂ = (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerLeft F (CategoryTheory.Comma.natTrans L R))).obj (R.mapCocone c₂)
Instances For
If L
preserves the appropriate colimit, then given a colimit cocone for F ⋙ fst L R : J ⥤ L
and
a cocone for F ⋙ snd L R : J ⥤ R
we can build a cocone for F
which will turn out to be a
colimit cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Provided that L
preserves the appropriate colimit, then the cocone in coconeOfPreserves
is
a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.StructuredArrow.createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)} => inferInstance }
Equations
- CategoryTheory.StructuredArrow.createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.57} [CategoryTheory.Category.{?u.56, ?u.57} J] => inferInstance }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.CostructuredArrow.createsColimitsOfShape = { CreatesColimit := fun {K : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow G X)} => inferInstance }
Equations
- CategoryTheory.CostructuredArrow.createsColimitsOfSize = { CreatesColimitsOfShape := fun {J : Type ?u.57} [CategoryTheory.Category.{?u.56, ?u.57} J] => inferInstance }
Equations
- ⋯ = ⋯