English
Inverse of the swapped-colimit is compatible with injections in the swapped and original orders
Русский
Обратное переставленной колимиты совместимо с инъекциями в переставленном и исходном порядках
LaTeX
$$$\\text{colimit}.\\iota _ k \\; \\gg \\; \\text{colimit}.\\iota (\\mathrm{curry.obj } G \\gg\\; \\mathrm{colim}) j \\; \\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}$$$
Lean4
@[simp]
theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv {j} {k} :
colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv =
(colimit.ι _ j ≫ colimit.ι (curry.obj _ ⋙ colim) k : _ ⟶ colimit (curry.obj (Prod.swap K J ⋙ G) ⋙ colim)) :=
by
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
slice_lhs 1 3 => simp only []
rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.isoOfEquivalence_inv_π]
dsimp [Equivalence.counitInv]
rw [CategoryTheory.Bifunctor.map_id]
simp
