# 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 #

theorem CategoryTheory.Limits.comp_lim_obj_ext {J : Type u₁} {K : Type u₂} [] [] [] {j : J} {G : } (x : (G.comp CategoryTheory.Limits.lim).obj j) (y : (G.comp CategoryTheory.Limits.lim).obj j) (w : ∀ (k : K), CategoryTheory.Limits.limit.π (G.obj j) k x = CategoryTheory.Limits.limit.π (G.obj j) k y) :
x = y

(G ⋙ lim).obj j = limit (G.obj j) definitionally, so this is just a variant of limit_ext'.

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₂} [] [] [] (F : CategoryTheory.Functor (J × K) (Type v)) [] :

This follows this proof from

• Borceux, Handbook of categorical algebra 1, Theorem 2.13.4

This follows this proof from

• Borceux, Handbook of categorical algebra 1, Theorem 2.13.4 although with different names.
Equations
• =
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance CategoryTheory.Limits.filteredColimPreservesFiniteLimits {J : Type u₁} {K : Type u₂} [] [] {C : Type u} :
CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
Equations
Equations
• One or more equations did not get rendered due to their size.

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_π_assoc {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : ) (a : K) (b : J) {Z : C} (h : ().obj b Z) :
@[simp]
theorem CategoryTheory.Limits.ι_colimitLimitIso_limit_π {J : Type u₁} {K : Type u₂} [] [] {C : Type u} (F : ) (a : K) (b : J) :