English
In a degreewise split short exact sequence of cochain complexes, the triangle obtained by triangleRotateShortComplexSplitting is compatible with the standard triangle of the mapping cone.
Русский
В короткой последовательности из степеней с разложением треугольник, полученный из triangleRotateShortComplexSplitting, согласован с обычным треугольником отображающего коня.
LaTeX
$$$\text{triangleRotateShortComplexSplitting}\; φ \; \Rightarrow \text{triangle compatibility with mapping cone triangle}$$$
Lean4
/-- The canonical isomorphism between `(trianglehOfDegreewiseSplit S σ).rotate.rotate` and
`mappingCone.triangleh (homOfDegreewiseSplit S σ)` when `S` is a degreewise split
short exact sequence of cochain complexes. -/
noncomputable def trianglehOfDegreewiseSplitRotateRotateIso :
(trianglehOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangleh (homOfDegreewiseSplit S σ) :=
(rotate _).mapIso ((HomotopyCategory.quotient _ _).mapTriangleRotateIso.app _) ≪≫
(HomotopyCategory.quotient _ _).mapTriangleRotateIso.app _ ≪≫
(HomotopyCategory.quotient _ _).mapTriangle.mapIso (triangleOfDegreewiseSplitRotateRotateIso S σ)
