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 CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit, is that when C = Type, filtered colimits commute with finite limits.

References #

theorem CategoryTheory.Limits.map_id_left_eq_curry_map {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) {j : J} {k : K} {k' : K} {f : k k'} : ( j, f) = ((CategoryTheory.curry.obj F).obj j).map f

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

Instances For
    theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] (F : CategoryTheory.Functor (J × K) (Type v)) (j : J) (k : K) (f : (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim).obj k) :
    CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj F) CategoryTheory.Limits.colim) j (CategoryTheory.Limits.colimitLimitToLimitColimit F (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types ((CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)).obj k) (_ : CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)).obj k)) j f)