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

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_π_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.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim).obj k) :
    CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj F) CategoryTheory.Limits.colim) j (CategoryTheory.Limits.colimitLimitToLimitColimit F (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) F)) CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) 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