English
Compatibility of the interchange isomorphism with the π-maps is expressed by the relation: colimit.ι _ (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom = colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j
Русский
Согласованность перестановки колимит с отображениями проекции π выражается равенством: колимит.ι_(j,k) затем гом-образ через изоморфизм равняется колимит.ι_k затем колимит.ι по curry(obj G) ⋙ colim на j
LaTeX
$$$\\text{colimit}.\\iota _ (j,k) \\; \\gg \\; (\\text{colimitIsoColimitCurryCompColim } G)^{\\mathrm{hom}} = \\text{colimit}.\\iota _ k \\; \\gg \\; \\text{colimit}.\\iota (\\mathrm{curry.obj } G \\;\\gg\\; \\mathrm{colim}) j$$$
Lean4
@[simp]
theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} :
(limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ limit.π _ j ≫ limit.π _ k = (limit.π _ k ≫ limit.π _ j) :=
by
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim, Equivalence.counit]
rw [Category.assoc, Category.assoc, limitIsoLimitCurryCompLim_hom_π_π, HasLimit.isoOfEquivalence_hom_π]
dsimp [Equivalence.counit]
rw [← prod_id, G.map_id]
simp
