Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

(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.
@[simp]
theorem CategoryTheory.Limits.combineCones_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) {k₁ : K} {k₂ : K} (f : k₁ k₂) :
(CategoryTheory.Limits.combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone (F.flip.map f) }

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.

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.

Stitching together limiting cones gives a limiting cone.

Equations
  • One or more equations did not get rendered due to their size.

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.
@[simp]
theorem CategoryTheory.Limits.combineCocones_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) {k₁ : K} {k₂ : K} (f : k₁ k₂) :
(CategoryTheory.Limits.combineCocones F c).pt.map f = (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := CategoryTheory.CategoryStruct.comp (F.flip.map f) (c k₂).cocone }

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.

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.

Stitching together colimiting cocones gives a colimiting cocone.

Equations
  • One or more equations did not get rendered due to their size.
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

Taking a limit after whiskering by G is the same as using G and then taking a limit.

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

Taking a colimit after whiskering by G is the same as using G and then taking a colimit.

Equations
  • One or more equations did not get rendered due to their size.

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.

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.

The constant functor C ⥤ (D ⥤ C) preserves limits.

Equations
  • One or more equations did not get rendered due to their size.

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.

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.

The constant functor C ⥤ (D ⥤ C) preserves colimits.

Equations
  • One or more equations did not get rendered due to their size.

A variant of limitIsoFlipCompLim where the arguments of F are flipped.

Equations
  • One or more equations did not get rendered due to their size.

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

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.

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.