mathlib3 documentation

category_theory.limits.functor_category

(Co)limits in functor categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We show that if D has limits, then the functor category C ⥤ D also has limits (category_theory.limits.functor_category_has_limits), and the evaluation functors preserve limits (category_theory.limits.evaluation_preserves_limits) (and similarly for colimits).

We also show that F : D ⥤ K ⥤ C preserves (co)limits if it does so for each k : K (category_theory.limits.preserves_limits_of_evaluation and category_theory.limits.preserves_colimits_of_evaluation).

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

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. combined_is_limit shows that the new cone is limiting, and eval_combined shows it is (essentially) made up of the original cones.

Equations
@[simp]
theorem category_theory.limits.combine_cones_X_map {C : Type u} [category_theory.category C] {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] (F : J K C) (c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k)) (k₁ k₂ : K) (f : k₁ k₂) :
(category_theory.limits.combine_cones F c).X.map f = (c k₂).is_limit.lift {X := (c k₁).cone.X, π := (c k₁).cone.π F.flip.map f}

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

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. combined_is_colimit shows that the new cocone is colimiting, and eval_combined shows it is (essentially) made up of the original cocones.

Equations
@[simp]
theorem category_theory.limits.combine_cocones_X_map {C : Type u} [category_theory.category C] {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] (F : J K C) (c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k)) (k₁ k₂ : K) (f : k₁ k₂) :
(category_theory.limits.combine_cocones F c).X.map f = (c k₁).is_colimit.desc {X := (c k₂).cocone.X, ι := F.flip.map f (c k₂).cocone.ι}

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

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