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'}
:
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 (Prod.mkHom f (CategoryStruct.id k)) = ((Functor.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]
:
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_π
{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.ι ((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim) k)
(CategoryStruct.comp (colimitLimitToLimitColimit F) (limit.π ((Functor.curry.obj F).comp colim) j)) = CategoryStruct.comp (limit.π ((Functor.curry.obj ((Prod.swap K J).comp F)).obj k) j)
(colimit.ι ((Functor.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 ((Functor.curry.obj F).obj j) ⟶ Z)
:
CategoryStruct.comp (colimit.ι ((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim) k)
(CategoryStruct.comp (colimitLimitToLimitColimit F)
(CategoryStruct.comp (limit.π ((Functor.curry.obj F).comp colim) j) h)) = CategoryStruct.comp (limit.π ((Functor.curry.obj ((Prod.swap K J).comp F)).obj k) j)
(CategoryStruct.comp (colimit.ι ((Functor.curry.obj F).obj j) k) h)
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₂}
[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 : ((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim).obj k)
:
limit.π ((Functor.curry.obj F).comp colim) j
(colimitLimitToLimitColimit F (colimit.ι ((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim) k f)) = colimit.ι ((Functor.curry.obj F).obj j) k (limit.π ((Functor.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]
:
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
@[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]
: