limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π

English

There is a natural isomorphism between the limit of the swapped G and the limit of G with respect to the outer curry, reflecting the symmetry of taking limits in J and K

Русский

Существует естественный изоморфизм между пределом переставленного G и пределом G по внешнему curry, отражающий симметрию взятия пределов по индексам J и K

LaTeX

$$$\\text{limit}\\bigl(\\mathrm{curry.obj}(\\mathrm{Prod.swap}\\ K\\ J \\;\\gg\\; G) \\gg\\; \\mathrm{lim}\\bigr) \\cong \\text{limit}\\bigl(\\mathrm{curry.obj} G \\gg\\; \\mathrm{lim}\\bigr)$$$

Lean4

@[simp]
theorem limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {j} {k} :
    (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫ limit.π _ k ≫ limit.π _ j = (limit.π _ j ≫ limit.π _ k) := by
  simp [limitCurrySwapCompLimIsoLimitCurryCompLim]

Похожие утверждения