English
The totalShift1Iso is an isomorphism between the total complex of the shifted bicomplex and the shifted total complex, with explicit description on components.
Русский
Изоморфизм totalShift1Iso — это изоморфизм между общим комплексом смещённого бикомплекса и смещённым общим комплексом, с явным описанием компонент.
LaTeX
$$$\\text{totalShift₁Iso} : ((\\text{shiftFunctor}_1 C x).obj K).total (up \\mathbb{Z}) \\cong (K.total (up \\mathbb{Z}))⟦x⟧$$$
Lean4
/-- The isomorphism `((shiftFunctor₁ C x).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦x⟧`
expressing the compatibility of the total complex with the shift on the first indices.
This isomorphism does not involve signs. -/
noncomputable def totalShift₁Iso : ((shiftFunctor₁ C x).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦x⟧ :=
HomologicalComplex.Hom.isoOfComponents (fun n => K.totalShift₁XIso x n (n + x) 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 x n n' _ _ rfl rfl, K.D₂_totalShift₁XIso_hom x n n' _ _ rfl rfl])
