Documentation

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

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_iff {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))} {x : (G.comp CategoryTheory.Limits.lim).obj j} {y : (G.comp CategoryTheory.Limits.lim).obj j} :
x = y ∀ (k : K), CategoryTheory.Limits.limit.π (G.obj j) k x = CategoryTheory.Limits.limit.π (G.obj j) k y
theorem CategoryTheory.Limits.comp_lim_obj_ext {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))} (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.

This follows this proof from

  • Borceux, Handbook of categorical algebra 1, Theorem 2.13.4 although with different names.
Equations
  • One or more equations did not get rendered due to their size.