English
The isomorphism of shifted short complex functors is realized by a canonical composition of shift functors.
Русский
Изоморфизм сдвинутых функторов реализуется канонической композицией сдвигов.
LaTeX
$$$ (shiftShortComplexFunctorIso\\; C\\; mn\\; a\\; a'').hom.app K = (shortComplexFunctor C (ComplexShape.up \\mathbb{Z}) a).map (shiftFunctorAdd'(F,C)...) \\circ \\cdots $$$
Lean4
theorem shiftShortComplexFunctorIso_add'_hom_app (n m mn : ℤ) (hmn : m + n = mn) (a a' a'' : ℤ) (ha' : n + a = a')
(ha'' : m + a' = a'') (K : CochainComplex C ℤ) :
(shiftShortComplexFunctorIso C mn a a'' (by rw [← ha'', ← ha', ← add_assoc, hmn])).hom.app K =
(shortComplexFunctor C (ComplexShape.up ℤ) a).map
((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
(shiftShortComplexFunctorIso C n a a' ha').hom.app (K⟦m⟧) ≫
(shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K :=
by
ext <;> dsimp <;>
simp only [← hmn, Int.negOnePow_add, shiftFunctorAdd'_hom_app_f', XIsoOfEq_shift, Linear.comp_units_smul,
Linear.units_smul_comp, XIsoOfEq_hom_comp_XIsoOfEq_hom, smul_smul]
