mathlib documentation

category_theory.limits.colimit_limit

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 #

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