Triangulated Categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains the definition of triangulated categories, which are
pretriangulated categories which satisfy the octahedron axiom.
Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧ given by an octahedron.
The first morphism of triangles given by an octahedron.
The second morphism of triangles given an octahedron.
A triangulated category is a pretriangulated category which satisfies
the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK
A choice of octahedron given by the octahedron axiom.