The morphism comparing a colimit of limits with the corresponding limit of colimits. #
In this file, we introduce morphisms which allow to study the commutation of limits with colimits.
In the case of an uncurried functor F : J × K ⥤ C there is always a
morphism $\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$ (see colimitLimitToLimitColimit).
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".
We also study the case of curried bifunctors F : J ⥤ K ⥤ C. In this case,
we define a morphism colimitLimToLimitColim : colimit (F.flip ⋙ lim) ⟶ limit (F ⋙ colim).
We show that this morphism is an isomorphism iff lim : (J ⥤ C) ⥤ C preserves the
colimit of F.flip, and this is also equivalent to saying that colim : (K ⥤ C) ⥤ C
preserves the limit of F. In particular, lim : (J ⥤ C) ⥤ C preserves colimits
of shape K iff colim : (K ⥤ C) ⥤ C preserves limits of shape J.
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₂}
[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]
{C : Type u}
[Category.{v, u} C]
(F : Functor (J × K) C)
[HasLimitsOfShape J C]
[HasColimitsOfShape K C]
(j : J)
(k : K)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : carrier (((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim).obj k))
:
(ConcreteCategory.hom (limit.π ((Functor.curry.obj F).comp colim) j))
((ConcreteCategory.hom (colimitLimitToLimitColimit F))
((ConcreteCategory.hom (colimit.ι ((Functor.curry.obj ((Prod.swap K J).comp F)).comp lim) k)) x)) = (ConcreteCategory.hom (colimit.ι ((Functor.curry.obj F).obj j) k))
((ConcreteCategory.hom (limit.π ((Functor.curry.obj ((Prod.swap K J).comp F)).obj k) j)) x)
Since colimit_limit_to_limit_colimit is a morphism from a colimit to a limit,
this lemma characterises it.
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]
:
@[implicit_reducible]
noncomputable def
CategoryTheory.Limits.colim.coconeFlip
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
(F : Functor J (Functor K C))
:
Given a bifunctor F : J ⥤ K ⥤ C, and assuming that C as colimits of shape K,
this is the cocone of F.flip with point F ⋙ colim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.colim.coconeFlip_ι_app_app
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
(F : Functor J (Functor K C))
(k : K)
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.colim.coconeFlip_pt
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
(F : Functor J (Functor K C))
:
noncomputable def
CategoryTheory.Limits.colim.isColimitCoconeFlip
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
(F : Functor J (Functor K C))
:
IsColimit (coconeFlip F)
Given a bifunctor F : J ⥤ K ⥤ C, and assuming that C has colimits of shape K,
the colimit of F.flip is F ⋙ colim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable def
CategoryTheory.Limits.lim.cone
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
Cone F
Given a bifunctor F : J ⥤ K ⥤ C, and assuming that C has limits of shape J,
this is the cone of F with point F.flip ⋙ lim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.lim.cone_pt
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
@[simp]
theorem
CategoryTheory.Limits.lim.cone_π_app_app
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
(j : J)
(k : K)
:
noncomputable def
CategoryTheory.Limits.lim.isLimitCone
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
Given a bifunctor F : J ⥤ K ⥤ C, and assuming that C has limits of shape J,
the limit of F is F.flip ⋙ lim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.colimitLimToLimitColim
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
Given a bifunctor F : J ⥤ K ⥤ C, and assuming that C has limits of shape J and
colimit of shape K, this is the canonical morphism from the colimit of F.flip ⋙ lim
to the limit of F ⋙ colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_colimitToLimit_π
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
(j : J)
(k : K)
:
CategoryStruct.comp (colimit.ι (F.flip.comp lim) k)
(CategoryStruct.comp (colimitLimToLimitColim F) (limit.π (F.comp colim) j)) = CategoryStruct.comp (limit.π (F.flip.obj k) j) (colimit.ι (F.obj j) k)
@[simp]
theorem
CategoryTheory.Limits.ι_colimitToLimit_π_assoc
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
(j : J)
(k : K)
{Z : C}
(h : colim.obj (F.obj j) ⟶ Z)
:
CategoryStruct.comp (colimit.ι (F.flip.comp lim) k)
(CategoryStruct.comp (colimitLimToLimitColim F) (CategoryStruct.comp (limit.π (F.comp colim) j) h)) = CategoryStruct.comp (limit.π (F.flip.obj k) j) (CategoryStruct.comp (colimit.ι (F.obj j) k) h)
theorem
CategoryTheory.Limits.colimitLimToLimitColim_eq_colimit_desc
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
theorem
CategoryTheory.Limits.colimitLimToLimitColim_eq_limit_lift
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
theorem
CategoryTheory.Limits.isIso_colimitLimToLimitColim_iff_preservesColimit
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
theorem
CategoryTheory.Limits.isIso_colimitLimToLimitColim_iff_preservesLimit
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
theorem
CategoryTheory.Limits.preservesColimit_flip_lim_iff_preservesLimit_colim
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor J (Functor K C))
:
theorem
CategoryTheory.Limits.preservesColimit_lim_iff_preservesLimit_colim
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
{C : Type u}
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
(F : Functor K (Functor J C))
:
theorem
CategoryTheory.Limits.preservesColimitsOfShape_lim_iff_preservesLimitsOfShape_colim
(J : Type u₁)
(K : Type u₂)
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
(C : Type u)
[Category.{v, u} C]
[HasColimitsOfShape K C]
[HasLimitsOfShape J C]
: