Triangulated categories · The Lumenary

MotivationH

What replaces short exact sequences?

The derived category $D(\mathcal{A})$ of an abelian category is not abelian: kernels and cokernels do not exist in general, so there are no short exact sequences. Yet the most important structure survives. A short exact sequence of complexes $0 \to X \to Y \to Z \to 0$ still gives a long exact sequence in cohomology, and the connecting maps $H^n(Z) \to H^{n+1}(X)$ suggest that $Z$ "maps to $X$ shifted by one". In $D(\mathcal{A})$ that map really exists: it is a morphism $Z \to X[1]$ , and we get a triangle

X \longrightarrow Y \longrightarrow Z \longrightarrow X[1].

Exactly the same shape appeared, at the same time and independently, in topology. For a map of spaces $f : X \to Y$ there is the cofibre sequence $X \to Y \to C_f \to \Sigma X \to \Sigma Y \to \cdots$ (Puppe, 1958), and in the stable homotopy category, where suspension $\Sigma$ is invertible, these sequences behave just like triangles in $D(\mathcal{A})$ . Jean-Louis Verdier (for algebra) and Dieter Puppe (for topology) extracted the common axioms around 1962–63. They are the subject of this lesson.

IntuitionH

Triangles that roll

Think of a distinguished triangle as a short exact sequence that has been allowed to wrap around: after $Z$ comes $X[1]$ , then $Y[1]$ , $Z[1]$ , $X[2]$ , … forever in both directions, and every three consecutive objects again form a triangle (the rotation axiom). Applying $\operatorname{Hom}(W, -)$ to this endless sequence gives an endless exact sequence of abelian groups. Every long exact sequence you know — in cohomology, in $\operatorname{Ext}$ , in homotopy groups of a fibration — is an instance.

Two warnings come with the picture. First, the third object $Z$ is determined by $X \to Y$ only up to isomorphism, and that isomorphism is not unique. Second, there are no kernels or cokernels to fall back on: everything must be done with triangles and Hom functors.

DefinitionsH

Verdier's axioms

Definition— triangle

Let $\mathcal{T}$ be an additive category with an additive automorphism (or autoequivalence) $[1] : \mathcal{T} \to \mathcal{T}$ , the shift, with $X[n] = X[1]^n$ . A triangle is a diagram $X \xrightarrow{u} Y \xrightarrow{v} Z \xrightarrow{w} X[1]$ . A morphism of triangles is a triple $(a, b, c)$ of maps $X \to X'$ , $Y \to Y'$ , $Z \to Z'$ making all three squares commute; the third square reads $w' c = a[1]\, w$ .

Definition— triangulated category

A triangulated category is such a $\mathcal{T}$ with a class of distinguished triangles satisfying:

TR1. (a) A triangle isomorphic to a distinguished one is distinguished. (b) For every $X$ , the triangle $X \xrightarrow{\mathrm{id}} X \to 0 \to X[1]$ is distinguished. (c) Every morphism $u : X \to Y$ is part of a distinguished triangle $X \xrightarrow{u} Y \to Z \to X[1]$ ; its third vertex $Z$ is called a cone of $u$ .
TR2 (rotation). $X \xrightarrow{u} Y \xrightarrow{v} Z \xrightarrow{w} X[1]$ is distinguished if and only if $Y \xrightarrow{v} Z \xrightarrow{w} X[1] \xrightarrow{-u[1]} Y[1]$ is.
TR3 (completion). Given distinguished triangles $(u, v, w)$ and $(u', v', w')$ and maps $a, b$ with $u' a = b u$ , there exists $c : Z \to Z'$ such that $(a, b, c)$ is a morphism of triangles.
TR4 (octahedral axiom). Given $u_{12} : X_1 \to X_2$ and $u_{23} : X_2 \to X_3$ with composite $u_{13}$ , and distinguished triangles on $u_{12}$ , $u_{23}$ , $u_{13}$ with cones $Z_{12}$ , $Z_{23}$ , $Z_{13}$ , there are maps $m_1 : Z_{12} \to Z_{13}$ and $m_3 : Z_{13} \to Z_{23}$ such that $Z_{12} \to Z_{13} \to Z_{23} \to Z_{12}[1]$ is distinguished and the diagram below commutes.

A category satisfying TR1–TR3 is called pretriangulated.

The octahedral axiom TR4: the two rows and the column through X₂ are the given triangles; the dashed maps exist and make the column through Z₁₃ a distinguished triangle.

The octahedral axiom is the triangulated form of the third isomorphism theorem $(X_3/X_1)/(X_2/X_1) \cong X_3/X_2$ : "the cone of $X_2/X_1 \to X_3/X_1$ is $X_3/X_2$ ". It is the axiom needed for Verdier quotients, for gluing t-structures and for most constructions; its name comes from drawing the four triangles as the faces of an octahedron.

Definition— homological functor

An additive functor $H : \mathcal{T} \to \mathcal{B}$ to an abelian category is homological if it sends every distinguished triangle to an exact sequence $H(X) \to H(Y) \to H(Z)$ . By rotation it then gives a long exact sequence $\cdots \to H(Z[-1]) \to H(X) \to H(Y) \to H(Z) \to H(X[1]) \to \cdots$ .

Definition— mapping cone

For a chain map $f : X \to Y$ of cochain complexes, the mapping cone is the complex $C(f)$ with $C(f)^n = X^{n+1} \oplus Y^n$ and

d_{C(f)}(x, y) = \big(-d_X x,\; f(x) + d_Y y\big).

It comes with chain maps $Y \to C(f)$ , $y \mapsto (0, y)$ , and $C(f) \to X[1]$ , $(x, y) \mapsto x$ , forming the standard triangle $X \xrightarrow{f} Y \to C(f) \to X[1]$ . One checks $d^2 = 0$ : $d(-dx, fx + dy) = (ddx,\, -f dx + d f x + ddy) = 0$ since $f$ is a chain map.

Definition— t-structure (Beilinson–Bernstein–Deligne)

A t-structure on a triangulated category $\mathcal{T}$ is a pair of strictly full subcategories $(\mathcal{T}^{\le 0}, \mathcal{T}^{\ge 0})$ ; writing $\mathcal{T}^{\le n} = \mathcal{T}^{\le 0}[-n]$ and $\mathcal{T}^{\ge n} = \mathcal{T}^{\ge 0}[-n]$ , it must satisfy

$\operatorname{Hom}(X, Y) = 0$ for $X \in \mathcal{T}^{\le 0}$ and $Y \in \mathcal{T}^{\ge 1}$ ;
$\mathcal{T}^{\le 0} \subseteq \mathcal{T}^{\le 1}$ and $\mathcal{T}^{\ge 1} \subseteq \mathcal{T}^{\ge 0}$ ;
every $X$ fits into a distinguished triangle $A \to X \to B \to A[1]$ with $A \in \mathcal{T}^{\le 0}$ and $B \in \mathcal{T}^{\ge 1}$ .

Its heart is $\mathcal{T}^{\heartsuit} = \mathcal{T}^{\le 0} \cap \mathcal{T}^{\ge 0}$ . The standard t-structure on $D(\mathcal{A})$ has $D^{\le 0} = \{X : H^i(X) = 0 \text{ for } i > 0\}$ and $D^{\ge 0} = \{X : H^i(X) = 0 \text{ for } i < 0\}$ ; the triangle in (3) is $\tau_{\le 0} X \to X \to \tau_{\ge 1} X \to$ , built from the truncations.

Worked examplesH

Examples and a worked long exact sequence

Example— The homotopy and derived categories

In $K(\mathcal{A})$ , for any additive category $\mathcal{A}$ , the distinguished triangles are those isomorphic to standard triangles $X \to Y \to C(f) \to X[1]$ . In $D(\mathcal{A})$ they are those isomorphic to images of standard triangles; equivalently, every short exact sequence of complexes $0 \to X \to Y \to Z \to 0$ gives a distinguished triangle $X \to Y \to Z \to X[1]$ in $D(\mathcal{A})$ — but not, in general, in $K(\mathcal{A})$ .

Example— Other sources of triangulated categories

The stable homotopy category of spectra, with cofibre sequences; homotopy groups and generalised cohomology theories are homological functors. See stable homotopy theory.
The stable module category $\underline{\mathrm{mod}}\, kG$ of a finite group in characteristic $p$ , where maps factoring through projectives are set to zero and the shift is $\Omega^{-1}$ (Happel). Its Hom groups compute Tate cohomology.
Over a field, $D(k)$ is equivalent to graded vector spaces, and every distinguished triangle is a direct sum of rotations of trivial triangles $V \xrightarrow{\mathrm{id}} V \to 0 \to V[1]$ .

Example— The cone of 2 : ℤ → ℤ, and its long exact sequence

In $K(\mathrm{Ab})$ the cone of $2 : \Z \to \Z$ is the complex $\Z \xrightarrow{2} \Z$ in degrees $-1, 0$ , which is quasi-isomorphic to $\Z/2$ . So in $D(\mathrm{Ab})$ there is a distinguished triangle

\Z \xrightarrow{\;2\;} \Z \longrightarrow \Z/2 \xrightarrow{\;\delta\;} \Z[1],

whose connecting map $\delta$ is the non-zero element of $\operatorname{Hom}_D(\Z/2, \Z[1]) = \operatorname{Ext}^1(\Z/2, \Z) \cong \Z/2$ . Apply the homological functor $\operatorname{Hom}(\Z/2, -)$ , and use $\operatorname{Hom}(\Z/2, N[n]) = \operatorname{Ext}^n(\Z/2, N)$ :

\underbrace{\operatorname{Hom}(\Z/2, \Z)}_{0} \to \underbrace{\operatorname{Hom}(\Z/2, \Z/2)}_{\Z/2} \xrightarrow{\delta_*} \underbrace{\operatorname{Ext}^1(\Z/2, \Z)}_{\Z/2} \xrightarrow{2} \underbrace{\operatorname{Ext}^1(\Z/2, \Z)}_{\Z/2} \to \underbrace{\operatorname{Ext}^1(\Z/2, \Z/2)}_{\Z/2} \to \underbrace{\operatorname{Ext}^2(\Z/2, \Z)}_{0}.

Exactness forces $\delta_*$ to be an isomorphism, multiplication by $2$ to be zero on $\Z/2$ (as it is), and $\operatorname{Ext}^1(\Z/2, \Z) \to \operatorname{Ext}^1(\Z/2, \Z/2)$ to be an isomorphism — every arrow is determined, and every group agrees with a direct computation.

Example— Fill-ins are not unique

Over a field $k$ , take $X = k$ and $Y = k[1]$ , and the zero map $0 : X \to Y$ . A cone is $Z = Y \oplus X[1] = k[1] \oplus k[1]$ , with $Y \to Z$ the inclusion and $Z \to X[1]$ the projection. Complete the identity square $(a, b) = (\mathrm{id}_X, \mathrm{id}_Y)$ by TR3. A map $c : Z \to Z$ is a $2 \times 2$ matrix, and the two commutation conditions force

c = \begin{pmatrix} 1 & t \\ 0 & 1 \end{pmatrix}, \qquad t \in \operatorname{Hom}(X[1], Y) = \operatorname{Hom}(k[1], k[1]) = k

arbitrary. Every $t$ gives a morphism of triangles extending the identity, and all of them are isomorphisms. So the " $c$ " of TR3 is not unique, even when $a$ and $b$ are identities — and the isomorphism between two cones of the same map is not canonical. The experiment below finds exactly $p$ fill-ins over $\mathbb{F}_p$ .

ProofH

First consequences of the axioms

Throughout, $\mathcal{T}$ is pretriangulated (TR1–TR3); the octahedral axiom is not needed for any of these results.

Theorem— Proposition 1 — consecutive maps compose to zero

In a distinguished triangle $X \xrightarrow{u} Y \xrightarrow{v} Z \xrightarrow{w} X[1]$ we have $vu = 0$ , $wv = 0$ and $u[1]\,w = 0$ .

Proof

The triangle $X \xrightarrow{\mathrm{id}} X \to 0 \to X[1]$ is distinguished (TR1b), and the square with vertical maps $\mathrm{id}_X$ and $u$ commutes ( $u \circ \mathrm{id} = u \circ \mathrm{id}$ ). By TR3 there is $c : 0 \to Z$ completing a morphism of triangles; the middle square says $v \circ u = c \circ 0 = 0$ . The other two identities follow by applying this to the rotated triangles (TR2).

∎

Theorem— Proposition 2 — Hom functors are homological

For every object $W$ , the functor $\operatorname{Hom}(W, -)$ is homological: for a distinguished triangle as above, $\operatorname{Hom}(W, X) \to \operatorname{Hom}(W, Y) \to \operatorname{Hom}(W, Z)$ is exact. Dually $\operatorname{Hom}(-, W)$ is cohomological. Hence every distinguished triangle gives long exact sequences

\cdots \to \operatorname{Hom}(W, Z[-1]) \to \operatorname{Hom}(W, X) \to \operatorname{Hom}(W, Y) \to \operatorname{Hom}(W, Z) \to \operatorname{Hom}(W, X[1]) \to \cdots

Proof

Composites are zero by Proposition 1. Conversely let $\varphi : W \to Y$ with $v \varphi = 0$ . Rotate both the trivial triangle $W \xrightarrow{\mathrm{id}} W \to 0 \to W[1]$ and our triangle once (TR2), giving distinguished triangles $W \to 0 \to W[1] \xrightarrow{-\mathrm{id}} W[1]$ and $Y \xrightarrow{v} Z \xrightarrow{w} X[1] \xrightarrow{-u[1]} Y[1]$ . The maps $\varphi : W \to Y$ and $0 : 0 \to Z$ form a commutative square, since $v\varphi = 0$ . TR3 gives $\psi' : W[1] \to X[1]$ with $-u[1]\,\psi' = \varphi[1] \circ (-\mathrm{id})$ , i.e. $u[1]\, \psi' = \varphi[1]$ . Since $[1]$ is an equivalence, $\psi' = \psi[1]$ for a unique $\psi : W \to X$ , and $u \psi = \varphi$ . Rotating the triangle gives exactness at every other place.

∎

Theorem— Proposition 3 — triangulated five lemma

If $(a, b, c)$ is a morphism of distinguished triangles and two of $a, b, c$ are isomorphisms, so is the third. In particular, the cone of a morphism is unique up to isomorphism.

Proof

Say $a$ and $c$ are isomorphisms. For every $W$ , apply $\operatorname{Hom}(W, -)$ to both triangles: Proposition 2 gives two long exact sequences and a map between them, in which the maps induced by $a$ , $c$ , $a[1]$ , $c[-1]$ are bijective. By the five lemma for abelian groups, $b_* : \operatorname{Hom}(W, Y) \to \operatorname{Hom}(W, Y')$ is bijective for every $W$ , so $b$ is an isomorphism by the Yoneda lemma. The other cases follow by rotation. If $Z$ and $Z'$ are both cones of $u$ , complete $(\mathrm{id}, \mathrm{id})$ by TR3 to $(\mathrm{id}, \mathrm{id}, c)$ ; by what we just proved $c$ is an isomorphism.

∎

The isomorphism $c$ between two cones is not unique — the example above exhibits a whole line of choices. This is what is meant by saying that cones are not functorial: the axioms provide no cone functor on morphisms, and the non-uniqueness of fill-ins means there is no canonical way to choose one.

Theorem— Theorem 4 — monomorphisms and epimorphisms split

In a pretriangulated category every monomorphism is a split monomorphism and every epimorphism is a split epimorphism.

Proof

Let $u : X \to Y$ be a monomorphism, and complete it to a distinguished triangle $X \xrightarrow{u} Y \xrightarrow{v} Z \xrightarrow{w} X[1]$ (TR1c). By Proposition 1, $u[1]\, w = 0$ ; and $u[1]$ is a monomorphism because $[1]$ is an equivalence. Hence $w = 0$ . Rotating backwards, $Z[-1] \xrightarrow{-w[-1]} X \xrightarrow{u} Y \xrightarrow{v} Z$ is distinguished with first map $0$ . By the cohomological exactness of $\operatorname{Hom}(-, X)$ , the map $\mathrm{id}_X$ , which kills $-w[-1] = 0$ , factors as $\mathrm{id}_X = r u$ for some $r : Y \to X$ .

If $u$ is an epimorphism instead, then $v u = 0 = 0 \circ u$ gives $v = 0$ . By Proposition 2, $\mathrm{id}_Y$ (which satisfies $v \circ \mathrm{id}_Y = 0$ ) factors as $\mathrm{id}_Y = u s$ .

∎

Theorem— Corollary 5 — triangulated and abelian means semisimple; D(Ab) is not abelian

If a pretriangulated category $\mathcal{T}$ is abelian, then every morphism $f$ is von Neumann regular ( $fgf = f$ for some $g$ ) and every short exact sequence splits. In particular $D(\mathrm{Ab})$ , $K(\mathrm{Ab})$ and $D(R)$ for any ring $R$ that is not semisimple are not abelian.

Proof

In an abelian category $f = m e$ with $e$ an epimorphism onto the image and $m$ a monomorphism. By Theorem 4, $e s = \mathrm{id}$ and $r m = \mathrm{id}$ for some $s, r$ ; then $f (s r) f = m (e s)(r m) e = m e = f$ . A short exact sequence $0 \to A \xrightarrow{i} B \to C \to 0$ splits because $i$ has a retraction.

In $D(\mathrm{Ab})$ , $\operatorname{End}(\Z) = \operatorname{End}_{\mathrm{Ab}}(\Z) = \Z$ because $\mathrm{Ab} \to D(\mathrm{Ab})$ is fully faithful, and $2 g 2 = 2$ has no solution $g \in \Z$ . So $2 : \Z \to \Z$ is not regular, and $D(\mathrm{Ab})$ is not abelian; the same argument works in $K(\mathrm{Ab})$ . More generally, if $R$ is not semisimple, some submodule $A \subseteq B$ is not a direct summand. Its inclusion $i$ is not regular in $R\text{-Mod}$ : from $i g i = i$ and $i$ injective we would get $g i = \mathrm{id}_A$ , splitting $A$ off $B$ . By full faithfulness of $R\text{-Mod} \to D(R)$ , $i$ is not regular in $D(R)$ either, so $D(R)$ is not abelian.

∎

Theorem— Theorem 6 — K(A) and D(A) are triangulated (proof sketched)

For an additive category $\mathcal{A}$ , $K(\mathcal{A})$ with the triangles isomorphic to standard cone triangles is triangulated. For an abelian category $\mathcal{A}$ , $D(\mathcal{A})$ is triangulated, $Q : K(\mathcal{A}) \to D(\mathcal{A})$ is an exact functor, and a chain map $s$ is a quasi-isomorphism if and only if its cone is acyclic.

Proof

Sketch. TR1 is immediate: the cone of $\mathrm{id}_X$ is contractible (the map $(x, y) \mapsto (y, 0)$ is a contracting homotopy). For TR2 one writes down an explicit homotopy equivalence between $C(v)$ for $v : Y \to C(u)$ and $X[1]$ ; the sign $-u[1]$ is forced by the sign in $d_{C(f)}$ . For TR3, a homotopy $h$ with $b u - u' a = dh + hd$ gives the chain map $C(u) \to C(u')$ , $(x, y) \mapsto (a x, b y + h x)$ — note that it depends on the choice of $h$ . TR4 is a direct but longer computation. Details: Weibel, An Introduction to Homological Algebra, §10.2; Kashiwara–Schapira, Categories and Sheaves, Ch. 11. The cone of $s$ sits in a short exact sequence of complexes $0 \to Y \to C(s) \to X[1] \to 0$ , whose long exact cohomology sequence has connecting maps $H^n(s)$ ; hence $C(s)$ is acyclic iff all $H^n(s)$ are isomorphisms. Finally, the acyclic complexes form a thick triangulated subcategory of $K(\mathcal{A})$ and $D(\mathcal{A})$ is the Verdier quotient by it, which inherits a triangulated structure (Verdier).

∎

Theorem— Theorem 7 — the heart of a t-structure (Beilinson–Bernstein–Deligne, 1982)

The heart of any t-structure is an abelian category, and its short exact sequences are exactly the distinguished triangles $A \to B \to C \to A[1]$ with $A, B, C$ in the heart. There is a homological functor $H^0_t : \mathcal{T} \to \mathcal{T}^{\heartsuit}$ . For the standard t-structure on $D(\mathcal{A})$ , the heart consists of the complexes with cohomology only in degree $0$ and is equivalent to $\mathcal{A}$ , with $H^0_t = H^0$ .

Proof

The general theorem is proved in BBD, Théorème 1.3.6; see also Gelfand–Manin, Ch. IV.4. For the standard t-structure: if $H^i(X) = 0$ for $i \neq 0$ , the truncation maps $X \leftarrow \tau_{\le 0} X \to H^0(X)[0]$ are quasi-isomorphisms, so $X \cong H^0(X)[0]$ , and $\mathcal{A} \to D(\mathcal{A})$ is fully faithful (previous lesson). A short exact sequence $0 \to A \to B \to C \to 0$ in $\mathcal{A}$ gives a distinguished triangle $A \to B \to C \to A[1]$ , and conversely a triangle with vertices in the heart has a long exact cohomology sequence which, all objects being concentrated in degree $0$ , is a short exact sequence.

∎

Theorem— Proposition 8 — negative Ext vanishes in the heart

If $A, B$ lie in the heart of a t-structure, then $\operatorname{Hom}(A, B[-1]) = 0$ .

Proof

$B \in \mathcal{T}^{\ge 0}$ , so $B[-1] \in \mathcal{T}^{\ge 1}$ , while $A \in \mathcal{T}^{\le 0}$ . Axiom (1) gives $\operatorname{Hom}(A, B[-1]) = 0$ .

∎

In $D(\mathcal{A})$ this is the statement $\operatorname{Ext}^{-1}_{\mathcal{A}}(A, B) = 0$ ; in general, Hom-groups $\operatorname{Hom}(A, B[n])$ between objects of the heart behave like Ext groups, but for $n \ge 2$ they need not agree with the Ext groups computed inside the heart (they do for the standard t-structure on $D^b(\mathcal{A})$ ).

ExplanationH

The landscape: enhancements, stability, open questions

Enhancements. Cones in $K(\mathcal{A})$ depend on a choice of homotopy (Theorem 6), so the triangulated structure is the shadow of something richer. Bondal and Kapranov (1990) proposed remembering the dg-category of complexes; Lurie's stable ∞-categories (2006 onwards) do the same homotopy-coherently, and in them cones are functorial (they are cofibres). Every stable ∞-category has a triangulated homotopy category (Lurie, Higher Algebra, Thm. 1.1.2.14). The converse fails: Muro, Schwede and Strickland (2007) constructed triangulated categories (for instance a triangulation of finitely generated free $\Z/4$ -modules with identity shift) that are not equivalent to a full triangulated subcategory of the homotopy category of any stable model category, hence not "algebraic" or "topological". See stable ∞-categories.

Uniqueness of enhancements. Lunts and Orlov (2010) proved that $D^b(\mathrm{Coh}\,X)$ for a quasi-projective variety $X$ has a unique dg-enhancement. Rizzardo, Van den Bergh and Neeman (2019) constructed an exact functor between derived categories of smooth projective varieties that is not of Fourier–Mukai type, showing that the triangulated structure alone does not determine everything one might hope.

Brown representability and compact generation. Neeman (1996) proved Brown representability for compactly generated triangulated categories — every cohomological functor sending coproducts to products is representable — and used it to give a short proof of Grothendieck duality.

Stability conditions. Bridgeland (2007) defined a stability condition on $\mathcal{T}$ as the heart of a bounded t-structure together with a "central charge" $Z : K_0 \to \mathbb{C}$ satisfying a Harder–Narasimhan property, and proved that the stability conditions (satisfying a support condition) form a complex manifold. These spaces are now studied in algebraic geometry, representation theory and mirror symmetry. Their topology is largely unknown: Bridgeland conjectured that a distinguished component for a K3 surface is simply connected, and Bayer and Bridgeland (2017) proved it is even contractible when the Picard rank is one.

Tensor-triangular geometry. Balmer (2005) attached to a tensor-triangulated category a topological space, its spectrum, recovering $X$ from $D^{\mathrm{perf}}(X)$ and organising the classification of thick subcategories (Hopkins–Smith in stable homotopy, Benson–Carlson–Rickard for $\underline{\mathrm{mod}}\,kG$ ).

Open questions. Whether the octahedral axiom TR4 follows from TR1–TR3 is a long-standing open question. Freyd's generating hypothesis (1966) — is the stable homotopy groups functor faithful on finite spectra? — is open. Which triangulated categories admit enhancements, and when they are unique, is understood only for special classes. Many spaces of stability conditions remain uncomputed.

Formal mathematicsF

Triangulated categories in Lean and Mathlib

Mathlib has pretriangulated categories (CategoryTheory.Pretriangulated: a preadditive category with an additive shift by $\Z$ and the axioms TR1–TR3 with rotation), the octahedral axiom (IsTriangulated), triangulated functors, the triangulated structures on HomotopyCategory and DerivedCategory, and t-structures with their hearts. We prove from the axioms the results of the previous section. Proposition 1 and Proposition 2:

comp_zero_of_distinguishedLean 4Proved here from basic factsFormally verified

/-- In a distinguished triangle `X → Y → Z → X[1]` the composite `X → Y → Z` is zero.
Proof from the axioms: the triangle `X = X → 0 → X[1]` is distinguished (TR1), and the square
`(𝟙 X, f)` from it to our triangle commutes, so TR3 gives `c : 0 → Z` with `g ∘ f = c ∘ 0 = 0`.
(Mathlib: `Pretriangulated.comp_distTriang_mor_zero₁₂`.) -/
theorem comp_zero_of_distinguished (T : Triangle C) (hT : T ∈ distTriang C) :
    T.mor₁ ≫ T.mor₂ = 0 := by
  have h₀ : Triangle.mk (𝟙 T.obj₁) (0 : T.obj₁ ⟶ 0) 0 ∈ distTriang C :=
    contractible_distinguished T.obj₁
  obtain ⟨c, hc₁, _⟩ := complete_distinguished_triangle_morphism _ T h₀ hT
    (𝟙 T.obj₁) T.mor₁ (by simp)
  rw [← hc₁]
  exact zero_comp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

hom_exact_middleLean 4Proved here from basic factsFormally verified

/-- `Hom(W, -)` is exact in the middle on a distinguished triangle `X → Y → Z → X[1]`:
a map `φ : W → Y` with `g ∘ φ = 0` factors through `f : X → Y`.
Proof: compare the distinguished triangle `W = W → 0 → W[1]` with ours using `(φ, 0)` on the
last two vertices; TR3 (in its rotated form `complete_distinguished_triangle_morphism₁`)
supplies `ψ : W → X` with `f ∘ ψ = φ ∘ 𝟙 = φ`.
(Mathlib: `Pretriangulated.Triangle.coyoneda_exact₂`.) -/
theorem hom_exact_middle (T : Triangle C) (hT : T ∈ distTriang C) {W : C}
    (φ : W ⟶ T.obj₂) (hφ : φ ≫ T.mor₂ = 0) : ∃ ψ : W ⟶ T.obj₁, ψ ≫ T.mor₁ = φ := by
  have h₀ : Triangle.mk (𝟙 W) (0 : W ⟶ 0) 0 ∈ distTriang C := contractible_distinguished W
  obtain ⟨a, ha₁, _⟩ := complete_distinguished_triangle_morphism₁ _ T h₀ hT φ 0
    (by simp [hφ])
  exact ⟨a, by simpa using ha₁.symm⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

Theorem 4, in four steps — the connecting map vanishes, a retraction exists, and every monomorphism and every epimorphism splits:

connecting_map_eq_zero_of_monoLean 4Proved here from basic factsFormally verified

/-- If `f : X → Y` in a distinguished triangle `X → Y → Z → X[1]` is a monomorphism, the
connecting map `h : Z → X[1]` is zero. Proof: `f[1] ∘ h = 0` (two consecutive maps of the
rotated triangle), and `f[1]` is again a monomorphism because `[1]` is an equivalence. -/
theorem connecting_map_eq_zero_of_mono (T : Triangle C) (hT : T ∈ distTriang C) [Mono T.mor₁] :
    T.mor₃ = 0 := by
  have h : T.mor₃ ≫ T.mor₁⟦(1 : ℤ)⟧' = 0 := comp_distTriang_mor_zero₃₁ T hT
  rw [← cancel_mono (T.mor₁⟦(1 : ℤ)⟧'), h, zero_comp]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

exists_retraction_of_monoLean 4Proved here from basic factsFormally verified

/-- If `f : X → Y` in a distinguished triangle is a monomorphism, it has a retraction
`r : Y → X` with `r ∘ f = 𝟙`. Proof: the connecting map vanishes
(`connecting_map_eq_zero_of_mono`), so in the rotated-back triangle `Z[-1] → X → Y → Z` the
first map is zero; then `𝟙 X` kills it and, by exactness of `Hom(-, X)` (Mathlib's
`Triangle.yoneda_exact₂`), factors through `f`. -/
theorem exists_retraction_of_mono (T : Triangle C) (hT : T ∈ distTriang C) [Mono T.mor₁] :
    ∃ r : T.obj₂ ⟶ T.obj₁, T.mor₁ ≫ r = 𝟙 T.obj₁ := by
  have h3 : T.mor₃ = 0 := connecting_map_eq_zero_of_mono T hT
  obtain ⟨r, hr⟩ := Triangle.yoneda_exact₂ T.invRotate (inv_rot_of_distTriang T hT)
    (𝟙 T.obj₁) (by simp [h3]; exact zero_comp)
  exact ⟨r, hr.symm⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

isSplitMono_of_monoLean 4Proved here from basic factsFormally verified

/-- **Every monomorphism in a (pre)triangulated category is split.** Complete `f` to a
distinguished triangle (TR1) and apply `exists_retraction_of_mono`. -/
theorem isSplitMono_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f := by
  obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
  have : Mono (Triangle.mk f g h).mor₁ := by simpa using (inferInstance : Mono f)
  obtain ⟨r, hr⟩ := exists_retraction_of_mono _ hT
  exact IsSplitMono.mk' ⟨r, hr⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

isSplitEpi_of_epiLean 4Proved here from basic factsFormally verified

/-- **Every epimorphism in a (pre)triangulated category is split.** Complete `f : X → Y` to a
distinguished triangle `X → Y → Z → X[1]`. Since `g ∘ f = 0` and `f` is epi, `g = 0`; so
`𝟙 Y` satisfies `g ∘ 𝟙 = 0` and factors through `f` by `hom_exact_middle`. -/
theorem isSplitEpi_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f := by
  obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
  have hg : g = 0 := by
    rw [← cancel_epi f, comp_zero]
    exact comp_zero_of_distinguished _ hT
  obtain ⟨s, hs⟩ := hom_exact_middle _ hT (𝟙 Y) (by simp [hg])
  exact IsSplitEpi.mk' ⟨s, hs⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

Corollary 5, split into its abstract half and its arithmetic half:

regular_of_epi_monoLean 4Proved here from basic factsFormally verified

/-- If `f = m ∘ e` with `e` epi and `m` mono (an image factorisation, which every morphism of an
abelian category has), then `f` is *von Neumann regular*: `f ∘ g ∘ f = f` for some `g`.
Proof: `e` has a section `s` and `m` a retraction `r`; take `g = s ∘ r`. This is the heart of
the argument that a triangulated category which is abelian must be semisimple. -/
theorem regular_of_epi_mono {X Y I : C} (f : X ⟶ Y) (e : X ⟶ I) (m : I ⟶ Y) [Epi e] [Mono m]
    (hf : e ≫ m = f) : ∃ g : Y ⟶ X, f ≫ g ≫ f = f := by
  obtain ⟨⟨s, hs⟩⟩ := (isSplitEpi_of_epi e).exists_splitEpi
  obtain ⟨⟨r, hr⟩⟩ := (isSplitMono_of_mono m).exists_splitMono
  refine ⟨r ≫ s, ?_⟩
  subst hf
  calc (e ≫ m) ≫ (r ≫ s) ≫ e ≫ m = e ≫ (m ≫ r) ≫ (s ≫ e) ≫ m := by
        simp only [Category.assoc]
    _ = e ≫ m := by rw [hr, hs]; simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

two_not_regularLean 4Proved here from basic factsFormally verified

/-- Multiplication by `2` on `ℤ` is not von Neumann regular: there is no integer `g` with
`2 · g · 2 = 2`. Combined with `regular_of_epi_mono`, and the fact that `Hom_{D(Ab)}(ℤ, ℤ) = ℤ`,
this shows that `D(Ab)` is not an abelian category. -/
theorem two_not_regular : ¬ ∃ g : ℤ, 2 * g * 2 = 2 := by
  rintro ⟨g, hg⟩
  omega

Axioms used: propext, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

The five lemma and the uniqueness of cones are applied from Mathlib (their proofs there follow Proposition 3):

five_lemmaLean 4Applies a library theoremFormally verified

/-- The triangulated five lemma: in a morphism of distinguished triangles, if the first and
third components are isomorphisms, so is the second. This applies Mathlib's
`Pretriangulated.isIso₂_of_isIso₁₃`. -/
theorem five_lemma {T T' : Triangle C} (φ : T ⟶ T') (hT : T ∈ distTriang C)
    (hT' : T' ∈ distTriang C) (h₁ : IsIso φ.hom₁) (h₃ : IsIso φ.hom₃) : IsIso φ.hom₂ :=
  isIso₂_of_isIso₁₃ φ hT hT' h₁ h₃

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

cone_unique_up_to_isoLean 4Applies a library theoremFormally verified

/-- Two distinguished triangles on isomorphic morphisms are isomorphic, compatibly with the
given isomorphism of arrows: the cone is unique up to isomorphism. The isomorphism of third
vertices is *not* unique — the source of the non-functoriality of cones. This applies Mathlib's
`Pretriangulated.exists_iso_of_arrow_iso` (proved with TR3 and the five lemma). -/
theorem cone_unique_up_to_iso (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C)
    (hT₂ : T₂ ∈ distTriang C) (e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁) :
    ∃ e' : T₁ ≅ T₂, e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right :=
  exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ e

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

Proposition 8, from the t-structure axioms as Mathlib states them:

heart_hom_neg_shift_eq_zeroLean 4Proved here from basic factsFormally verified

/-- For a t-structure `t` and objects `A`, `B` of its heart, every map `A → B[-1]` is zero:
"negative Ext groups vanish in the heart". Proof: `B` is `≥ 0`, so `B[-1]` is `≥ 1` (shift
axiom), while `A` is `≤ 0`; the orthogonality axiom `Hom(D^{≤0}, D^{≥1}) = 0` finishes. -/
theorem heart_hom_neg_shift_eq_zero (t : Triangulated.TStructure C) {A B : C}
    (hA : t.heart A) (hB : t.heart B) (f : A ⟶ B⟦(-1 : ℤ)⟧) : f = 0 := by
  rw [Triangulated.TStructure.mem_heart_iff] at hA hB
  have hB' : t.ge 1 (B⟦(-1 : ℤ)⟧) := t.ge_shift 0 (-1) 1 (by norm_num) B hB.2.ge
  exact t.zero' f hA.1.le hB'

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

And the triangulated structures of Theorem 6, which are substantial theorems in Mathlib (the octahedral axiom for $K(\mathcal{A})$ is verified with explicit homotopy equivalences of mapping cones):

homotopy_category_triangulatedLean 4Applies a library theoremFormally verified

/-- The homotopy category `K(A)` of cochain complexes in an additive category is triangulated:
distinguished triangles are those isomorphic to mapping-cone triangles, and the octahedral
axiom holds. This is Mathlib's instance for `HomotopyCategory C (ComplexShape.up ℤ)`. -/
theorem homotopy_category_triangulated (A : Type u) [Category.{v} A] [Preadditive A]
    [HasZeroObject A] [HasBinaryBiproducts A] :
    IsTriangulated (HomotopyCategory A (ComplexShape.up ℤ)) :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

derived_category_triangulatedLean 4Applies a library theoremFormally verified

/-- The derived category `D(A)` of an abelian category is triangulated. Mathlib deduces this
from the triangulated structure on `K(A)` by Verdier localisation at the acyclic complexes. -/
theorem derived_category_triangulated (A : Type u) [Category.{v} A] [Abelian A]
    [HasDerivedCategory A] : IsTriangulated (DerivedCategory A) :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TriangulatedCategories.leanTry it in the Lean web editor

Not formalised here: the full long exact Hom sequence as a single statement (Mathlib has it via Pretriangulated.Triangle.coyoneda_exact₁, ₂, ₃), the octahedral axiom's consequences, and the theorem that the heart is abelian, which at this Mathlib version is listed as future work in Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean. The identification of the standard heart with $\mathcal{A}$ is likewise not yet in Mathlib.

ComputationC

Cones over a finite field

The experiment builds random cochain complexes and chain maps over $\mathbb{F}_{101}$ , forms mapping cones with the formula above, and checks three things exactly: $d_C^2 = 0$ ; the dimension formula

\dim H^n(C(f)) = \big(\dim H^n(Y) - \operatorname{rank} H^n(f)\big) + \big(\dim H^{n+1}(X) - \operatorname{rank} H^{n+1}(f)\big),

which is equivalent to the exactness of the long exact cohomology sequence of the cone; and that $f$ is a quasi-isomorphism exactly when $C(f)$ is acyclic. Then it counts, by brute force over all $2 \times 2$ matrices, the fill-ins of the worked example: there are $p$ of them over $\mathbb{F}_p$ .

Mapping cones over F_p: exactness and non-unique fill-insPythonExact computationExperimental evidenceExhaustive finite checkComputationally tested

"""Mapping cones over a finite field: the long exact sequence, checked exactly.

In the homotopy category K(k) every chain map f : X -> Y sits in a
distinguished triangle X -> Y -> C(f) -> X[1], where the mapping cone has
C(f)^n = X^(n+1) + Y^n and d(x, y) = (-dx, f(x) + dy). Applying cohomology
gives a long exact sequence, which is equivalent to the dimension formula

    dim H^n(C) = (dim H^n(Y) - rank H^n(f)) + (dim H^(n+1)(X) - rank H^(n+1)(f)).

We build random complexes and random chain maps over F_101 (exact modular
arithmetic), check that d_C o d_C = 0, check the formula in every degree, and
check that f is a quasi-isomorphism exactly when C(f) is acyclic. Then we count
by brute force the morphisms of triangles that complete the identity square
for the triangle X --0--> Y -> Y + X[1] -> X[1] in D(F_p): there are p of them,
so the third map in TR3 is not unique. Exact computations on random examples
and a finite count: evidence for the theorems proved in the lesson.
"""

import random
from itertools import product

P = 101

def rank(rows, p=P):
    """Rank of a matrix (list of rows) over F_p by Gaussian elimination."""
    m = [[v % p for v in r] for r in rows if r]
    if not m:
        return 0
    r, cols = 0, len(m[0])
    for c in range(cols):
        piv = next((i for i in range(r, len(m)) if m[i][c]), None)
        if piv is None:
            continue
        m[r], m[piv] = m[piv], m[r]
        inv = pow(m[r][c], p - 2, p)
        m[r] = [v * inv % p for v in m[r]]
        for i in range(len(m)):
            if i != r and m[i][c]:
                t = m[i][c]
                m[i] = [(a - t * b) % p for a, b in zip(m[i], m[r])]
        r += 1
    return r

def nullspace(rows, ncols, p=P):
    """A basis of {v : rows v = 0} over F_p."""
    m = [[v % p for v in r] for r in rows]
    pivots, r = [], 0
    for c in range(ncols):
        piv = next((i for i in range(r, len(m)) if m[i][c]), None)
        if piv is None:
            continue
        m[r], m[piv] = m[piv], m[r]
        inv = pow(m[r][c], p - 2, p)
        m[r] = [v * inv % p for v in m[r]]
        for i in range(len(m)):
            if i != r and m[i][c]:
                t = m[i][c]
                m[i] = [(a - t * b) % p for a, b in zip(m[i], m[r])]
        pivots.append(c)
        r += 1
    basis = []
    for free in (c for c in range(ncols) if c not in pivots):
        v = [0] * ncols
        v[free] = 1
        for i, c in enumerate(pivots):
            v[c] = -m[i][free] % p
        basis.append(v)
    return basis

def matmul(a, b, p=P):
    """Product of matrices given as lists of rows (handles empty shapes)."""
    if not a or not b:
        return [[0] * (len(b[0]) if b else 0) for _ in a]
    return [[sum(x * y for x, y in zip(row, col)) % p for col in zip(*b)]
            for row in a]

def zeros(r, c):
    """The r x c zero matrix."""
    return [[0] * c for _ in range(r)]

def random_complex(rng, length=4, max_dim=3):
    """A random complex: dims[n] and differentials d[n] : X^n -> X^(n+1).

    Built as a sum of pieces k (in one degree) and k --1--> k, then hidden by
    random changes of basis, so that d o d = 0 holds by construction.
    """
    pieces = []
    for n in range(length):
        pieces += [("H", n)] * rng.randint(0, max_dim - 1)
        if n + 1 < length:
            pieces += [("A", n)] * rng.randint(0, 1)
    dims = [0] * length
    where = []
    for kind, n in pieces:
        where.append((kind, n, dims[n], dims[n + 1] if kind == "A" else None))
        dims[n] += 1
        if kind == "A":
            dims[n + 1] += 1
    d = [zeros(dims[n + 1], dims[n]) for n in range(length - 1)]
    for kind, n, i, j in where:
        if kind == "A":
            d[n][j][i] = 1
    g = [random_invertible(rng, k) for k in dims]
    ginv = [inverse(m) for m in g]
    return dims, [matmul(matmul(g[n + 1], d[n]), ginv[n])
                  for n in range(length - 1)]

def random_invertible(rng, k):
    """A uniformly random invertible k x k matrix over F_p."""
    while True:
        m = [[rng.randrange(P) for _ in range(k)] for _ in range(k)]
        if rank(m) == k:
            return m

def inverse(m):
    """Inverse of an invertible matrix over F_p (Gauss-Jordan)."""
    k = len(m)
    aug = [row[:] + [int(i == j) for j in range(k)] for i, row in enumerate(m)]
    for c in range(k):
        piv = next(i for i in range(c, k) if aug[i][c] % P)
        aug[c], aug[piv] = aug[piv], aug[c]
        inv = pow(aug[c][c], P - 2, P)
        aug[c] = [v * inv % P for v in aug[c]]
        for i in range(k):
            if i != c and aug[i][c]:
                t = aug[i][c]
                aug[i] = [(a - t * b) % P for a, b in zip(aug[i], aug[c])]
    return [row[k:] for row in aug]

def random_chain_map(rng, x, y):
    """A random solution f of d_Y f^n = f^(n+1) d_X (all degrees)."""
    (dx, ddx), (dy, ddy) = x, y
    length = len(dx)
    offs, tot = [], 0
    for n in range(length):
        offs.append(tot)
        tot += dy[n] * dx[n]
    eqs = []
    for n in range(length - 1):
        for i in range(dy[n + 1]):
            for j in range(dx[n]):
                row = [0] * tot
                for k in range(dy[n]):  # (d_Y f^n)[i][j]
                    row[offs[n] + k * dx[n] + j] += ddy[n][i][k]
                for k in range(dx[n + 1]):  # (f^(n+1) d_X)[i][j]
                    row[offs[n + 1] + i * dx[n + 1] + k] -= ddx[n][k][j]
                eqs.append(row)
    basis = nullspace(eqs, tot) if eqs else [
        [int(i == j) for j in range(tot)] for i in range(tot)]
    v = [0] * tot
    for b in basis:
        c = rng.randrange(P)
        v = [(a + c * bb) % P for a, bb in zip(v, b)]
    return [[[v[offs[n] + i * dx[n] + j] for j in range(dx[n])]
             for i in range(dy[n])] for n in range(length)]

def cone(x, y, f):
    """Mapping cone, with C^n = X^(n+1) + Y^n, as (dims, differentials).

    Degrees run from -1 (where C^-1 = X^0) to length - 1.
    """
    (dx, ddx), (dy, ddy) = x, y
    length = len(dx)
    xd = lambda n: dx[n] if 0 <= n < length else 0
    yd = lambda n: dy[n] if 0 <= n < length else 0
    dims = [xd(n + 1) + yd(n) for n in range(-1, length)]
    diffs = []
    for n in range(-1, length - 1):
        m = zeros(xd(n + 2) + yd(n + 1), xd(n + 1) + yd(n))
        for i in range(xd(n + 2)):
            for j in range(xd(n + 1)):
                m[i][j] = -ddx[n + 1][i][j] % P
        for i in range(yd(n + 1)):
            for j in range(xd(n + 1)):
                m[xd(n + 2) + i][j] = f[n + 1][i][j]
            for j in range(yd(n)):
                m[xd(n + 2) + i][xd(n + 1) + j] = ddy[n][i][j]
        diffs.append(m)
    return dims, diffs

def cohomology(c):
    """dim H^n for a complex (dims, diffs) indexed from its first term."""
    dims, d = c
    out = []
    for n in range(len(dims)):
        rk_out = rank(d[n]) if n < len(d) else 0
        rk_in = rank(d[n - 1]) if n > 0 else 0
        out.append(dims[n] - rk_out - rk_in)
    return out

def cycles(c, n):
    """A basis of Z^n = ker d^n (as vectors)."""
    dims, d = c
    if n >= len(d):
        return [[int(i == j) for j in range(dims[n])] for i in range(dims[n])]
    return nullspace(d[n], dims[n])

def rank_on_cohomology(x, y, f, n):
    """rank of H^n(f) = dim(f(Z^n X) + B^n Y) - dim B^n Y."""
    image = [[sum(f[n][i][j] * z[j] for j in range(len(z))) % P
              for i in range(y[0][n])] for z in cycles(x, n)]
    bound = [list(col) for col in zip(*y[1][n - 1])] if n > 0 else []
    return rank(image + bound) - rank(bound)

def fill_in_count(p):
    """Morphisms c : Z -> Z completing (id, id) on X --0--> Y -> Z -> X[1].

    Model in D(F_p) = graded vector spaces with X = F_p, Y = F_p[1], so that
    Z = Y + X[1] has both summands in degree -1, g = inclusion of Y and
    h = projection to X[1]; conditions: c g = g and h c = h.
    """
    g = [[1], [0]]
    h = [[0, 1]]
    count = 0
    for a, b, c, d in product(range(p), repeat=4):
        m = [[a, b], [c, d]]
        if matmul(m, g, p) == g and matmul(h, m, p) == h:
            count += 1
    return count

def identity_map(x):
    """The identity chain map of a complex x."""
    return [[[int(i == j) for j in range(k)] for i in range(k)] for k in x[0]]

def main():
    rng = random.Random(2024)
    trials, d2_ok, les_ok, qis_ok, quasi = 200, 0, 0, 0, 0
    for t in range(trials):
        x = random_complex(rng)
        if t % 4 == 0:  # every fourth example: the identity, a quasi-iso
            y, f = x, identity_map(x)
        else:
            y = random_complex(rng)
            f = random_chain_map(rng, x, y)
        c = cone(x, y, f)
        d2_ok += all(not any(map(any, matmul(c[1][n + 1], c[1][n])))
                     for n in range(len(c[1]) - 1))
        hx, hy, hc = cohomology(x), cohomology(y), cohomology(c)
        length = len(hx)
        rk = [rank_on_cohomology(x, y, f, n) for n in range(length)] + [0]
        hx_ = hx + [0]
        les_ok += all(hc[n + 1] == hy[n] - rk[n] + hx_[n + 1] - rk[n + 1]
                      for n in range(length))
        is_qis = hx == hy and all(rk[n] == hx[n] for n in range(length))
        quasi += is_qis
        qis_ok += is_qis == (sum(hc) == 0)
    print(f"Chain maps of random complexes over F_{P}, degrees 0..3: {trials}")
    print(f"  cones with d o d = 0:                     {d2_ok}/{trials}")
    print(f"  dimension formula (long exact sequence):  {les_ok}/{trials}")
    print(f"  'quasi-iso <=> acyclic cone' consistent:  {qis_ok}/{trials}"
          f"  ({quasi} quasi-isos)")
    print()
    print("Fill-ins c completing (id, id) for X --0--> Y -> Y + X[1] -> X[1]")
    print("in D(F_p), X = F_p, Y = F_p[1] (c = [[1, t], [0, 1]], t free):")
    print("  " + ", ".join(f"p = {p}: {fill_in_count(p)}" for p in (2, 3, 5)))
    print()
    print("Epistemic status: exact arithmetic mod 101 on 200 pseudo-random")
    print("examples (seeded), plus an exhaustive count over 2 x 2 matrices.")
    print("This is evidence that the cone construction behaves as the lesson")
    print("proves (exactness, cones detect quasi-isomorphisms, non-unique")
    print("fill-ins); random examples over one field do not prove it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The random checks are exact computations on finitely many examples over one field — evidence, not proof. The count of fill-ins is exhaustive for the primes shown.

Exercises

1. Triangulated categories

Warm-upHuman

Suppose $X \xrightarrow{u} Y \xrightarrow{v} Z \xrightarrow{w} X[1]$ is distinguished. Which triangle is distinguished by the rotation axiom TR2?

Choose one

Y \xrightarrow{v} Z \xrightarrow{w} X[1] \xrightarrow{-u[1]} Y[1]

Y \xrightarrow{v} Z \xrightarrow{w} X[1] \xrightarrow{u[1]} Y[1]

Z \xrightarrow{v} Y \xrightarrow{u} X \xrightarrow{w} Z[1]

X[1] \xrightarrow{u[1]} Y[1] \xrightarrow{v[1]} Z[1] \xrightarrow{w[1]} X[2]

2. Triangulated categories

Warm-upHuman

Over a field $k$ , let $f : k^3 \to k^5$ be a linear map of rank $2$ , viewed as a morphism in $D(k)$ between complexes concentrated in degree $0$ . What is $\dim H^{-1}(C(f)) + \dim H^0(C(f))$ for its cone?

3. Triangulated categories

CoreHuman

In the proof that every monomorphism $u : X \to Y$ in a triangulated category splits, we deduce $w = 0$ from $u[1]\, w = 0$ . Which fact justifies cancelling $u[1]$ ?

Choose one

u[1]

is a monomorphism, because the shift

[1]

is an equivalence and equivalences preserve monomorphisms

u[1]

is an isomorphismEvery map into

X[1]

is zeroThe octahedral axiom

4. Triangulated categories

CoreHuman

Apply $\operatorname{Hom}(\Z/2, -)$ to the distinguished triangle $\Z \xrightarrow{2} \Z \to \Z/2 \xrightarrow{\delta} \Z[1]$ in $D(\mathrm{Ab})$ . What is the induced map $\delta_* : \operatorname{Hom}(\Z/2, \Z/2) \to \operatorname{Hom}(\Z/2, \Z[1])$ ?

Choose one

An isomorphism

\Z/2 \to \Z/2

The zero mapA map

\Z/2 \to 0

, since

\operatorname{Hom}(\Z/2, \Z[1]) = 0

Multiplication by

2

5. Triangulated categories

CoreComputational

In $D(\mathbb{F}_5)$ take $X = \mathbb{F}_5$ , $Y = \mathbb{F}_5[1]$ and the zero map $X \to Y$ , with cone $Z = Y \oplus X[1]$ as in the lesson. How many morphisms $c : Z \to Z$ make $(\mathrm{id}_X, \mathrm{id}_Y, c)$ a morphism of triangles?

6. Triangulated categories

StretchHuman

Which of these triangulated categories are also abelian? (Choose all that apply.)

Choose all that apply

D(k)

for a field

k

D(\mathrm{Ab})

K(\mathrm{Ab})

D^b(kQ)

for the quiver

Q = (1 \to 2)

7. Triangulated categories

CoreHuman

For the standard t-structure on $D(\mathcal{A})$ , which subcategory is the heart?

Choose one

The complexes with

H^i = 0

for all

i \ne 0

; it is equivalent to

\mathcal{A}

via

X \mapsto H^0(X)

The acyclic complexes

D^{\le 0}

, the complexes with

H^i = 0

for

i > 0

The complexes of projective objects

8. Triangulated categories

CoreFormal

Which Lean statement formalises “in a pretriangulated category, every monomorphism is split”? (C carries the instances of a pretriangulated category.)

Choose one

theorem t {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono ftheorem t {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : Mono ftheorem t {X Y : C} (f : X ⟶ Y) : Mono ftheorem t {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f

9. Triangulated categories

StretchComputational

A linear map $f : \mathbb{Q}^n \to \mathbb{Q}^m$ , viewed in $D(\mathbb{Q})$ in degree $0$ , has cone $C(f) = (\mathbb{Q}^n \xrightarrow{f} \mathbb{Q}^m)$ in degrees $-1, 0$ . Write cone_cohomology(matrix, n) that returns [dim H^-1, dim H^0], where matrix is the list of the $m$ rows of $f$ (each of length n; it may be empty if $m = 0$ ). Use exact rational arithmetic (fractions.Fraction) to compute the rank.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"The cone construction is functorial." TR3 asserts that a fill-in exists; it is not unique (the worked example has a whole line of them), and the axioms give no cone functor on the category of morphisms. Even in $K(\mathcal{A})$ , the map of cones induced by a square commuting up to homotopy depends on the chosen homotopy. Functorial cones are recovered only in enhancements (dg-categories, stable ∞-categories).

Misconception

"Every triangulated category is the homotopy category of a stable ∞-category (or a stable model category, or a dg-category)." Muro, Schwede and Strickland (2007) found triangulated categories without such models. The triangulated axioms are strictly weaker than having an enhancement.

Misconception

"Distinguished triangles are just short exact sequences." A short exact sequence $0 \to A \to B \to C \to 0$ in $\mathcal{A}$ gives a triangle in $D(\mathcal{A})$ , but triangles are far more general: $X \xrightarrow{u} Y$ need not be a monomorphism (in fact non-split monomorphisms do not exist in $\mathcal{T}$ ), and the connecting map $C \to A[1]$ is part of the data — two triangles with the same three objects can be non-isomorphic.

Misconception

"The octahedral axiom follows from the others." No proof is known: whether TR4 follows from TR1–TR3 is a long-standing open question, so it is assumed as an axiom. (It holds in every triangulated category that comes from an enhancement.) Most structural results — Verdier quotients, gluing of t-structures — use it.

Misconception

"A triangulated category is a special kind of abelian category." The two notions are nearly disjoint: by Corollary 5 a triangulated category that is abelian is semisimple. Abelian categories sit inside triangulated ones as hearts of t-structures.

ViewpointsH

Viewpoints

Topology— Cofibre sequences and stable homotopy

For a map of pointed spaces $f : X \to Y$ , the mapping cone $C_f = Y \cup_f CX$ gives the Puppe sequence $X \to Y \to C_f \to \Sigma X \to \Sigma Y \to \cdots$ , and for every space $W$ the sets $[W, -]$ form an exact sequence, as do $[-, W]$ . In the stable homotopy category, where $\Sigma$ is inverted, these become distinguished triangles, and a cohomology theory $E^*$ is exactly a cohomological functor commuting with the shift. Brown representability — every such theory is represented by a spectrum — has a triangulated generalisation (Neeman). The octahedral axiom is the homotopical third isomorphism theorem $C_{gf} / C_f \simeq C_g$ . Historically, the stable homotopy category is the second birthplace of triangulated categories.

Geometry— Perverse sheaves and stability conditions

For a complex algebraic variety $X$ , the derived category $D^b_c(X)$ of constructible sheaves carries, besides the standard t-structure, the perverse t-structure of Beilinson–Bernstein–Deligne–Gabber, whose heart is the abelian category of perverse sheaves. Its simple objects are the intersection cohomology complexes, which carry Poincaré duality on singular spaces; the decomposition theorem of BBD is formulated in this heart. Changing the t-structure changes which abelian category one sees inside the same triangulated category — a phenomenon geometers now study systematically through Bridgeland stability conditions, whose hearts vary continuously over a complex manifold. See algebraic geometry and sheaves.

Algebra— Stable module categories and tilting

For a self-injective algebra (for example a group algebra $kG$ ), the stable module category is triangulated, with $\Omega^{-1}$ as shift; Happel proved that $D^b(\mathrm{mod}\,A)$ for a finite-dimensional algebra of finite global dimension is equivalent to the stable module category of its repetitive algebra. A derived equivalence $D^b(\mathrm{mod}\,A) \simeq D^b(\mathrm{mod}\,B)$ , such as one given by tilting, exhibits $\mathrm{mod}\,B$ as a second heart inside the triangulated category of $A$ : the same triangulated category, seen through a different t-structure. For a Dynkin quiver $Q$ , Happel described $D^b(kQ)$ completely by the mesh category of $\Z Q$ (see quiver representations).

Physics— Branes and their bound states (heuristic)

In Douglas's proposal for D-branes on Calabi–Yau manifolds, branes are objects of a triangulated category and a distinguished triangle $A \to B \to C \to A[1]$ describes $C$ as a bound state of $B$ and an anti-brane of $A$ , formed or decaying as moduli vary ("Π-stability"). Bridgeland's stability conditions are the mathematical formalisation of this idea. The physics is a heuristic guide, not a proof: the mathematical theory stands on its own axioms.

Category theory— Localisation and the axioms' weak spot

Categorically, a triangulated category is an additive category with a suspension and a class of "exact triangles"; Verdier quotients $\mathcal{T}/\mathcal{S}$ by thick subcategories are localisations, and this is how $D(\mathcal{A}) = K(\mathcal{A})/K_{\mathrm{acyc}}$ is built. The axioms' weak spot — non-unique fill-ins, hence no functorial cones and no homotopy (co)limits — is the reason for enhancements: in a stable ∞-category, cones are colimits and are unique up to a contractible space of choices.

History & global context

History and global context

1950s. Dieter Puppe (Germany) introduces cofibre sequences (1958). Grothendieck's programme in algebraic geometry needs a home for complexes of sheaves.
1962–63. Puppe, for stable homotopy theory, and Jean-Louis Verdier, in his thesis supervised by Grothendieck (notes 1963, defence 1967, publication 1996), independently axiomatise triangulated categories; Verdier adds the octahedral axiom and constructs quotients.
1960s–70s. J. Michael Boardman constructs the stable homotopy category; Freyd poses the generating hypothesis (1966).
1982. Alexander Beilinson, Joseph Bernstein, Pierre Deligne and Ofer Gabber introduce t-structures and perverse sheaves (Faisceaux pervers), connecting with the Riemann–Hilbert correspondence of Kashiwara and Mebkhout and the intersection cohomology of Goresky and MacPherson.
1987–88. Dieter Happel (Germany) develops triangulated categories in the representation theory of finite-dimensional algebras.
1990s–2000s. Amnon Neeman (Israel/Australia) proves Brown representability for compactly generated categories (1996) and writes the standard monograph (2001). Tom Bridgeland (UK) introduces stability conditions (2007); Paul Balmer (Switzerland/USA) introduces tensor-triangular geometry (2005); Fernando Muro, Stefan Schwede, Neil Strickland exhibit triangulated categories without models (2007).

What replaces short exact sequences?

Triangles that roll

Verdier's axioms

Examples and a worked long exact sequence

First consequences of the axioms

The landscape: enhancements, stability, open questions

Triangulated categories in Lean and Mathlib

Cones over a finite field

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading