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_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.

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

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))) : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimitCone F)

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Limits.filteredColimPreservesFiniteLimits {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {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

Equations

• CategoryTheory.Limits.filteredColimPreservesFiniteLimits = CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves CategoryTheory.Limits.colim (CategoryTheory.forget C)

noncomputable instance CategoryTheory.Limits.instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape K C] [(CategoryTheory.forget C).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.colimitLimitIso {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {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 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_π_assoc {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {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 F.flip).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 F.flip) b) h)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F.flip a).app b) h)

@[simp]

theorem CategoryTheory.Limits.ι_colimitLimitIso_limit_π {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {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 F.flip) b)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) ((CategoryTheory.Limits.colimit.ι F.flip a).app b)