singleTriangle_distinguished — Mathlib

English

The distinguished triangle hS.singleTriangle in DerivedCategory(C) is indeed a distinguished triangle.

Русский

Выделенный треугольник hS.singleTriangle в DerivedCategory(C) действительно является выделенным треугольником.

LaTeX

$$$$ hS.singleTriangle \in \mathrm{distTriang}(\mathrm{DerivedCategory}(C)). $$$$

Lean4

/-- The distinguished triangle in the derived category of `C` given by a
short exact short complex in `C`. -/
theorem singleTriangle_distinguished : hS.singleTriangle ∈ distTriang (DerivedCategory C) :=
  isomorphic_distinguished _
    (triangleOfSES_distinguished (hS.map_of_exact (HomologicalComplex.single C (ComplexShape.up ℤ) 0))) _
    (singleTriangleIso hS)

Похожие утверждения