# mathlibdocumentation

category_theory.limits.functor_category

# (Co)limits in functor categories. #

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).

@[simp]
theorem category_theory.limits.limit.lift_π_app {C : Type u} {J : Type u₁} {K : Type u₂} (H : J K C) (j : J) (k : K) :
= (c.π.app j).app k
@[simp]
theorem category_theory.limits.limit.lift_π_app_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (H : J K C) (j : J) (k : K) {X' : C} (f' : (H.obj j).obj k X') :
f' = (c.π.app j).app k f'
@[simp]
theorem category_theory.limits.colimit.ι_desc_app_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (H : J K C) (j : J) (k : K) {X' : C} (f' : c.X.obj k X') :
f' = (c.ι.app j).app k f'
@[simp]
theorem category_theory.limits.colimit.ι_desc_app {C : Type u} {J : Type u₁} {K : Type u₂} (H : J K C) (j : J) (k : K) :
= (c.ι.app j).app k
def category_theory.limits.evaluation_jointly_reflects_limits {C : Type u} {J : Type u₁} {K : Type u₂} {F : J K C} (t : Π (k : K), ) :

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
def category_theory.limits.combine_cones {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) :

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_obj {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k : K) :
= (c k).cone.X
@[simp]
theorem category_theory.limits.combine_cones_π_app_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (j : J) (k : K) :
j).app k = (c k).cone.π.app j
@[simp]
theorem category_theory.limits.combine_cones_X_map {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k₁ k₂ : K) (f : k₁ k₂) :
= (c k₂).is_limit.lift {X := (c k₁).cone.X, π := (c k₁).cone.π F.flip.map f}
def category_theory.limits.evaluate_combined_cones {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k : K) :
(c k).cone

The stitched together cones each project down to the original given cones (up to iso).

Equations
def category_theory.limits.combined_is_limit {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) :

Stitching together limiting cones gives a limiting cone.

Equations
def category_theory.limits.evaluation_jointly_reflects_colimits {C : Type u} {J : Type u₁} {K : Type u₂} {F : J K C} (t : Π (k : K), ) :

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
def category_theory.limits.combine_cocones {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) :

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_obj {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k : K) :
= (c k).cocone.X
@[simp]
theorem category_theory.limits.combine_cocones_X_map {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k₁ k₂ : K) (f : k₁ k₂) :
= (c k₁).is_colimit.desc {X := (c k₂).cocone.X, ι := F.flip.map f (c k₂).cocone.ι}
@[simp]
theorem category_theory.limits.combine_cocones_ι_app_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (j : J) (k : K) :
j).app k = (c k).cocone.ι.app j
def category_theory.limits.evaluate_combined_cocones {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) (k : K) :
(c k).cocone

The stitched together cocones each project down to the original given cocones (up to iso).

Equations
def category_theory.limits.combined_is_colimit {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (c : Π (k : K), ) :

Stitching together colimiting cocones gives a colimiting cocone.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.limits.evaluation_preserves_limits_of_shape {C : Type u} {J : Type u₁} {K : Type u₂} (k : K) :
Equations
noncomputable def category_theory.limits.limit_obj_iso_limit_comp_evaluation {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (k : K) :

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
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_hom_π_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) {X' : C} (f' : (F k).obj j X') :
= f'
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_hom_π {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) {X' : C} (f' : (F.obj j).obj k X') :
= j f'
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_π_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.limit_map_limit_obj_iso_limit_comp_evaluation_hom_assoc {C : Type u} {J : Type u₁} {K : Type u₂} {i j : K} (F : J K C) (f : i j) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.limit_map_limit_obj_iso_limit_comp_evaluation_hom {C : Type u} {J : Type u₁} {K : Type u₂} {i j : K} (F : J K C) (f : i j) :
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_limit_map {C : Type u} {J : Type u₁} {K : Type u₂} {i j : K} (F : J K C) (f : i j) :
@[simp]
theorem category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_limit_map_assoc {C : Type u} {J : Type u₁} {K : Type u₂} {i j : K} (F : J K C) (f : i j) {X' : C} (f' : X') :
@[ext]
theorem category_theory.limits.limit_obj_ext {C : Type u} {J : Type u₁} {K : Type u₂} {H : J K C} {k : K} {W : C} {f g : W } (w : (j : J), f = g ) :
f = g
@[protected, instance]
noncomputable def category_theory.limits.evaluation_preserves_colimits_of_shape {C : Type u} {J : Type u₁} {K : Type u₂} (k : K) :
Equations
noncomputable def category_theory.limits.colimit_obj_iso_colimit_comp_evaluation {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (k : K) :

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
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_inv_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) {X' : C} (f' : X') :
= f'
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_inv {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_app_hom_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) {X' : C} (f' : X') :
= j f'
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_app_hom {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_inv_colimit_map {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) {i j : K} (f : i j) :
@[simp]
theorem category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_inv_colimit_map_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) {i j : K} (f : i j) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.colimit_map_colimit_obj_iso_colimit_comp_evaluation_hom {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) {i j : K} (f : i j) :
@[simp]
theorem category_theory.limits.colimit_map_colimit_obj_iso_colimit_comp_evaluation_hom_assoc {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) {i j : K} (f : i j) {X' : C} (f' : X') :
@[ext]
theorem category_theory.limits.colimit_obj_ext {C : Type u} {J : Type u₁} {K : Type u₂} {H : J K C} {k : K} {W : C} {f g : W} (w : (j : J), f = g) :
f = g
@[protected, instance]
noncomputable def category_theory.limits.evaluation_preserves_limits {C : Type u} {K : Type u₂} (k : K) :
Equations
def category_theory.limits.preserves_limit_of_evaluation {C : Type u} {D : Type u'} {J : Type u₁} {K : Type u₂} (F : D K C) (G : J D) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves the limit of some G : J ⥤ D if it does for each k : K.

Equations
def category_theory.limits.preserves_limits_of_shape_of_evaluation {C : Type u} {D : Type u'} {K : Type u₂} (F : D K C) (J : Type u_1) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves limits of shape J if it does for each k : K.

Equations
def category_theory.limits.preserves_limits_of_evaluation {C : Type u} {D : Type u'} {K : Type u₂} (F : D K C) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves all limits if it does for each k : K.

Equations
@[protected, instance]

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

Equations
@[protected, instance]
noncomputable def category_theory.limits.evaluation_preserves_colimits {C : Type u} {K : Type u₂} (k : K) :
Equations
def category_theory.limits.preserves_colimit_of_evaluation {C : Type u} {D : Type u'} {J : Type u₁} {K : Type u₂} (F : D K C) (G : J D) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves the colimit of some G : J ⥤ D if it does for each k : K.

Equations
def category_theory.limits.preserves_colimits_of_shape_of_evaluation {C : Type u} {D : Type u'} {K : Type u₂} (F : D K C) (J : Type u_1) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves all colimits of shape J if it does for each k : K.

Equations
def category_theory.limits.preserves_colimits_of_evaluation {C : Type u} {D : Type u'} {K : Type u₂} (F : D K C) (H : Π (k : K), ) :

F : D ⥤ K ⥤ C preserves all colimits if it does for each k : K.

Equations
@[protected, instance]

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

Equations
@[simp]
theorem category_theory.limits.limit_iso_flip_comp_lim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (X : K) :
noncomputable def category_theory.limits.limit_iso_flip_comp_lim {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) :

The limit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by the individual limits on objects.

Equations
@[simp]
theorem category_theory.limits.limit_iso_flip_comp_lim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (X : K) :
@[simp]
theorem category_theory.limits.limit_flip_iso_comp_lim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) (X : K) :
noncomputable def category_theory.limits.limit_flip_iso_comp_lim {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) :

A variant of limit_iso_flip_comp_lim where the arguemnts of F are flipped.

Equations
@[simp]
theorem category_theory.limits.limit_flip_iso_comp_lim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) (X : K) :
noncomputable def category_theory.limits.limit_iso_swap_comp_lim {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) :

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
@[simp]
theorem category_theory.limits.limit_iso_swap_comp_lim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) (X : K) :
@[simp]
theorem category_theory.limits.limit_iso_swap_comp_lim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) (X : K) :
@[simp]
theorem category_theory.limits.colimit_iso_flip_comp_colim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (X : K) :
@[simp]
theorem category_theory.limits.colimit_iso_flip_comp_colim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) (X : K) :
noncomputable def category_theory.limits.colimit_iso_flip_comp_colim {C : Type u} {J : Type u₁} {K : Type u₂} (F : J K C) :

The colimit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by the individual colimits on objects.

Equations
@[simp]
theorem category_theory.limits.colimit_flip_iso_comp_colim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) (X : K) :
@[simp]
theorem category_theory.limits.colimit_flip_iso_comp_colim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) (X : K) :
noncomputable def category_theory.limits.colimit_flip_iso_comp_colim {C : Type u} {J : Type u₁} {K : Type u₂} (F : K J C) :

A variant of colimit_iso_flip_comp_colim where the arguemnts of F are flipped.

Equations
@[simp]
theorem category_theory.limits.colimit_iso_swap_comp_colim_hom_app {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) (X : K) :
noncomputable def category_theory.limits.colimit_iso_swap_comp_colim {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) :

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
@[simp]
theorem category_theory.limits.colimit_iso_swap_comp_colim_inv_app {C : Type u} {J : Type u₁} {K : Type u₂} (G : J K C) (X : K) :