(Co)limits in functor categories. #
We show that if D
has limits, then the functor category C ⥤ D
also has limits
(CategoryTheory.Limits.functorCategoryHasLimits
),
and the evaluation functors preserve limits
(CategoryTheory.Limits.evaluationPreservesLimits
)
(and similarly for colimits).
We also show that F : D ⥤ K ⥤ C
preserves (co)limits if it does so for each k : K
(CategoryTheory.Limits.preservesLimitsOfEvaluation
and
CategoryTheory.Limits.preservesColimitsOfEvaluation
).
The evaluation functors jointly reflect limits: that is, to show a cone is a limit of F
it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is
limiting you can show it's pointwise limiting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a functor F
and a collection of limit cones for each diagram X ↦ F X k
, we can stitch
them together to give a cone for the diagram F
.
combinedIsLimit
shows that the new cone is limiting, and evalCombined
shows it is
(essentially) made up of the original cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stitched together cones each project down to the original given cones (up to iso).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stitching together limiting cones gives a limiting cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of F
it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is
colimiting you can show it's pointwise colimiting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a functor F
and a collection of colimit cocones for each diagram X ↦ F X k
, we can stitch
them together to give a cocone for the diagram F
.
combinedIsColimit
shows that the new cocone is colimiting, and evalCombined
shows it is
(essentially) made up of the original cocones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stitched together cocones each project down to the original given cocones (up to iso).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stitching together colimiting cocones gives a colimiting cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
If F : J ⥤ K ⥤ C
is a functor into a functor category which has a limit,
then the evaluation of that limit at k
is the limit of the evaluations of F.obj j
at k
.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
If F : J ⥤ K ⥤ C
is a functor into a functor category which has a colimit,
then the evaluation of that colimit at k
is the colimit of the evaluations of F.obj j
at k
.
Equations
Instances For
Equations
- CategoryTheory.Limits.evaluationPreservesLimits k = { preservesLimitsOfShape := fun {x : Type ?u.49} (_𝒥 : CategoryTheory.Category.{?u.49, ?u.49} x) => inferInstance }
F : D ⥤ K ⥤ C
preserves the limit of some G : J ⥤ D
if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F : D ⥤ K ⥤ C
preserves limits of shape J
if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F : D ⥤ K ⥤ C
preserves all limits if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant functor C ⥤ (D ⥤ C)
preserves limits.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Limits.evaluationPreservesColimits k = { preservesColimitsOfShape := fun {J : Type ?u.49} [CategoryTheory.Category.{?u.49, ?u.49} J] => inferInstance }
F : D ⥤ K ⥤ C
preserves the colimit of some G : J ⥤ D
if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F : D ⥤ K ⥤ C
preserves all colimits of shape J
if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F : D ⥤ K ⥤ C
preserves all colimits if it does for each k : K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant functor C ⥤ (D ⥤ C)
preserves colimits.
Equations
- One or more equations did not get rendered due to their size.
The limit of a diagram F : J ⥤ K ⥤ C
is isomorphic to the functor given by
the individual limits on objects.
Equations
Instances For
A variant of limitIsoFlipCompLim
where the arguments of F
are flipped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor G : J ⥤ K ⥤ C
, its limit K ⥤ C
is given by (G' : K ⥤ J ⥤ C) ⋙ lim
.
Note that this does not require K
to be small.
Equations
- CategoryTheory.Limits.limitIsoSwapCompLim G = CategoryTheory.Limits.limitIsoFlipCompLim G ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.flipIsoCurrySwapUncurry G) CategoryTheory.Limits.lim
Instances For
The colimit of a diagram F : J ⥤ K ⥤ C
is isomorphic to the functor given by
the individual colimits on objects.
Equations
Instances For
A variant of colimit_iso_flip_comp_colim
where the arguments of F
are flipped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor G : J ⥤ K ⥤ C
, its colimit K ⥤ C
is given by (G' : K ⥤ J ⥤ C) ⋙ colim
.
Note that this does not require K
to be small.
Equations
- One or more equations did not get rendered due to their size.