shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app

English

The add'-inversion identity for shifts yields an inv.app equality expressing the compatibility of inverses in nested shifts.

Русский

Идентичность обратного для add' смещений даёт равенство inv.app, отражающее совместимость обратных внутри вложенных сдвигов.

LaTeX

$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C p' p hp).inv.app X) = ((\\mathrm{shiftFunctorCompIsoId} \\ C n' n hn).inv.app X) \\\\gg ((\\mathrm{shiftFunctorCompIsoId} \\ C m' m hm).inv.app (X⟦n'⟧)) \\\\gg ((\\mathrm{shiftFunctorAdd'} \\ C m n p h).inv.app (X⟦n'⟧⟦m'⟧)) $$$

Lean4

theorem shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).inv.app X)⟦-n⟧' =
      (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X⟦-n⟧) :=
  by apply shift_shiftFunctorCompIsoId_inv_app

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