English
There is an isomorphism between colimits after swapping the order, and the inverse is compatible with injections in the swapped and original orders
Русский
Существует изоморфизм между колимитами после смены порядка, а его обратная сторона согласуется с инъекциями в переставленном и исходном порядках
LaTeX
$$$\\text{colimit}.\\iota _ k \\; \\gg \\; \\text{colimit}.\\iota (\\mathrm{G})\\; \\gg \\; (\\text{colimitCurrySwapCompColimIsoColimitCurryCompColim } G)^{\\mathrm{inv}} = \\text{colimit}.\\iota _ j \\; \\gg \\; \\text{colimit}.\\iota (\\mathrm{curry.obj } (\\mathrm{Prod.swap } K J \\;\\gg\\; G) \\;\\gg\\; \\mathrm{colim}) k$$
Lean4
/-- A variant of the Fubini theorem for a functor `G : J × K ⥤ C`,
showing that $\colim_k \colim_j G(j,k) ≅ \colim_j \colim_k G(j,k)$.
-/
noncomputable def colimitCurrySwapCompColimIsoColimitCurryCompColim :
colimit (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) ≅ colimit (curry.obj G ⋙ colim) :=
calc
colimit (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) ≅ colimit (Prod.swap K J ⋙ G) :=
(colimitIsoColimitCurryCompColim _).symm
_ ≅ colimit G := (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl _))
_ ≅ colimit (curry.obj G ⋙ colim) := colimitIsoColimitCurryCompColim _
