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 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'} : F.toPrefunctor.map (CategoryTheory.CategoryStruct.id j, f) = ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.obj j).toPrefunctor.map f

theorem CategoryTheory.Limits.map_id_right_eq_curry_swap_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} {j' : J} {f : j ⟶ j'} {k : K} : F.toPrefunctor.map (f, CategoryTheory.CategoryStruct.id k) = ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)).toPrefunctor.obj k).toPrefunctor.map f

noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimit {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) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim) ⟶ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj F) 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.

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π {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) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj F) CategoryTheory.Limits.colim) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)).toPrefunctor.obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.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 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.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim).toPrefunctor.obj k) : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj F) CategoryTheory.Limits.colim) j (CategoryTheory.Limits.colimitLimitToLimitColimit F (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.obj j) k (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)).toPrefunctor.obj k) j f)

@[simp]

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

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