noncomputable def filteredColimit_finiteLimits_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit F.flip)

Filtered colimits commute with finite limits: the canonical comparison colim_K lim_J F ≅ lim_J colim_K F is an isomorphism under the hypothesis that the colimit functor preserves finite limits.

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

In the category of types, filtered colimits preserve finite limits.

noncomputable def filteredColimit_finiteLimits_iso_type {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] [CategoryTheory.Limits.HasLimitsOfShape J (Type v)] [CategoryTheory.Limits.HasColimitsOfShape K (Type v)] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))) : CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit F.flip)

Filtered-colimit-vs-finite-limit isomorphism specialized to types.

instance filteredColimit_preservesFiniteLimits_concrete {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] [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

In a concrete category compatible with the forgetful functor, filtered colimits commute with finite limits, generalizing the type-level statement.

theorem filteredColimit_finiteLimits_iso_components {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (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 (filteredColimit_finiteLimits_iso 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)

Explicit description of the filtered-colimit/finite-limit isomorphism on the cone components: colim.ι ≫ iso ≫ lim.π = lim.π ≫ colim.ι.