English
There is an isomorphism of triangles between the rotated triangle of a degreewise split cochain complex and the usual mapping cone triangle of homOfDegreewiseSplit.
Русский
Существует изоморфизм треугольников между повёрнутым треугольником степень-распределённого сложного коцепана и обычным треугольником отображающего коня для homOfDegreewiseSplit.
LaTeX
$$$(\triangle h φ).rotate \simeq \triangle hOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ)$$$
Lean4
/-- The canonical isomorphism of triangles
`(triangleOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangle (homOfDegreewiseSplit S σ)`
when `S` is a degreewise split short exact sequence of cochain complexes. -/
noncomputable def triangleOfDegreewiseSplitRotateRotateIso :
(triangleOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangle (homOfDegreewiseSplit S σ) :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (mappingConeHomOfDegreewiseSplitIso S σ).symm
(by dsimp; simp only [comp_id, id_comp])
(by dsimp; simp only [neg_comp, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, neg_neg, id_comp])
(by dsimp;
simp only [CategoryTheory.Functor.map_id, comp_id, mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃])
