shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app

English

Special case of shift identities with -n and n; the hom component matches the previously established 'add_neg_cancel' symmetry between n and -n.

Русский

Особый случай с -n и n; гомкомпонента совпадает с симметрией add_neg_cancel между n и -n.

LaTeX

$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C n (-n) (\\mathrm{add_neg_cancel} n)).hom.app X)\\langle n \\rangle' = ((\\mathrm{shiftFunctorCompIsoId} \\ C (-n) n (\\mathrm{neg_add_cancel} n)).hom.app (X⟦n⟧)) $$$

Lean4

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

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