# mathlibdocumentation

category_theory.limits.filtered_colimit_commutes_finite_limit

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

Injectivity doesn't need that we have finitely many morphisms in J, only that there are finitely many objects.

theorem category_theory.limits.colimit_limit_to_limit_colimit_injective {J K : Type v} (F : J × K Type v) [fintype J] :

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.
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

A curried version of the fact that filtered colimits commute with finite limits.

Equations
@[simp]
@[simp]
theorem category_theory.limits.ι_colimit_limit_iso_limit_π_assoc {J K : Type v} {C : Type u} (F : J K C) (a : K) (b : J) {X' : C} (f' : X') :