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

• Borceux, Handbook of categorical algebra 1, Section 2.13
• Stacks: Filtered colimits

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

theorem CategoryTheory.Limits.map_id_right_eq_curry_swap_map {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor (J × K) C) {j j' : J} {f : j ⟶ j'} {k : K} : F.map (f, CategoryStruct.id k) = ((curry.obj ((Prod.swap K J).comp F)).obj k).map f

noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimit {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor (J × K) C) [HasLimitsOfShape J C] [HasColimitsOfShape K C] : colimit ((curry.obj ((Prod.swap K J).comp F)).comp lim) ⟶ limit ((curry.obj F).comp 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.

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor (J × K) C) [HasLimitsOfShape J C] [HasColimitsOfShape K C] (j : J) (k : K) : CategoryStruct.comp (colimit.ι ((curry.obj ((Prod.swap K J).comp F)).comp lim) k) (CategoryStruct.comp (colimitLimitToLimitColimit F) (limit.π ((curry.obj F).comp colim) j)) = CategoryStruct.comp (limit.π ((curry.obj ((Prod.swap K J).comp F)).obj k) j) (colimit.ι ((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_π_assoc {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor (J × K) C) [HasLimitsOfShape J C] [HasColimitsOfShape K C] (j : J) (k : K) {Z : C} (h : colim.obj ((curry.obj F).obj j) ⟶ Z) : CategoryStruct.comp (colimit.ι ((curry.obj ((Prod.swap K J).comp F)).comp lim) k) (CategoryStruct.comp (colimitLimitToLimitColimit F) (CategoryStruct.comp (limit.π ((curry.obj F).comp colim) j) h)) = CategoryStruct.comp (limit.π ((curry.obj ((Prod.swap K J).comp F)).obj k) j) (CategoryStruct.comp (colimit.ι ((curry.obj F).obj j) k) h)

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] [Small.{v, u₁} J] [Small.{v, u₂} K] (F : Functor (J × K) (Type v)) (j : J) (k : K) (f : ((curry.obj ((Prod.swap K J).comp F)).comp lim).obj k) : limit.π ((curry.obj F).comp colim) j (colimitLimitToLimitColimit F (colimit.ι ((curry.obj ((Prod.swap K J).comp F)).comp lim) k f)) = colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj ((Prod.swap K J).comp F)).obj k) j f)

noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimitCone {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [HasColimitsOfShape K C] (G : Functor J (Functor K C)) [HasLimit G] : colim.mapCone (limit.cone G) ⟶ limit.cone (G.comp 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.

@[simp]

theorem CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom {J : Type u₁} {K : Type u₂} [Category.{v₁, u₁} J] [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [HasColimitsOfShape K C] (G : Functor J (Functor K C)) [HasLimit G] : (colimitLimitToLimitColimitCone G).hom = CategoryStruct.comp (colim.map (limitIsoSwapCompLim G).hom) (CategoryStruct.comp (colimitLimitToLimitColimit (uncurry.obj G)) (lim.map (whiskerRight (currying.unitIso.app G).inv colim)))