# 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 u₁} {K : Type u₂} [] [] {C : Type u} (F : CategoryTheory.Functor (J × K) C) {j : J} {k : K} {k' : K} {f : k k'} :
F.map = ((CategoryTheory.curry.obj F).obj j).map f
theorem CategoryTheory.Limits.map_id_right_eq_curry_swap_map {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : CategoryTheory.Functor (J × K) C) {j : J} {j' : J} {f : j j'} {k : K} :
F.map = ((CategoryTheory.curry.obj (().comp F)).obj k).map f
noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimit {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : CategoryTheory.Functor (J × K) C) :
CategoryTheory.Limits.colimit ((CategoryTheory.curry.obj (().comp F)).comp CategoryTheory.Limits.lim) CategoryTheory.Limits.limit ((CategoryTheory.curry.obj F).comp CategoryTheory.Limits.colim)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : CategoryTheory.Functor (J × K) C) (j : J) (k : K) {Z : C} (h : CategoryTheory.Limits.colim.obj ((CategoryTheory.curry.obj F).obj j) Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj F).comp CategoryTheory.Limits.colim) j) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp F)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k) h)
@[simp]
theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : CategoryTheory.Functor (J × K) C) (j : J) (k : K) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj F).comp CategoryTheory.Limits.colim) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp F)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.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.

@[simp]
theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply {J : Type u₁} {K : Type u₂} [] [] [] [] (F : CategoryTheory.Functor (J × K) (Type v)) (j : J) (k : K) (f : ((CategoryTheory.curry.obj (().comp F)).comp CategoryTheory.Limits.lim).obj k) :
CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj F).comp CategoryTheory.Limits.colim) j (CategoryTheory.Limits.colimitLimitToLimitColimit F (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp F)).comp CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp F)).obj k) j f)
@[simp]
theorem CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (G : ) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.uncurry.obj G)) (CategoryTheory.Limits.lim.map (CategoryTheory.whiskerRight (CategoryTheory.currying.unitIso.app G).inv CategoryTheory.Limits.colim)))
noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimitCone {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (G : ) :
CategoryTheory.Limits.colim.mapCone CategoryTheory.Limits.limit.cone (G.comp CategoryTheory.Limits.colim)

The map colimit_limit_to_limit_colimit realized as a map of cones.

Equations
• One or more equations did not get rendered due to their size.
Instances For