Limits and the category of (co)cones #
This files contains results that stem from the limit API. For the definition and the category
instance of Cone
, please refer to CategoryTheory/Limits/Cones.lean
.
Main results #
- The category of cones on
F : J ⥤ C
is equivalent to the categoryCostructuredArrow (const J) F
. - A cone is limiting iff it is terminal in the category of cones. As a corollary, an equivalence of categories of cones preserves limiting properties.
Given a cone c
over F
, we can interpret the legs of c
as structured arrows
c.pt ⟶ F.obj -
.
Instances For
Cone.toStructuredArrow
can be expressed in terms of Functor.toStructuredArrow
.
Instances For
Functor.toStructuredArrow
can be expressed in terms of Cone.toStructuredArrow
.
Instances For
Interpreting the legs of a cone as a structured arrow and then forgetting the arrow again does nothing.
Instances For
Interpreting the legs of a cone as a structured arrow, interpreting this arrow as an arrow over the cone point, and finally forgetting the arrow is the same as just applying the functor the cone was over.
Instances For
Given a diagram of StructuredArrow X F
s, we may obtain a cone with cone point X
.
Instances For
Given a cone c : Cone K
and a map f : X ⟶ F.obj c.X
, we can construct a cone of structured
arrows over X
with f
as the cone point.
Instances For
Construct an object of the category (Δ ↓ F)
from a cone on F
. This is part of an
equivalence, see Cone.equivCostructuredArrow
.
Instances For
Construct a cone on F
from an object of the category (Δ ↓ F)
. This is part of an
equivalence, see Cone.equivCostructuredArrow
.
Instances For
The category of cones on F
is just the comma category (Δ ↓ F)
, where Δ
is the constant
functor.
Instances For
A cone is a limit cone iff it is terminal.
Instances For
If G : Cone F ⥤ Cone F'
preserves terminal objects, it preserves limit cones.
Instances For
If G : Cone F ⥤ Cone F'
reflects terminal objects, it reflects limit cones.
Instances For
Given a cocone c
over F
, we can interpret the legs of c
as costructured arrows
F.obj - ⟶ c.pt
.
Instances For
Cocone.toCostructuredArrow
can be expressed in terms of Functor.toCostructuredArrow
.
Instances For
Functor.toCostructuredArrow
can be expressed in terms of Cocone.toCostructuredArrow
.
Instances For
Interpreting the legs of a cocone as a costructured arrow and then forgetting the arrow again does nothing.
Instances For
Interpreting the legs of a cocone as a costructured arrow, interpreting this arrow as an arrow over the cocone point, and finally forgetting the arrow is the same as just applying the functor the cocone was over.
Instances For
Given a diagram CostructuredArrow F X
s, we may obtain a cocone with cone point X
.
Instances For
Given a cocone c : Cocone K
and a map f : F.obj c.X ⟶ X
, we can construct a cocone of
costructured arrows over X
with f
as the cone point.
Instances For
Construct an object of the category (F ↓ Δ)
from a cocone on F
. This is part of an
equivalence, see Cocone.equivStructuredArrow
.
Instances For
Construct a cocone on F
from an object of the category (F ↓ Δ)
. This is part of an
equivalence, see Cocone.equivStructuredArrow
.
Instances For
The category of cocones on F
is just the comma category (F ↓ Δ)
, where Δ
is the constant
functor.
Instances For
A cocone is a colimit cocone iff it is initial.
Instances For
If G : Cocone F ⥤ Cocone F'
preserves initial objects, it preserves colimit cocones.
Instances For
If G : Cocone F ⥤ Cocone F'
reflects initial objects, it reflects colimit cocones.