CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π

theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj F).comp CategoryTheory.Limits.colim) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k)

This theorem, `CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π`, characterizes a morphism from a colimit to a limit in category theory. Given a functor `F` from the cartesian product of categories `J` and `K` to a category `C`, which has both limits of shape `J` and colimits of shape `K`, for any objects `j` in `J` and `k` in `K`, the composition of the coprojection from a value of the functor to the colimit object, the morphism `colimitLimitToLimitColimit F`, and the projection from the limit object to a value of functor, is equal to the composition of the projection from the limit object to a value of functor, and the coprojection from a value of the functor to the colimit object. The proof has been omitted for brevity.

More concisely: Given a functor between cartesian products of categories with both limit and colimit, the composition of the morphism from a value of the functor to the colimit object, followed by the morphism from the limit object to the value, equals the morphism from the limit object to the value, followed by the morphism from the value to the colimit object.