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 category_theory.limits.filtered_colimit_commutes_finite_limit,
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
category_theory.limits.map_id_left_eq_curry_map
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J × K ⥤ C)
{j : J}
{k k' : K}
{f : k ⟶ k'} :
theorem
category_theory.limits.map_id_right_eq_curry_swap_map
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J × K ⥤ C)
{j j' : J}
{f : j ⟶ j'}
{k : K} :
F.map (f, 𝟙 k) = ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k).map f
def
category_theory.limits.colimit_limit_to_limit_colimit
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J × K ⥤ C)
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C] :
The universal morphism $\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$.
Equations
- category_theory.limits.colimit_limit_to_limit_colimit F = category_theory.limits.limit.lift (category_theory.curry.obj F ⋙ category_theory.limits.colim) {X := (category_theory.limits.colimit.cocone (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim)).X, π := {app := λ (j : J), category_theory.limits.colimit.desc (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) {X := (category_theory.limits.colimit.cocone ((category_theory.curry.obj F).obj j)).X, ι := {app := λ (k : K), category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j ≫ category_theory.limits.colimit.ι ((category_theory.curry.obj F).obj j) k, naturality' := _}}, naturality' := _}}
@[simp]
theorem
category_theory.limits.ι_colimit_limit_to_limit_colimit_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J × K ⥤ C)
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
(j : J)
(k : K) :
category_theory.limits.colimit.ι (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) k ≫ category_theory.limits.colimit_limit_to_limit_colimit F ≫ category_theory.limits.limit.π (category_theory.curry.obj F ⋙ category_theory.limits.colim) j = category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j ≫ category_theory.limits.colimit.ι ((category_theory.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
category_theory.limits.ι_colimit_limit_to_limit_colimit_π_apply
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
(F : J × K ⥤ Type v)
(j : J)
(k : K)
(f : (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim).obj k) :
category_theory.limits.limit.π (category_theory.curry.obj F ⋙ category_theory.limits.colim) j (category_theory.limits.colimit_limit_to_limit_colimit F (category_theory.limits.colimit.ι (category_theory.curry.obj (category_theory.prod.swap K J ⋙ F) ⋙ category_theory.limits.lim) k f)) = category_theory.limits.colimit.ι ((category_theory.curry.obj F).obj j) k (category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ F)).obj k) j f)