ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Hard Lefschetz splitting for a three-degree complex

Example

Let $k$ be a field and let $T = D^{b} ({v e c t}_{k}^{f d})$ be the bounded derived category of finite-dimensional $k$ -vector spaces with its canonical t-structure. Take $K = k [2] \oplus k \oplus k [- 2] \in T,$ and let $L : K \to K [2]$ identify the first summand $k [2]$ with the shifted second summand $k [2]$ of $K [2]$ , the second summand $k$ with the shifted third summand $k$ of $K [2]$ , and the third summand $k [- 2]$ with $0$ . Its nonzero t-cohomology objects are $H_{t}^{- 2} (K) = k, H_{t}^{0} (K) = k, H_{t}^{2} (K) = k,$ and for every $j \geq 0$ the map $H_{t}^{- j} (L^{j})$ is an isomorphism: $j = 0$ and $j = 2$ are the two Lefschetz steps, while for $j = 1$ and for $j \geq 3$ both sides are zero. Consequently the splitting of Hard Lefschetz splits a bounded t-structure complex returns exactly $K ≅ H_{t}^{- 2} (K) [2] \oplus H_{t}^{0} (K) \oplus H_{t}^{2} (K) [- 2] = k [2] \oplus k \oplus k [- 2] .$ This example tests the abstract splitting on the simplest complex with two hard Lefschetz steps; it does not test primitive-lift compatibility.

Facts & Assumptions

Given: A field $k$ , the category ${v e c t}_{k}^{f d}$ of finite-dimensional $k$ -vector spaces and its bounded derived category $T = D^{b} ({v e c t}_{k}^{f d})$ with the canonical t-structure, the object $K = k [2] \oplus k \oplus k [- 2]$ and the morphism $L : K \to K [2]$ described in the Example.

[F1]

Abelian and size structure of the coefficient category: finite-dimensional $k$ -vector spaces form the full subcategory of the abelian category $k - M o d$ (Modules over a ring form an abelian category) closed under kernels, cokernels and finite direct sums, as supplied by rank-nullity (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ), the first isomorphism theorem (First isomorphism theorem in an abelian category) and the dimension of a direct sum (If $V = ⨁_{i < n} U_{i}$ with every $U_{i}$ finite-dimensional, then $V$ is finite-dimensional and $\dim_{F} V = \sum_{i < n} \dim_{F} U_{i}$ ; in particular $\dim_{F} (U \oplus W) = \dim_{F} U + \dim_{F} W$ ); a finite-dimensional space is isomorphic to $k^{n}$ for $n = \dim_{k} V$ (Two finite-dimensional vector spaces over $F$ are linearly isomorphic if and only if they have the same dimension), so the category is essentially small and the standing size hypothesis of Derived category of an abelian category holds. Hence $T$ is triangulated (The derived category inherits a triangulated structure) and carries the canonical t-structure $T^{\leq 0} = {X : H^{i} (X) = 0 for i > 0}$ , $T^{\geq 0} = {X : H^{i} (X) = 0 for i < 0}$ on $D^{b}$ (Canonical t structure on a derived category, The canonical pair is a t structure), where $H^{i}$ denotes the cohomology functor on the derived category (Cohomology factors through the derived category).

[F2]

Boundedness: a bounded complex has cohomology vanishing outside some finite interval of degrees, so it lies in $T^{\leq n} \cap T^{\geq - n}$ for $n$ large; thus the canonical t-structure is bounded (Truncation functors, t-cohomology, amplitude and bounded t-structures).

[F3]

Heart and shift rules (t-cohomology is functorial, additive, shift-compatible and detects amplitude): an object of the heart satisfies $X ≅ H_{t}^{0} (X)$ and $H_{t}^{j} (X) = 0$ for $j \neq 0$ ; more generally $H_{t}^{j} (X [m]) ≅ H_{t}^{j + m} (X)$ naturally, and for a finite biproduct the structure maps identify $H_{t}^{j}$ of the sum with the direct sum of the $H_{t}^{j}$ of the summands.

[F4]

The hard Lefschetz splitting lemma: for a triangulated category with a bounded t-structure and a morphism $L : K \to K [2]$ with every $H_{t}^{- j} (L^{j})$ , $j \geq 0$ , an isomorphism, one has $K ≅ ⨁_{j} H_{t}^{j} (K) [- j]$ (Hard Lefschetz splits a bounded t-structure complex).

Verification

technique · direct

1.1givenF1F2F3

By (F1) the category $T = D^{b} ({v e c t}_{k}^{f d})$ is triangulated and carries the canonical t-structure, which is bounded by (F2). The complex $k$ concentrated in degree zero lies in the heart, since $H^{i} (k) = 0$ for $i \neq 0$ ; hence $H_{t}^{0} (k) ≅ k$ and $H_{t}^{j} (k) = 0$ for $j \neq 0$ by (F3).

2.1step 1.1F3

Since $k [m]$ satisfies $H_{t}^{j} (k [m]) ≅ H_{t}^{j + m} (k)$ by the shift rule (F3), it has $H_{t}^{j} (k [m]) ≅ k$ for $j = - m$ and vanishing $H_{t}^{j}$ otherwise. The object $K = k [2] \oplus k \oplus k [- 2]$ is a finite biproduct in the additive category $T$ (Biproduct), so additivity of $H_{t}^{j}$ gives $H_{t}^{- 2} (K) ≅ k$ , $H_{t}^{0} (K) ≅ k$ , $H_{t}^{2} (K) ≅ k$ , and $H_{t}^{j} (K) = 0$ for all other $j$ ; in particular $H_{t}^{- 1} (K) = 0$ and $H_{t}^{j} (K) = 0$ for $j \geq 3$ .

3.1step 2.1given

The description of $L$ is a well-defined morphism: $K [2] = k [4] \oplus k [2] \oplus k$ , and $L$ has the canonical isomorphisms $k [2] \overset{≅}{\to} k [2]$ and $k \overset{≅}{\to} k$ as its components onto the second and third summands of $K [2]$ , all other components being zero, so the third summand $k [- 2]$ is carried to $0$ . Its iterate $L^{2} = L [2] \circ L$ maps $K$ to $K [4] = k [6] \oplus k [4] \oplus k [2]$ , carrying the first summand $k [2]$ isomorphically onto the third summand $k [2]$ of $K [4]$ (first through the second summand of $K [2]$ , then through the third summand of $K [4]$ ) and killing the other two summands; and $L^{0} = 1_{K}$ .

4.1step 2.1step 3.1F3

Hence $H_{t}^{- j} (L^{j})$ is an isomorphism for every $j \geq 0$ . For $j = 0$ it is the identity of $H_{t}^{0} (K) = k$ ; for $j = 1$ its source $H_{t}^{- 1} (K)$ is zero and its target $H_{t}^{- 1} (K [2]) ≅ H_{t}^{1} (K)$ is zero; for $j = 2$ it is the isomorphism induced on $H_{t}^{- 2}$ by the nonzero component $k [2] \overset{≅}{\to} k [2]$ of $L^{2}$ , between $H_{t}^{- 2} (K) ≅ k$ and $H_{t}^{- 2} (K [4]) ≅ H_{t}^{2} (K) ≅ k$ ; and for $j \geq 3$ the source $H_{t}^{- j} (K)$ and the target $H_{t}^{- j} (K [2 j]) ≅ H_{t}^{j} (K)$ both vanish. A map between zero objects is an isomorphism, so the hard Lefschetz hypothesis holds in every case.

5.1step 1.1step 4.1F4∎

The hypotheses of (F4) are therefore satisfied: $T$ is triangulated with a bounded t-structure and $L$ satisfies the hard Lefschetz condition. The lemma yields $K ≅ ⨁_{j} H_{t}^{j} (K) [- j] = H_{t}^{- 2} (K) [2] \oplus H_{t}^{0} (K) \oplus H_{t}^{2} (K) [- 2] = k [2] \oplus k \oplus k [- 2]$ , which is the displayed $K$ , so the abstract splitting returns exactly the direct sum of the shifted t-cohomology objects and the example checks no more than that.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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)
P. Deligne, «Théorème de Lefschetz et critères de dégénérescence de suites spectrales», Publ. Math. IHÉS 35 (1968) 107–126 (complete numdam PDF) (standard reference, not scraped)