Creating (co)limits #
We say that F
creates limits of K
if, given any limit cone c
for K ⋙ F
(i.e. below) we can lift it to a cone "above", and further that F
reflects
limits for K
.
- liftedCone : CategoryTheory.Limits.Cone K
a cone in the source category of the functor
- validLift : F.mapCone s.liftedCone ≅ c
the isomorphism expressing that
liftedCone
lifts the given cone
Define the lift of a cone: For a cone c
for K ⋙ F
, give a cone for K
which is a lift of c
, i.e. the image of it under F
is (iso) to c
.
We will then use this as part of the definition of creation of limits: every limit cone has a lift.
Note this definition is really only useful when c
is a limit already.
Instances For
- liftedCocone : CategoryTheory.Limits.Cocone K
a cocone in the source category of the functor
- validLift : F.mapCocone s.liftedCocone ≅ c
the isomorphism expressing that
liftedCocone
lifts the given cocone
Define the lift of a cocone: For a cocone c
for K ⋙ F
, give a cocone for
K
which is a lift of c
, i.e. the image of it under F
is (iso) to c
.
We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.
Note this definition is really only useful when c
is a colimit already.
Instances For
- reflects : {c : CategoryTheory.Limits.Cone K} → CategoryTheory.Limits.IsLimit (F.mapCone c) → CategoryTheory.Limits.IsLimit c
- lifts : (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)) → CategoryTheory.Limits.IsLimit c → CategoryTheory.LiftableCone K F c
any limit cone can be lifted to a cone above
Definition 3.3.1 of [Riehl].
We say that F
creates limits of K
if, given any limit cone c
for K ⋙ F
(i.e. below) we can lift it to a cone "above", and further that F
reflects
limits for K
.
If F
reflects isomorphisms, it suffices to show only that the lifted cone is
a limit - see createsLimitOfReflectsIso
.
Instances
- CreatesLimit : {K : CategoryTheory.Functor J C} → CategoryTheory.CreatesLimit K F
F
creates limits of shape J
if F
creates the limit of any diagram
K : J ⥤ C
.
Instances
- CreatesLimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesLimitsOfShape J F
F
creates limits if it creates limits of shape J
for any J
.
Instances
F
creates small limits if it creates limits of shape J
for any small J
.
Instances For
- reflects : {c : CategoryTheory.Limits.Cocone K} → CategoryTheory.Limits.IsColimit (F.mapCocone c) → CategoryTheory.Limits.IsColimit c
- lifts : (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F)) → CategoryTheory.Limits.IsColimit c → CategoryTheory.LiftableCocone K F c
any limit cocone can be lifted to a cocone above
Dual of definition 3.3.1 of [Riehl].
We say that F
creates colimits of K
if, given any limit cocone c
for
K ⋙ F
(i.e. below) we can lift it to a cocone "above", and further that F
reflects limits for K
.
If F
reflects isomorphisms, it suffices to show only that the lifted cocone is
a limit - see createsColimitOfReflectsIso
.
Instances
- CreatesColimit : {K : CategoryTheory.Functor J C} → CategoryTheory.CreatesColimit K F
F
creates colimits of shape J
if F
creates the colimit of any diagram
K : J ⥤ C
.
Instances
- CreatesColimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesColimitsOfShape J F
F
creates colimits if it creates colimits of shape J
for any small J
.
Instances
F
creates small colimits if it creates colimits of shape J
for any small J
.
Instances For
liftLimit t
is the cone for K
given by lifting the limit t
for K ⋙ F
.
Instances For
The lifted cone has an image isomorphic to the original cone.
Instances For
The lifted cone is a limit.
Instances For
If F
creates the limit of K
and K ⋙ F
has a limit, then K
has a limit.
If F
creates limits of shape J
, and D
has limits of shape J
, then
C
has limits of shape J
.
If F
creates limits, and D
has all limits, then C
has all limits.
liftColimit t
is the cocone for K
given by lifting the colimit t
for K ⋙ F
.
Instances For
The lifted cocone has an image isomorphic to the original cocone.
Instances For
The lifted cocone is a colimit.
Instances For
If F
creates the limit of K
and K ⋙ F
has a limit, then K
has a limit.
If F
creates colimits of shape J
, and D
has colimits of shape J
, then
C
has colimits of shape J
.
If F
creates colimits, and D
has all colimits, then C
has all colimits.
- liftedCone : CategoryTheory.Limits.Cone K
- validLift : F.mapCone s.liftedCone ≅ c
- makesLimit : CategoryTheory.Limits.IsLimit s.liftedCone
the lifted cone is limit
A helper to show a functor creates limits. In particular, if we can show
that for any limit cone c
for K ⋙ F
, there is a lift of it which is
a limit and F
reflects isomorphisms, then F
creates limits.
Usually, F
creating limits says that any lift of c
is a limit, but
here we only need to show that our particular lift of c
is a limit.
Instances For
- liftedCocone : CategoryTheory.Limits.Cocone K
- validLift : F.mapCocone s.liftedCocone ≅ c
- makesColimit : CategoryTheory.Limits.IsColimit s.liftedCocone
the lifted cocone is colimit
A helper to show a functor creates colimits. In particular, if we can show
that for any limit cocone c
for K ⋙ F
, there is a lift of it which is
a limit and F
reflects isomorphisms, then F
creates colimits.
Usually, F
creating colimits says that any lift of c
is a colimit, but
here we only need to show that our particular lift of c
is a colimit.
Instances For
If F
reflects isomorphisms and we can lift any limit cone to a limit cone,
then F
creates limits.
In particular here we don't need to assume that F reflects limits.
Instances For
When F
is fully faithful, to show that F
creates the limit for K
it suffices to exhibit a lift
of a limit cone for K ⋙ F
.
Instances For
When F
is fully faithful, and HasLimit (K ⋙ F)
, to show that F
creates the limit for K
it suffices to exhibit a lift of the chosen limit cone for K ⋙ F
.
Instances For
When F
is fully faithful, to show that F
creates the limit for K
it suffices to show that a
limit point is in the essential image of F
.
Instances For
When F
is fully faithful, and HasLimit (K ⋙ F)
, to show that F
creates the limit for K
it suffices to show that the chosen limit point is in the essential image of F
.
Instances For
F
preserves the limit of K
if it creates the limit and K ⋙ F
has the limit.
F
preserves the limit of shape J
if it creates these limits and D
has them.
F
preserves limits if it creates limits and D
has limits.
If F
reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then F
creates colimits.
In particular here we don't need to assume that F reflects colimits.
Instances For
When F
is fully faithful, to show that F
creates the colimit for K
it suffices to exhibit a
lift of a colimit cocone for K ⋙ F
.
Instances For
When F
is fully faithful, and HasColimit (K ⋙ F)
, to show that F
creates the colimit for K
it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F
.
Instances For
When F
is fully faithful, to show that F
creates the colimit for K
it suffices to show that
a colimit point is in the essential image of F
.
Instances For
When F
is fully faithful, and HasColimit (K ⋙ F)
, to show that F
creates the colimit for K
it suffices to show that the chosen colimit point is in the essential image of F
.
Instances For
F
preserves the colimit of K
if it creates the colimit and K ⋙ F
has the colimit.
F
preserves the colimit of shape J
if it creates these colimits and D
has them.
F
preserves limits if it creates limits and D
has limits.
Transfer creation of limits along a natural isomorphism in the diagram.
Instances For
If F
creates the limit of K
and F ≅ G
, then G
creates the limit of K
.
Instances For
If F
creates limits of shape J
and F ≅ G
, then G
creates limits of shape J
.
Instances For
If F
creates limits and F ≅ G
, then G
creates limits.
Instances For
Transfer creation of colimits along a natural isomorphism in the diagram.
Instances For
If F
creates the colimit of K
and F ≅ G
, then G
creates the colimit of K
.
Instances For
If F
creates colimits of shape J
and F ≅ G
, then G
creates colimits of shape J
.
Instances For
If F
creates colimits and F ≅ G
, then G
creates colimits.
Instances For
If F creates the limit of K, any cone lifts to a limit.
Instances For
If F creates the colimit of K, any cocone lifts to a colimit.
Instances For
Any cone lifts through the identity functor.
Instances For
The identity functor creates all limits.
Any cocone lifts through the identity functor.
Instances For
The identity functor creates all colimits.
Satisfy the inhabited linter
Satisfy the inhabited linter