shiftShortComplexFunctorIso_zero_add_hom_app

English

There is a canonical isomorphism relating the shift of a short complex to another short complex obtained by shifting indices, with explicit homology-compatible components.

Русский

Существует каноническая изоморфия между сдвигом короткого комплекса и другим коротким комплексом, полученным путём сдвига индексов, с явными компонентами, совместимыми с гомологией.

LaTeX

$$$ (\\mathrm{shiftShortComplexFunctorIso} C n i i' ha ha') \\;:\\; (n,i,i')$ satisfying $n+i=i'$, etc., with hom-app equality as in the lemma.$$

Lean4

theorem shiftShortComplexFunctorIso_zero_add_hom_app (a : ℤ) (K : CochainComplex C ℤ) :
    (shiftShortComplexFunctorIso C 0 a a (zero_add a)).hom.app K =
      (shortComplexFunctor C (ComplexShape.up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K) :=
  by ext <;> simp [one_smul, shiftFunctorZero_hom_app_f]

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