English
The compatibility of the total complex with shifts in both variables commutes only up to a sign, namely (x*y).negOnePow. In particular, compositions that should be the same differ by this sign.
Русский
Согласование полного комплекса сдвигов в обеих переменных совпадает только до знака (−1)^{xy}. Конкретно, две композиции, которые должны совпадать, отличаются знаком.
LaTeX
$$$((\mathrm{shift}_2\ C\ y).\mathrm{obj} K).{\text{totalShift}}_1^x \;\;\; ≪≫ \;\; (x \cdot y).\mathrm{negOnePow} \; \cdot \; \big(\mathrm{total.mapIso}( (\mathrm{shiftFunctor}_1\_2\mathrm{CommIso}\ C x y).app K) (up\ Z) \; ≪≫ \; ((\mathrm{shift}_1\ C\ x).\mathrm{obj} K).\mathrm{totalShift}_2^y
\; ≪≫ \; (\mathrm{shift}_\mathrm{functor}(\mathrm{CochainComplex}\ C\ \Z) x).mapIso (K.\mathrm{totalShift}_1^{} x) \big)$$$$
Lean4
/-- The compatibility isomorphisms of the total complex with the shifts
in both variables "commute" only up to a sign `(x * y).negOnePow`. -/
theorem totalShift₁Iso_trans_totalShift₂Iso :
((shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫ (shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) =
(x * y).negOnePow •
(total.mapIso ((shiftFunctor₁₂CommIso C x y).app K) (up ℤ)) ≪≫
((shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫
(shiftFunctor _ y).mapIso (K.totalShift₁Iso x) ≪≫ (shiftFunctorComm (CochainComplex C ℤ) x y).app _ :=
by
ext n n₁ n₂ h
dsimp at h ⊢
rw [Linear.comp_units_smul, ι_totalShift₁Iso_hom_f_assoc _ x n₁ n₂ n h _ rfl _ rfl, ιTotal_map_assoc,
ι_totalShift₂Iso_hom_f_assoc _ y n₁ n₂ n h _ rfl _ rfl, Linear.units_smul_comp, Linear.comp_units_smul]
dsimp [shiftFunctor₁₂CommIso]
rw [id_comp, id_comp, id_comp, id_comp, comp_id,
ι_totalShift₂Iso_hom_f _ y (n₁ + x) n₂ (n + x) (by cutsat) _ rfl _ rfl, smul_smul, ← Int.negOnePow_add, add_mul,
add_comm (x * y)]
dsimp
rw [id_comp, comp_id, ι_totalShift₁Iso_hom_f_assoc _ x n₁ (n₂ + y) (n + y) (by cutsat) _ rfl (n + x + y) (by cutsat),
CochainComplex.shiftFunctorComm_hom_app_f]
dsimp
rw [Iso.inv_hom_id, comp_id, id_comp]
