English
There is a canonical isomorphism between the mapped cone triangles: mapTrianglehIso φ G: (G.mapHomotopyCategory (up ℤ)).mapTriangle.obj (triangle φ) ≅ triangleh ((G.mapHomologicalComplex (up ℤ)).map φ).
Русский
Существует каноническое изоморфизм между отображенными треугольниками конуса: mapTrianglehIso φ G: (G.mapHomotopyCategory (up ℤ)).mapTriangle.obj (triangle φ) ≅ triangleh ((G.mapHomologicalComplex (up ℤ)).map φ).
LaTeX
$$$ (G.mapHomotopyCategory (ComplexShape.up \\mathbb{Z})).mapTriangle.obj (triangle \\phi) \\cong triangleh ((G.mapHomologicalComplex (ComplexShape.up \\mathbb{Z})).map \\phi) $$$
Lean4
/-- A triangle in `HomotopyCategory C (ComplexShape.up ℤ)` is distinguished if it is isomorphic to
the triangle `CochainComplex.mappingCone.triangleh φ` for some morphism of cochain
complexes `φ`. -/
def distinguishedTriangles : Set (Triangle (HomotopyCategory C (ComplexShape.up ℤ))) := fun T =>
∃ (X Y : CochainComplex C ℤ) (φ : X ⟶ Y), Nonempty (T ≅ CochainComplex.mappingCone.triangleh φ)
