English
There is a canonical isomorphism between the total complex of a bicomplex shifted in the second index and the total of the shifted bicomplex; the isomorphism is explicit on components and respects the total structure.
Русский
Существет канонический изоморфизм между общим комплексом бикомплекса, сдвинутого во втором индексе, и общим комплексом после сдвига; изоморфизм явен по компонентам и сохраняет общую структуру.
LaTeX
$$$\\text{totalShift₂Iso} : ((\\text{shiftFunctor₂ C y}.obj K).total (up \\mathbb{Z})) \\cong (K.total (up \\mathbb{Z}))⟦y⟧$$$
Lean4
/-- The isomorphism `((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧`
expressing the compatibility of the total complex with the shift on the second indices.
This isomorphism involves signs: on the summand in degree `(p, q)` of `K`, it is given by the
multiplication by `(p * y).negOnePow`. -/
noncomputable def totalShift₂Iso : ((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧ :=
HomologicalComplex.Hom.isoOfComponents (fun n => K.totalShift₂XIso y n (n + y) rfl)
(fun n n' _ => by
dsimp
simp only [total_d, Preadditive.add_comp, Preadditive.comp_add, smul_add, Linear.comp_units_smul,
K.D₁_totalShift₂XIso_hom y n n' _ _ rfl rfl, K.D₂_totalShift₂XIso_hom y n n' _ _ rfl rfl])
