Filtered colimits commute with finite limits. #
We show that for a functor F : J × K ⥤ Type v, when J is finite and K is filtered,
the universal morphism colimitLimitToLimitColimit F comparing the
colimit (over K) of the limits (over J) with the limit of the colimits is an isomorphism.
(In fact, to prove that it is injective only requires that J has finitely many objects.)
References #
- Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
- Stacks: Filtered colimits
theorem
CategoryTheory.Limits.comp_lim_obj_ext
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
{j : J}
{G : Functor J (Functor K (Type v))}
(x y : (G.comp lim).obj j)
(w : ∀ (k : K), limit.π (G.obj j) k x = limit.π (G.obj j) k y)
:
(G ⋙ lim).obj j = limit (G.obj j) definitionally, so this
is just a variant of limit_ext'.
theorem
CategoryTheory.Limits.comp_lim_obj_ext_iff
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
{j : J}
{G : Functor J (Functor K (Type v))}
{x y : (G.comp lim).obj j}
:
Injectivity doesn't need that we have finitely many morphisms in J,
only that there are finitely many objects.
theorem
CategoryTheory.Limits.colimitLimitToLimitColimit_injective
{J : Type u₁}
{K : Type u₂}
[Category.{v₁, u₁} J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
(F : Functor (J × K) (Type v))
[IsFiltered K]
[Finite J]
:
This follows this proof from
- Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
theorem
CategoryTheory.Limits.colimitLimitToLimitColimit_surjective
{J : Type u₁}
{K : Type u₂}
[SmallCategory J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[FinCategory J]
(F : Functor (J × K) (Type v))
[IsFiltered K]
:
This follows this proof from Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
although with different names.
instance
CategoryTheory.Limits.colimitLimitToLimitColimit_isIso
{J : Type u₁}
{K : Type u₂}
[SmallCategory J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[FinCategory J]
(F : Functor (J × K) (Type v))
[IsFiltered K]
:
instance
CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso
{J : Type u₁}
{K : Type u₂}
[SmallCategory J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[FinCategory J]
[IsFiltered K]
(F : Functor J (Functor K (Type v)))
:
instance
CategoryTheory.Limits.filtered_colim_preservesFiniteLimits_of_types
{K : Type u₂}
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[IsFiltered K]
:
instance
CategoryTheory.Limits.filtered_colim_preservesFiniteLimits
{J : Type u₁}
{K : Type u₂}
[SmallCategory J]
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[FinCategory J]
[IsFiltered K]
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasLimitsOfShape J C]
[HasColimitsOfShape K C]
[ReflectsLimitsOfShape J (forget C)]
[PreservesColimitsOfShape K (forget C)]
[PreservesLimitsOfShape J (forget C)]
:
instance
CategoryTheory.Limits.instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget
{K : Type u₂}
[Category.{v₂, u₂} K]
[Small.{v, u₂} K]
[IsFiltered K]
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[PreservesFiniteLimits (forget C)]
[PreservesColimitsOfShape K (forget C)]
[HasFiniteLimits C]
[HasColimitsOfShape K C]
[(forget C).ReflectsIsomorphisms]
:
noncomputable def
CategoryTheory.Limits.colimitLimitIso
{C : Type u}
[Category.{v, u} C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
[HasLimitsOfShape J C]
[HasColimitsOfShape K C]
[PreservesLimitsOfShape J colim]
(F : Functor J (Functor K C))
:
A curried version of the fact that filtered colimits commute with finite limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_colimitLimitIso_limit_π
{C : Type u}
[Category.{v, u} C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
[HasLimitsOfShape J C]
[HasColimitsOfShape K C]
[PreservesLimitsOfShape J colim]
(F : Functor J (Functor K C))
(a : K)
(b : J)
:
CategoryStruct.comp (colimit.ι (limit F) a) (CategoryStruct.comp (colimitLimitIso F).hom (limit.π (colimit F.flip) b)) = CategoryStruct.comp ((limit.π F b).app a) ((colimit.ι F.flip a).app b)
@[simp]
theorem
CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc
{C : Type u}
[Category.{v, u} C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
[HasLimitsOfShape J C]
[HasColimitsOfShape K C]
[PreservesLimitsOfShape J colim]
(F : Functor J (Functor K C))
(a : K)
(b : J)
{Z : C}
(h : (colimit F.flip).obj b ⟶ Z)
:
CategoryStruct.comp (colimit.ι (limit F) a)
(CategoryStruct.comp (colimitLimitIso F).hom (CategoryStruct.comp (limit.π (colimit F.flip) b) h)) = CategoryStruct.comp ((limit.π F b).app a) (CategoryStruct.comp ((colimit.ι F.flip a).app b) h)