# mathlib3documentation

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 #

theorem category_theory.limits.map_id_left_eq_curry_map {J K : Type v} {C : Type u} (F : J × K C) {j : J} {k k' : K} {f : k k'} :
F.map (𝟙 j, f) = .obj j).map f
theorem category_theory.limits.map_id_right_eq_curry_swap_map {J K : Type v} {C : Type u} (F : J × K C) {j j' : J} {f : j j'} {k : K} :

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
@[simp]

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

@[simp]
theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π_assoc {J K : Type v} {C : Type u} (F : J × K C) (j : J) (k : K) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.ι_colimit_limit_to_limit_colimit_π_apply {J K : Type v} (F : J × K Type v) (j : J) (k : K) (f : k) :

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
@[simp]