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) : x = 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} : x = y ↔ ∀ (k : K), limit.π (G.obj j) k x = limit.π (G.obj j) k y

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] : Function.Injective (colimitLimitToLimitColimit F)

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] : Function.Surjective (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 u₁} {K : Type u₂} [SmallCategory J] [Category.{v₂, u₂} K] [Small.{v, u₂} K] [FinCategory J] (F : Functor (J × K) (Type v)) [IsFiltered K] : IsIso (colimitLimitToLimitColimit F)

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))) : IsIso (colimitLimitToLimitColimitCone F)

instance CategoryTheory.Limits.filtered_colim_preservesFiniteLimits_of_types {K : Type u₂} [Category.{v₂, u₂} K] [Small.{v, u₂} K] [IsFiltered K] : PreservesFiniteLimits colim

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)] : PreservesLimitsOfShape J colim

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] : PreservesFiniteLimits colim

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)) : colimit (limit F) ≅ limit (colimit F.flip)

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.

@[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)