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 v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))} (x : (CategoryTheory.Functor.comp G CategoryTheory.Limits.lim).obj j) (y : (CategoryTheory.Functor.comp G CategoryTheory.Limits.lim).obj j) (w : ∀ (k : K), CategoryTheory.Limits.limit.π K inst✝ (Type v) CategoryTheory.types (G.obj j) (_ : CategoryTheory.Limits.HasLimit (G.obj j)) k x = CategoryTheory.Limits.limit.π K inst✝ (Type v) CategoryTheory.types (G.obj j) (_ : CategoryTheory.Limits.HasLimit (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 v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] [Finite J] : Function.Injective (CategoryTheory.Limits.colimitLimitToLimitColimit F)

This follows this proof from

• Borceux, Handbook of categorical algebra 1, Theorem 2.13.4

theorem CategoryTheory.Limits.colimitLimitToLimitColimit_surjective {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] : Function.Surjective (CategoryTheory.Limits.colimitLimitToLimitColimit F)

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 v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimit F)

instance CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))) : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimitCone F)

noncomputable instance CategoryTheory.Limits.filteredColimPreservesFiniteLimitsOfTypes {K : Type v} [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

noncomputable instance CategoryTheory.Limits.filteredColimPreservesFiniteLimits {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim

noncomputable instance CategoryTheory.Limits.instPreservesFiniteLimitsFunctorCategoryColim {K : Type v} [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget C)] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

noncomputable def CategoryTheory.Limits.colimitLimitIso {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit (CategoryTheory.Functor.flip F))

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

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J) {Z : C} (h : (CategoryTheory.Limits.colimit (CategoryTheory.Functor.flip F)).obj b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit (CategoryTheory.Functor.flip F)) b) h)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.flip F) a).app b) h)

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitIso_limit_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] [CategoryTheory.IsFiltered K] [CategoryTheory.FinCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit (CategoryTheory.Functor.flip F)) b)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) ((CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.flip F) a).app b)