English
The mor3 component of the mappingConeCompTriangle is natural with respect to φ: for φ: mk2 f g → mk2 f' g', a certain equality of composites holds.
Русский
Компонента mor3 треугольника mappingConeCompTriangle диагонально естественна по отношению к φ: для φ: mk2 f g → mk2 f' g' выполняется тождество композиции.
LaTeX
$$$\forall X_1,X_2,X_3,Y_1,Y_2,Y_3, f,g, f',g',\; \phi,\; \text{mor}_3(\cdot)\text{nat}$$$
Lean4
/-- Given two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` in the category
of cochain complexes, this is the canonical triangle
`mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧`
in the homotopy category. It is a distinguished triangle,
see `HomotopyCategory.mappingConeCompTriangleh_distinguished`. -/
noncomputable def mappingConeCompTriangleh : Triangle (HomotopyCategory C (ComplexShape.up ℤ)) :=
(HomotopyCategory.quotient _ _).mapTriangle.obj (mappingConeCompTriangle f g)
