English
For all j ∈ J and k ∈ K, the hom component of the interchange is compatible with the injections: colimit.ι _ (j, k) followed by the isomorphism’s hom equals the composite colimit.ι _ k followed by colimit.ι (curry.obj G ⋙ colim) j
Русский
Для всех j∈J и k∈K гом-компонента перестановочного изоморфизма совместима с инъекциями: колимитная инъекция по (j,k) далее гом-часть изоморфизма равна композиции колимитной инъекции по k затем инъекции по j для curry(G)
LaTeX
$$$\\text{colimit}.\\iota _ (j,k) \\; \\gg \\; (\\text{colimitIsoColimitCurryCompColim } G)^{\\mathrm{hom}} = \\bigl(\\text{colimit}.\\iota _ k \\; \\gg \\; \\text{colimit}.\\iota (\\mathrm{curry.obj } G \\;\\gg\\; \\mathrm{colim}) j\\bigr)$$$
Lean4
@[simp, reassoc]
theorem colimitIsoColimitCurryCompColim_ι_hom {j} {k} :
colimit.ι _ (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom =
(colimit.ι (_) k ≫ colimit.ι (curry.obj G ⋙ colim) j : _ ⟶ colimit (_ ⋙ colim)) :=
by
rw [← cancel_mono (colimitIsoColimitCurryCompColim G).inv]
simp
