English
Let φ be a morphism between cochain complexes. The rotated mapping-cone triangle (triangle φ).rotate is isomorphic to the degreewise-split triangle built from the short complex splitting triangleRotateShortComplexSplitting φ.
Русский
Пусть φ — морфизм между когейн-комплексами. Повёрнутый треугольник отображения (triangle φ).rotate изоморфен треугольнику, полученному степенным образом разложенной кратности короткого комплекса: triangleOfDegreewiseSplit с указанным разложением triangleRotateShortComplexSplitting φ.
LaTeX
$$$ (\triangle φ).rotate \cong \triangleOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ) $$$
Lean4
/-- The triangle `(triangle φ).rotate` is isomorphic to a triangle attached to a
degreewise split short exact sequence of cochain complexes. -/
noncomputable def triangleRotateIsoTriangleOfDegreewiseSplit :
(triangle φ).rotate ≅ triangleOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ) :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) (by ext; simp)
