mathlib3 documentation

category_theory.limits.colimit_limit

The morphism comparing a colimit of limits with the corresponding limit of colimits. #

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

For F : J × K ⥤ C there is always a morphism $\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$. While it is not usually an isomorphism, with additional hypotheses on J and K it may be, in which case we say that "colimits commute with limits".

The prototypical example, proved in category_theory.limits.filtered_colimit_commutes_finite_limit, is that when C = Type, filtered colimits commute with finite limits.

References #

source
theorem category_theory.limits.map_id_left_eq_curry_map {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J × K ⥤ C) {j : J} {k k' : K} {f : k ⟶ k'} :
F.map (𝟙 j, f) = ((category_theory.curry.obj F).obj j).map f
source
theorem category_theory.limits.map_id_right_eq_curry_swap_map {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J × K ⥤ C) {j j' : J} {f : j ⟶ j'} {k : K} :
F.map (f, 𝟙 k) = ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k).map f
source
noncomputable def category_theory.limits.colimit_limit_to_limit_colimit {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J × K ⥤ C) [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.has_colimits_of_shape K C] :
category_theory.limits.colimit (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) ⟶ category_theory.limits.limit (category_theory.curry.obj F ⋙ category_theory.limits.colim)

The universal morphism $\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$.

Equations
Instances for category_theory.limits.colimit_limit_to_limit_colimit
source
@[simp]
theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J × K ⥤ C) [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.has_colimits_of_shape K C] (j : J) (k : K) :
category_theory.limits.colimit.ι (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) k ≫ category_theory.limits.colimit_limit_to_limit_colimit F ≫ category_theory.limits.limit.π (category_theory.curry.obj F ⋙ category_theory.limits.colim) j = category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j ≫ category_theory.limits.colimit.ι ((category_theory.curry.obj F).obj j) k

Since colimit_limit_to_limit_colimit is a morphism from a colimit to a limit, this lemma characterises it.

source
@[simp]
theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π_assoc {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J × K ⥤ C) [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.has_colimits_of_shape K C] (j : J) (k : K) {X' : C} (f' : (category_theory.curry.obj F ⋙ category_theory.limits.colim).obj j ⟶ X') :
category_theory.limits.colimit.ι (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) k ≫ category_theory.limits.colimit_limit_to_limit_colimit F ≫ category_theory.limits.limit.π (category_theory.curry.obj F ⋙ category_theory.limits.colim) j ≫ f' = category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j ≫ category_theory.limits.colimit.ι ((category_theory.curry.obj F).obj j) k ≫ f'
source
@[simp]
theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π_apply {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] (F : J × K ⥤ Type v) (j : J) (k : K) (f : (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim).obj k) :
category_theory.limits.limit.π (category_theory.curry.obj F ⋙ category_theory.limits.colim) j (category_theory.limits.colimit_limit_to_limit_colimit F (category_theory.limits.colimit.ι (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) k f)) = category_theory.limits.colimit.ι ((category_theory.curry.obj F).obj j) k (category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j f)
source
noncomputable def category_theory.limits.colimit_limit_to_limit_colimit_cone {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.has_colimits_of_shape K C] (G : J ⥤ K ⥤ C) [category_theory.limits.has_limit G] :
category_theory.limits.colim.map_cone (category_theory.limits.limit.cone G) ⟶ category_theory.limits.limit.cone (G ⋙ category_theory.limits.colim)

The map colimit_limit_to_limit_colimit realized as a map of cones.

Equations
Instances for category_theory.limits.colimit_limit_to_limit_colimit_cone
source
@[simp]
theorem category_theory.limits.colimit_limit_to_limit_colimit_cone_hom {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.has_colimits_of_shape K C] (G : J ⥤ K ⥤ C) [category_theory.limits.has_limit G] :
(category_theory.limits.colimit_limit_to_limit_colimit_cone G).hom = category_theory.limits.colim.map (category_theory.limits.limit_iso_swap_comp_lim G).hom ≫ category_theory.limits.colimit_limit_to_limit_colimit (category_theory.uncurry.obj G) ≫ category_theory.limits.lim.map (category_theory.whisker_right (category_theory.currying.unit_iso.app G).inv category_theory.limits.colim)