English
The hom components of the total-shift compatibility also satisfy a signed compatibility: the composed homs on one side equal the signed composition of the corresponding total maps and shift isomorphisms on the other side.
Русский
Гомоморфизмы согласованности полного сдвига также удовлетворяют знаковую согласованность: левая и правая части композиции гомоморфизмов совпадают с соответствующим подпроизведением из суммарных отображений и изоморфизмов сдвига.
LaTeX
$$$(((\mathrm{shift}_2\ C\ y).\obj K).\mathrm{totalShift}_1^x).\hom \;\; \big\circ (K.\mathrm{totalShift}_2^y).\hom\langle x\rangle' = (x \cdot y).\negOnePow \; \big(\mathrm{total.mapIso}( ((\mathrm{shiftFunctor}_1\_2\CommIso\ C x y).hom.app K) ) (up\ Z) \; ≫ (((\mathrm{shift}_1\ C\ x).\obj K).\mathrm{totalShift}_2^y).hom ≫ (K.\mathrm{totalShift}_1^x).hom\langle y\rangle' ≫ (\mathrm{shiftFunctorComm}(CochainComplex C \Z) x y).hom.app _ \big)$$$
Lean4
/-- The compatibility isomorphisms of the total complex with the shifts
in both variables "commute" only up to a sign `(x * y).negOnePow`. -/
@[reassoc]
theorem totalShift₁Iso_hom_totalShift₂Iso_hom :
(((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ≫ (K.totalShift₂Iso y).hom⟦x⟧' =
(x * y).negOnePow •
(total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (up ℤ) ≫
(((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom ≫
(K.totalShift₁Iso x).hom⟦y⟧' ≫ (shiftFunctorComm (CochainComplex C ℤ) x y).hom.app _) :=
congr_arg Iso.hom (totalShift₁Iso_trans_totalShift₂Iso K x y)
