mathlib documentation


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

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} [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'} :

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

Instances for category_theory.limits.colimit_limit_to_limit_colimit