Documentation

Mathlib.CategoryTheory.Limits.ColimitLimit

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₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} 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.map (CategoryTheory.CategoryStruct.id j, f) = ((CategoryTheory.curry.obj F).obj j).map f
theorem CategoryTheory.Limits.map_id_right_eq_curry_swap_map {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} 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.map (f, CategoryTheory.CategoryStruct.id k) = ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k).map f
noncomputable def CategoryTheory.Limits.colimitLimitToLimitColimit {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} 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.curry.obj ((CategoryTheory.Prod.swap K J).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₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} 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.obj ((CategoryTheory.curry.obj F).obj j) Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (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 ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k) h)
    @[simp]

    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₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₁} J] [Small.{v, u₂} K] (F : CategoryTheory.Functor (J × K) (Type v)) (j : J) (k : K) (f : ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).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 ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j f)

    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