LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Truncation triangles are essentially unique and give adjoint truncation functors

Statement

Let $(T^{\leq 0}, T^{\geq 0})$ be a t-structure on a triangulated category $T$ , with truncations as in Truncation functors, t-cohomology, amplitude and bounded t-structures.

(i) Essential uniqueness. For every $X$ and $n$ , every distinguished triangle $A \to X \to B \to A [1]$ with $A \in T^{\leq n}$ and $B \in T^{\geq n + 1}$ is isomorphic to the truncation triangle $τ_{\leq n} X \to X \to τ_{\geq n + 1} X \to τ_{\leq n} X [1]$ by an isomorphism of triangles whose middle component is the identity of $X$ ; this isomorphism is unique.

(ii) Adjunction and orthogonality. The assignment $X \mapsto τ_{\leq n} X$ is a functor and for $T \in T^{\leq n}$ the map $Hom (T, τ_{\leq n} X) \to Hom (T, X)$ , $f \mapsto (τ_{\leq n} X \to X) \circ f$ , is a bijection natural in $X$ ; dually $Hom (τ_{\geq n} X, T) \to Hom (X, T)$ is a bijection for $T \in T^{\geq n}$ . Moreover $Hom (T^{\leq n}, T^{\geq n + 1}) = 0$ for every $n$ .

(iii) Aisle criteria. $X \in T^{\leq n}$ if and only if $τ_{\leq n} X \to X$ is an isomorphism, if and only if $τ_{\geq n + 1} X = 0$ , if and only if $Hom (X, T^{\geq n + 1}) = 0$ ; dually $X \in T^{\geq n}$ if and only if $X \to τ_{\geq n} X$ is an isomorphism, if and only if $τ_{\leq n - 1} X = 0$ , if and only if $Hom (T^{\leq n - 1}, X) = 0$ .

(iv) Extensions, direct sums and iteration. In a distinguished triangle $X \to Y \to Z \to X [1]$ , if $X, Z \in T^{\leq n}$ (respectively $T^{\geq n}$ ), then $Y$ lies in the same aisle. If $X, Y \in T^{\leq n}$ then $Z \in T^{\leq n}$ , while if $Y, Z \in T^{\leq n}$ then $X \in T^{\leq n + 1}$ ; dually, if $Y, Z \in T^{\geq n}$ then $X \in T^{\geq n}$ , while if $X, Y \in T^{\geq n}$ then $Z \in T^{\geq n - 1}$ . Also, a finite direct sum lies in $T^{\leq n}$ (respectively $T^{\geq n}$ ) if and only if each summand does. For $m \leq n$ there are canonical isomorphisms $τ_{\leq m} τ_{\leq n} ≅ τ_{\leq m}$ , $τ_{\leq n} τ_{\leq m} ≅ τ_{\leq m}$ , $τ_{\geq n} τ_{\geq m} ≅ τ_{\geq n}$ and $τ_{\geq m} τ_{\geq n} ≅ τ_{\geq n}$ compatible with the truncation maps, and $τ_{\leq m} τ_{\geq n} = 0$ when $m < n$ .

Facts & Assumptions

Given: A t-structure $(T^{\leq 0}, T^{\geq 0})$ on a triangulated category $T$ , with $T^{\leq n} = T^{\leq 0} [- n]$ , $T^{\geq n} = T^{\geq 0} [- n]$ and $Hom (T^{\leq 0}, T^{\geq 1}) = 0$ (Canonical t structure on a derived category, Truncation functors, t-cohomology, amplitude and bounded t-structures).

[F1]

For every object $W$ and distinguished triangle $X \to Y \to Z \to X [1]$ , the sequences $T (W, X) \to T (W, Y) \to T (W, Z) \to T (W, X [1])$ and, dually, $T (Z, W) \to T (Y, W) \to T (X, W) \to T (Z [- 1], W)$ are exact (Long exact Hom sequences of a distinguished triangle).

[F2]

Orthogonality and monotonicity: $Hom (T^{\leq n}, T^{\geq n + 1}) = 0$ for every $n$ by the t-structure axiom $Hom (T^{\leq 0}, T^{\geq 1}) = 0$ and the shift conventions, since a map $X \to Y$ with $X \in T^{\leq n}$ and $Y \in T^{\geq n + 1}$ is a map $X [n] \in T^{\leq 0} \to Y [n] \in T^{\geq 1}$ ; moreover $T^{\leq m} \subseteq T^{\leq n}$ and $T^{\geq n} \subseteq T^{\geq m}$ whenever $m \leq n$ , because $T^{\leq 0} [1] \subseteq T^{\leq 0}$ and $T^{\geq 0} [- 1] \subseteq T^{\geq 0}$ (Canonical t structure on a derived category).

[F3]

TR3: every commutative square on the first maps of two distinguished triangles extends to a morphism of triangles (Triangulated-category axiom TR3, Morphism and isomorphism of triangles); and a morphism of triangles with two adjacent isomorphism components has its third component an isomorphism (The triangulated five lemma).

[F4]

The triangles $X \overset{1}{\to} X \to 0 \to X [1]$ and $X \to 0 \to X [1] \overset{1}{\to} X [1]$ are distinguished, and distinguished triangles are closed under translations and rotations (Zero and split triangles are distinguished, Distinguished triangles are closed under shifts and both rotations).

[F5]

The triangulated category is additive, so finite biproducts exist, and $T (X \oplus Y, W) ≅ T (X, W) \oplus T (Y, W)$ and $T (W, X \oplus Y) ≅ T (W, X) \oplus T (W, Y)$ (Additive category, Biproduct).

Proof

technique · direct

1.1F1F2algebra

Let $A \overset{a}{\to} X \overset{b}{\to} B \to A [1]$ be distinguished with $A \in T^{\leq n}$ and $B \in T^{\geq n + 1}$ . For $T \in T^{\leq n}$ , the exact segment $Hom (T, B [- 1]) \to Hom (T, A) \overset{a_{*}}{\to} Hom (T, X) \to Hom (T, B)$ has zero outer terms by [F2], since $B [- 1] \in T^{\geq n + 2}$ . Thus $a_{*}$ is bijective. Dually, for $T \in T^{\geq n + 1}$ the segment $Hom (A [1], T) \to Hom (B, T) \overset{b^{*}}{\to} Hom (X, T) \to Hom (A, T)$ has zero outer terms, since $A [1] \in T^{\leq n - 1}$ , so $b^{*}$ is bijective.

1.2F3F4algebra

If $A \overset{f}{\to} B \to 0 \to A [1]$ is a distinguished triangle, then $f$ is an isomorphism. Indeed, the triangle $B \overset{1}{\to} B \to 0 \to B [1]$ is distinguished by [F4], and $(f, 1_{B}, 0)$ is a morphism of triangles from the first to the second, commuting with all three arrows; the components $1_{B}$ and $0 \to 0$ are adjacent isomorphisms, so $f$ is an isomorphism by [F3].

2.1step 1.1F3algebra

Claim (i). Let $A \overset{a}{\to} X \overset{b}{\to} B \to A [1]$ be distinguished with $A \in T^{\leq n}$ , $B \in T^{\geq n + 1}$ , and let $P \overset{p}{\to} X \overset{q}{\to} Q \to P [1]$ be the truncation triangle. By step 1.1 applied to the truncation triangle with $T = A$ there is a unique $f : A \to P$ with $p f = a$ , and applied to the given triangle with $T = P$ there is a unique $f^{'} : P \to A$ with $a f^{'} = p$ . Then $p (f f^{'}) = a f^{'} = p = p 1_{P}$ , and $f f^{'} = 1_{P}$ because $Hom (P, P) \to Hom (P, X)$ is injective by step 1.1 applied to the truncation triangle with $T = P$ ; symmetrically $f^{'} f = 1_{A}$ using the given triangle with $T = A$ . So $f$ is an isomorphism. By TR3 [F3] the commutative square $(f, 1_{X})$ extends to a morphism of triangles $(f, 1_{X}, g)$ , which is an isomorphism of triangles because $f$ and $1_{X}$ are adjacent isomorphism components, and its middle component is the identity of $X$ . For uniqueness, let $(f^{''}, 1_{X}, g^{''})$ be another such isomorphism; then $p f^{''} = a$ , so $f^{''} = f$ by the uniqueness in step 1.1 applied to the truncation triangle with $T = A$ . Hence the composite of $(f^{''}, 1_{X}, g^{''})$ with the inverse of $(f, 1_{X}, g)$ is an automorphism $(1_{A}, 1_{X}, d)$ of the given triangle; it satisfies $d b = b$ , and $Hom (B, B) \to Hom (X, B)$ , $v \mapsto v b$ , is injective by step 1.1 applied to the given triangle with $T = B \in T^{\geq n + 1}$ , so $d = 1_{B}$ and the isomorphism over $X$ is unique.

2.2step 1.1F2algebra

Claim (ii), the $\leq$ side. Fix the truncation triangle $P_{X} \overset{p_{X}}{\to} X \overset{q_{X}}{\to} Q_{X} \to P_{X} [1]$ for every $X$ . For $f : X \to Y$ , the composite $f p_{X}$ lies in $Hom (P_{X}, Y)$ , and step 1.1 applied to the truncation triangle of $Y$ with $T = P_{X} \in T^{\leq n}$ gives a unique map $τ_{\leq n} f : P_{X} \to P_{Y}$ with $p_{Y} (τ_{\leq n} f) = f p_{X}$ . This makes $τ_{\leq n}$ a functor: $τ_{\leq n} (1_{X}) = 1_{P_{X}}$ by uniqueness, and for $X \overset{f}{\to} Y \overset{h}{\to} Z$ both $τ_{\leq n} (h f)$ and $τ_{\leq n} h \circ τ_{\leq n} f$ have the same composite with $p_{Z}$ , so they are equal by the uniqueness. The map $Hom (T, P_{X}) \to Hom (T, X)$ , $u \mapsto p_{X} u$ , is a bijection for $T \in T^{\leq n}$ by step 1.1 applied to the truncation triangle of $X$ , and it is natural in $X$ because both $p_{Y} (τ_{\leq n} f u)$ and $f (p_{X} u)$ equal $(f p_{X}) u$ . Applying the same argument with arrows reversed to the truncation triangle at $n - 1$ , whose third vertex is $τ_{\geq n} X$ , makes $X \mapsto τ_{\geq n} X$ a functor and gives a bijection $Hom (τ_{\geq n} X, T) \to Hom (X, T)$ for $T \in T^{\geq n}$ . The final vanishing $Hom (T^{\leq n}, T^{\geq n + 1}) = 0$ is [F2].

2.3step 1.1step 1.2F1F2

Claim (iii), the $\leq$ side. Let $P \overset{p}{\to} X \overset{q}{\to} Q \to P [1]$ be the truncation triangle. The following are equivalent: (a) $X \in T^{\leq n}$ ; (b) $p$ is an isomorphism; (c) $Q = 0$ ; (d) $Hom (X, T^{\geq n + 1}) = 0$ . (a) $\Rightarrow$ (d) is [F2]. (a) $\Rightarrow$ (c): if $X \in T^{\leq n}$ then $q \in Hom (X, Q) = 0$ by [F2], so $q^{*} (1_{Q}) = q = 0 = q^{*} (0)$ , and $q^{*} : Hom (Q, Q) \to Hom (X, Q)$ is injective by step 1.1 applied to the truncation triangle with $T = Q \in T^{\geq n + 1}$ , hence $1_{Q} = 0$ and $Q$ is a zero object. (c) $\Rightarrow$ (b): if $Q = 0$ , step 1.2 applied to the triangle $P \to X \to 0 \to P [1]$ makes $p$ an isomorphism. (b) $\Rightarrow$ (c): if $p$ is an isomorphism, then in the exact sequence $Hom (Q, Q) \overset{q^{*}}{\to} Hom (X, Q) \overset{p^{*}}{\to} Hom (P, Q)$ of [F1] the map $p^{*}$ is injective (a map $φ$ with $φ p = 0$ vanishes because $p$ is an isomorphism), so $im (q^{*}) = 0$ ; since $q^{*}$ is a bijection by step 1.1, $1_{Q} = 0$ and $Q = 0$ . (d) $\Rightarrow$ (c): if $Hom (X, T^{\geq n + 1}) = 0$ then $q = 0$ , so $q^{*} (1_{Q}) = 0 = q^{*} (0)$ and injectivity of $q^{*}$ gives $1_{Q} = 0$ , i.e. $Q = 0$ . Finally (b) $\Rightarrow$ (a): if $p$ is an isomorphism then $X ≅ P$ and $P \in T^{\leq n}$ , so $X \in T^{\leq n}$ .

2.4step 1.1step 1.2F2F4

Claim (iii), the $\geq$ side, by the same arguments with the roles of the two maps interchanged. Let $P \overset{p}{\to} X \overset{q}{\to} Q \to P [1]$ be the truncation triangle at $n - 1$ , so that $P = τ_{\leq n - 1} X$ and $Q = τ_{\geq n} X$ . Then: (a $^{'}$ ) $X \in T^{\geq n}$ implies $Hom (T^{\leq n - 1}, X) = 0$ by [F2], hence $p = 0$ and $p_{*} (1_{P}) = p = 0 = p_{*} (0)$ with $p_{*}$ injective by step 1.1, so $P = 0$ ; (b $^{'}$ ) $P = 0$ makes the triangle $X \to Q \to 0 \to X [1]$ distinguished by [F4], so $X \to Q$ is an isomorphism by step 1.2 and $X ≅ Q \in T^{\geq n}$ ; (c $^{'}$ ) if $X \to Q$ is an isomorphism then $q p = 0$ forces $p = 0$ and hence $1_{P} = 0$ as above, so $P = 0$ ; (d $^{'}$ ) if $Hom (T^{\leq n - 1}, X) = 0$ then $p = 0$ and $1_{P} = 0$ as in (a $^{'}$ ), so $P = 0$ and $X \in T^{\geq n}$ by (b $^{'}$ ); and $X \in T^{\geq n}$ implies $Hom (T^{\leq n - 1}, X) = 0$ by [F2]. This proves $X \in T^{\geq n}$ if and only if $X \to τ_{\geq n} X$ is an isomorphism, if and only if $τ_{\leq n - 1} X = 0$ , if and only if $Hom (T^{\leq n - 1}, X) = 0$ .

3.1step 2.3step 2.4F1F2F4

Claim (iv), extensions: let $X \to Y \to Z \to X [1]$ be distinguished. If $X, Z \in T^{\geq n}$ , then for $W \in T^{\leq n - 1}$ exactness of $Hom (W, X) \to Hom (W, Y) \to Hom (W, Z)$ and orthogonality force $Hom (W, Y) = 0$ , hence $Y \in T^{\geq n}$ by step 2.4. Dually, $X, Z \in T^{\leq n}$ force $Y \in T^{\leq n}$ using $Hom (Z, W) \to Hom (Y, W) \to Hom (X, W)$ and step 2.3. Applying these extension statements to the rotations $Y \to Z \to X [1] \to$ and $Z [- 1] \to X \to Y \to$ , and using $X [1] \in T^{\leq n - 1}$ when $X \in T^{\leq n}$ and $Z [- 1] \in T^{\geq n + 1}$ when $Z \in T^{\geq n}$ , gives the four other bounds in (iv).

3.2step 2.3step 2.4F5

Claim (iv), direct sums: for objects $X, Y$ one has $Hom (X \oplus Y, W) ≅ Hom (X, W) \oplus Hom (Y, W)$ and $Hom (W, X \oplus Y) ≅ Hom (W, X) \oplus Hom (W, Y)$ by [F5]. Hence $X \oplus Y \in T^{\leq n}$ implies $Hom (X, W) = 0$ for every $W \in T^{\geq n + 1}$ , as a direct summand of the vanishing group $Hom (X \oplus Y, W)$ , so $X \in T^{\leq n}$ and likewise $Y \in T^{\leq n}$ by step 2.3; conversely if $X, Y \in T^{\leq n}$ then every such $Hom (X \oplus Y, W)$ vanishes and $X \oplus Y \in T^{\leq n}$ by step 2.3. The same argument with the second displayed bijection and step 2.4 gives the statement for $T^{\geq n}$ ; the empty direct sum is the zero object and the claims are vacuous for it.

3.3step 2.2step 2.3step 2.4F2

Claim (iv), iteration: let $m \leq n$ . Since $τ_{\leq m} X \in T^{\leq n}$ , its truncation map $τ_{\leq n} τ_{\leq m} X \to τ_{\leq m} X$ is an isomorphism by step 2.3. Put $P = τ_{\leq m} τ_{\leq n} X$ and $Q = τ_{\leq m} X$ , and let $α : P \to X$ and $β : Q \to X$ be the composites of their truncation maps. For every $T \in T^{\leq m}$ , composition with either $α$ or $β$ is a bijection onto $Hom (T, X)$ by step 2.2 and $T^{\leq m} \subseteq T^{\leq n}$ . Thus there are unique $d : P \to Q$ and $v : Q \to P$ with $β d = α$ and $α v = β$ , and injectivity gives $d v = 1_{Q}$ and $v d = 1_{P}$ . These isomorphisms commute with the maps to $X$ and are natural by uniqueness. Dually, since $τ_{\geq n} X \in T^{\geq m}$ , the map $τ_{\geq n} X \to τ_{\geq m} τ_{\geq n} X$ is an isomorphism by step 2.4; the dual factorization argument identifies $τ_{\geq n} τ_{\geq m} X$ with $τ_{\geq n} X$ , compatibly with the maps from $X$ . Finally, if $m < n$ , then $τ_{\geq n} X \in T^{\geq m + 1}$ , so $τ_{\leq m} τ_{\geq n} X = 0$ by step 2.4.

4.1step 2.1step 2.2step 2.3step 2.4step 3.1step 3.2step 3.3∎

Steps 2.1, 2.2, 2.3, 2.4, 3.1, 3.2 and 3.3 prove claims (i), (ii), (iii) and (iv) respectively, including the uniqueness of the isomorphism in (i), the naturality and the dual statements in (ii), all four equivalent formulations in (iii), and the closure, direct-sum and iteration statements in (iv).

Depends on

Used by

Cited to discharge well-definedness by Truncation functors, t-cohomology, amplitude and bounded t-structures.

Dependency tree · two levels

27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. A. Beilinson, J. Bernstein and P. Deligne, «Faisceaux pervers», Astérisque 100 (1982), Société Mathématique de France (complete numdam PDF) (standard reference, not scraped)