shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app

English

Special case with negation in both sides; the inv component satisfies a shifted version of the previous relation.

Русский

Специальный случай с отрицанием слева и справа; inv-элемент удовлетворяет сдвинутой версией предыдущего соотношения.

LaTeX

$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C (-n) n (\\mathrm{neg_add_cancel} n)).inv.app X) = ((\\mathrm{shiftFunctorCompIsoId} \\ C n (-n) (\\mathrm{add_neg_cancel} n)).inv.app (X⟦-n⟧)) $$$

Lean4

theorem shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X)⟦-n⟧' =
      (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).hom.app (X⟦-n⟧) :=
  by apply shift_shiftFunctorCompIsoId_hom_app

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