Connected limits in the over category #
We show that the projection CostructuredArrow K B ⥤ C
creates and preserves
connected limits, without assuming that C
has any limits.
In particular, CostructuredArrow K B
has any connected limit which C
has.
From this we deduce the corresponding results for the over category.
(Implementation) Given a diagram in CostructuredArrow K B
, produce a natural transformation
from the diagram legs to the specific object.
Equations
Instances For
(Implementation) Given a cone in the base category, raise it to a cone in
CostructuredArrow K B
. Note this is where the connected assumption is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation) Show that the raised cone is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projection from CostructuredArrow K B
to C
creates any connected limit.
Equations
- One or more equations did not get rendered due to their size.
The forgetful functor from CostructuredArrow K B
preserves any connected limit.
The over category has any connected limit which the original category has.
The forgetful functor from the over category creates any connected limit.
Alias of CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected
.
The forgetful functor from the over category creates any connected limit.
Equations
Instances For
The forgetful functor from the over category preserves any connected limit.
Alias of CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected
.
The forgetful functor from the over category preserves any connected limit.
The over category has any connected limit which the original category has.
The functor taking a cone over F
to a cone over Over.post F : Over i ⥤ Over (F.obj i)
.
This takes limit cones to limit cones when J
is cofiltered. See isLimitConePost
Equations
- One or more equations did not get rendered due to their size.
Instances For
conePost
is compatible with the forgetful functors on over categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor taking a cone over F
to a cone over Over.post F : Over i ⥤ Over (F.obj i)
preserves limit cones
Equations
- One or more equations did not get rendered due to their size.