English
Characterization of distinguished triangles in the derived category via isomorphism to cones of morphisms between shifted singleFunctors objects; equivalently, a triangle lies in distTriang if and only if it is isomorphic to one built from a cone of a map between two singleFunctors objects.
Русский
Характеризация вычленённых треугольников в производной категории через изоморфизм к конусам морфизмов между сдвинутыми объектами-одиночками; треугольник принадлежит к distTriang тогда и только тогда, когда он изоморфен треугольнику, построенному как конус отображения между двумя объектами singleFunctors.
LaTeX
$$$T \in \mathrm{distTriang}(\mathrm{DerivedCategory}(\mathcal{C})) \;\Longleftrightarrow\; \exists X,Y,f:\; T \cong Q.mapTriangle.obj(\mathrm{CochainComplex}.mappingCone.triangle(f)).$$$
Lean4
noncomputable instance : IsTriangulated (DerivedCategory C) :=
Triangulated.Localization.isTriangulated Qh (HomotopyCategory.subcategoryAcyclic C).trW
