English
Let G : J × K ⥤ C be a functor for which the relevant colimits exist. Then the canonical comparison between the iterated colimits and the colimit over the product commutes with the injection maps; in particular the two-step injections into the iterated colimit coincide with the single injection into the joint colimit via the canonical isomorphism
Русский
Пусть G : J × K ⥤ C – это функция, для которой существуют нужные колимиты. Тогда каноническое сравнение между последовательными колимитами и колимитой над произведением приводят к совместимости с инъекциями; в частности два последовательных вкола в получившийся колимит совпадают с единичной инъекцией в общий колимит через каноническое изоморечение
LaTeX
$$$\\text{colimit}.\\iota((\\mathrm{curry.obj}\\ G).\\mathrm{obj}\\ j)\\,k \\; \\gg \\; \\text{colimit}.\\iota(\\mathrm{curry.obj}\\ G \\;\\gg\\; \\mathrm{colim})\\ j \\; \\gg \\; (\\text{colimitIsoColimitCurryCompColim } G)^{-1} = \\text{colimit}.\\iota _ {(j,k)}$$$
Lean4
@[simp, reassoc]
theorem colimitIsoColimitCurryCompColim_ι_ι_inv {j} {k} :
colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv =
colimit.ι _ (j, k) :=
by simp [colimitIsoColimitCurryCompColim, Trans.simple, colimitUncurryIsoColimitCompColim]
