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.

Graded hard Lefschetz has a canonical primitive decomposition

Statement

Let $H^{j}$ , $j \in Z$ , be objects of an abelian category, zero for all but finitely many $j$ , and let $L_{j} : H^{j} \to H^{j + 2}$ be morphisms whose iterates give isomorphisms $L^{r} : H^{- r} \to H^{r}$ for every $r \geq 0$ , with $L^{0} = 1_{H^{0}}$ . Put $P^{- r} : = \ker (L^{r + 1} : H^{- r} \to H^{r + 2})$ for $r \geq 0$ , and $P^{- r} = 0$ for $r < 0$ . Then for every $r \geq 0$ the powers of $L$ induce finite direct sum decompositions $H^{- r} = ⨁_{j \geq 0} L^{j} P^{- r - 2 j}, H^{r} = ⨁_{j \geq 0} L^{r + j} P^{- r - 2 j},$ where $L^{j} P^{- r - 2 j}$ denotes the image of the restriction of $L^{j}$ to the subobject $P^{- r - 2 j} \subseteq H^{- r - 2 j}$ , and likewise for $L^{r + j} P^{- r - 2 j}$ . Each displayed power $L^{j}$ or $L^{r + j}$ restricts to a monomorphism on its primitive source, and both decompositions are natural for morphisms commuting with $L$ . This is a decomposition statement for graded objects in an abelian category; it does not identify primitive objects with classes annihilated by an untruncated map on a derived splitting of a complex.

Facts & Assumptions

Given: Objects $H^{j}$ of an abelian category, zero for all but finitely many $j$ , morphisms $L_{j} : H^{j} \to H^{j + 2}$ , and the hypothesis that each iterate $L^{r} : H^{- r} \to H^{r}$ , $r \geq 0$ , is an isomorphism, with $L^{0} = 1_{H^{0}}$ ; the objects $P^{- r} = \ker (L^{r + 1} : H^{- r} \to H^{r + 2})$ for $r \geq 0$ and $P^{- r} = 0$ for $r < 0$ .

[F1]

Kernels and cokernels are the equalizers and coequalizers of a morphism with the zero morphism: the kernel inclusion $k$ of $f$ satisfies $f k = 0$ and every $h$ with $f h = 0$ factors uniquely as $h = k h^{'}$ , and any two kernels of the same morphism are canonically isomorphic over it (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Image and coimage in a category with kernels and cokernels).

[F2]

A composable triple $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ is a short exact sequence if and only if $i$ is a kernel of $p$ and $p$ is a cokernel of $i$ , and every epimorphism is the cokernel of its kernel (A short exact sequence is a kernel-cokernel pair, Exact sequence and short exact sequence in an abelian category, Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

[F3]

Splitting lemma: if $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ is a short exact sequence admitting $s : C \to B$ with $p s = 1_{C}$ , then there is a unique $π : B \to A$ with $π i = 1_{A}$ and $i π + s p = 1_{B}$ , so that $(B, i, s, π, p)$ is the biproduct diagram of $A$ and $C$ (Splitting lemma in an abelian category, Split short exact sequence in an abelian category, Biproduct).

[F4]

A monomorphism $f : X \to Y$ induces an isomorphism $X \to im (f)$ over $Y$ : by Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel the map $f$ itself is a kernel of its cokernel $coker (f)$ , while the image inclusion $im (f) \to Y$ is a kernel of $coker (f)$ by definition, and kernels of one morphism are unique up to a unique compatible isomorphism by [F1]. Consequently, if $X$ is the biproduct of $A$ and $B$ with injections $i_{A}, i_{B}$ , then applying this isomorphism to the biproduct identities exhibits $im (f)$ as the biproduct of $im (f i_{A})$ and $im (f i_{B})$ .

Proof

technique · induction on the number $j$ of peeled degree-two steps

1.1givenalgebra

For every $m \geq 2$ the map $L : H^{- m} \to H^{- m + 2}$ is a monomorphism, because $L^{m} = L^{m - 1} L$ is an isomorphism: if $L u = 0$ then $L^{m} u = L^{m - 1} L u = 0$ , hence $u = 0$ .

1.2givenalgebra

For every $r \geq 0$ the map $p : = L^{r + 1} : H^{- r} \to H^{r + 2}$ is an epimorphism and $s : = L (L^{r + 2})^{- 1} : H^{r + 2} \to H^{- r}$ satisfies $p s = 1_{H^{r + 2}}$ , because $p L = L^{r + 2}$ is an isomorphism: if $v p = 0$ then $v L^{r + 2} = v p L = 0$ , hence $v = 0$ , and $p s = L^{r + 1} L (L^{r + 2})^{- 1} = L^{r + 2} (L^{r + 2})^{- 1} = 1$ .

2.1F1F2F3F4step 1.1step 1.2construct

Fix $r \geq 0$ and let $i : P^{- r} \to H^{- r}$ be the kernel of $p = L^{r + 1}$ . Since $p$ is epic by step 1.2, [F2] makes $0 \to P^{- r} \overset{i}{\to} H^{- r} \overset{p}{\to} H^{r + 2} \to 0$ short exact. Its section $s = L (L^{r + 2})^{- 1}$ gives, by [F3], a projection $π : H^{- r} \to P^{- r}$ with $π i = 1$ , $i π + s p = 1$ and $π s = 0$ . Put $t = L : H^{- r - 2} \to H^{- r}$ and $g = L^{r + 2} : H^{- r - 2} \to H^{r + 2}$ . Then $g$ is an isomorphism, $s = t g^{- 1}$ , $p t = g$ and $π t = π s g = 0$ . Consequently $(i, t) : P^{- r} \oplus H^{- r - 2} \to H^{- r}$ has inverse $(π, g^{- 1} p)$ : the diagonal composites are identities, the off-diagonal composites vanish, and $i π + t g^{- 1} p = i π + s p = 1$ . Since $t$ is monic by step 1.1, [F4] identifies its source with its image. Hence this is the canonical decomposition $H^{- r} = P^{- r} \oplus L H^{- r - 2}$ . The endomorphism $s p$ projects onto the second summand, whereas its projection to the source $H^{- r - 2}$ is $g^{- 1} p$ .

3.1basestep 2.1

Base of the induction: for $j = 0$ the object $H^{- r}$ is the biproduct of $P^{- r} = L^{0} P^{- r}$ and $L^{1} H^{- r - 2} = L H^{- r - 2}$ . This is exactly the decomposition of step 2.1, so the assertion holds for $j = 0$ .

3.2ihstep 2.1

Induction hypothesis: fix $j \geq 0$ and assume the assertion for this $j$ , that is, $H^{- r}$ is the biproduct of $P^{- r}, L P^{- r - 2}, \dots, L^{j} P^{- r - 2 j}$ and $L^{j + 1} H^{- r - 2 j - 2}$ ; we must derive it for $j + 1$ .

4.1F4step 1.1step 2.1step 3.2algebra

Applying step 2.1 with $r$ replaced by $r + 2 j + 2$ gives the biproduct decomposition $H^{- r - 2 j - 2} = P^{- r - 2 j - 2} \oplus L H^{- r - 2 j - 4}$ . The map $L^{j + 1} : H^{- r - 2 j - 2} \to H^{- r}$ is a monomorphism, being a composite of the monomorphisms of step 1.1; by [F4] it carries this biproduct diagram to the biproduct diagram of its image, $im (L^{j + 1}) = L^{j + 1} P^{- r - 2 j - 2} \oplus L^{j + 1} (L H^{- r - 2 j - 4}) = L^{j + 1} P^{- r - 2 j - 2} \oplus L^{j + 2} H^{- r - 2 j - 4}$ . Substituting this into the biproduct of the induction hypothesis (step 3.2) gives that $H^{- r}$ is the biproduct of $P^{- r}, L P^{- r - 2}, \dots, L^{j + 1} P^{- r - 2 j - 2}$ and $L^{j + 2} H^{- r - 2 j - 4}$ , which is the assertion for $j + 1$ .

5.1step 1.1step 4.1givenalgebra

By induction (steps 3.1, 3.2 and 4.1) the biproduct decomposition of step 3.2 holds for every $j \geq 0$ . Since $H^{n} = 0$ for all sufficiently negative $n$ , choose $J$ with $H^{- r - 2 J - 2} = 0$ ; then the tail $L^{J + 1} H^{- r - 2 J - 2}$ vanishes, and $H^{- r}$ is the biproduct of $P^{- r}, L P^{- r - 2}, \dots, L^{J} P^{- r - 2 J}$ , i.e. the finite direct sum decomposition $H^{- r} = ⨁_{j \geq 0} L^{j} P^{- r - 2 j}$ of the Statement. Each restricted power $L^{j} ∣_{P^{- r - 2 j}}$ is a monomorphism, being for $j \geq 1$ a composite of the monomorphisms of step 1.1 and for $j = 0$ the primitive kernel inclusion.

6.1givenstep 5.1algebra

Applying the isomorphism $L^{r} : H^{- r} \to H^{r}$ to the decomposition of step 5.1 carries the biproduct decomposition of $H^{- r}$ to a biproduct decomposition of $H^{r}$ with summands $L^{r} (L^{j} P^{- r - 2 j}) = L^{r + j} P^{- r - 2 j}$ , giving $H^{r} = ⨁_{j \geq 0} L^{r + j} P^{- r - 2 j}$ . Each restricted power $L^{r + j} ∣_{P^{- r - 2 j}} = L^{r} \circ (L^{j} ∣_{P^{- r - 2 j}})$ is a monomorphism, being the composite of an isomorphism with the monomorphism of step 5.1.

7.1F1step 2.1step 5.1step 6.1algebra

Naturality. Let $φ_{j} : H^{j} \to H^{' j}$ be a morphism of graded objects into another such family $(H^{' j}, L^{' j})$ with $L^{'} φ_{j} = φ_{j + 2} L$ for all $j$ . Then $φ$ commutes with every iterate: $L^{' r} φ_{- r} = φ_{r} L^{r}$ , hence $(L^{' r + 2})^{- 1} φ_{r + 2} = φ_{- r - 2} (L^{r + 2})^{- 1}$ ; consequently $φ_{- r}$ carries $P^{- r} = \ker L^{r + 1}$ into $P^{' - r} = \ker L^{' r + 1}$ , because $L^{' r + 1} φ_{- r} i = φ_{r + 2} L^{r + 1} i = 0$ and the kernel inclusion of $L^{' r + 1}$ has the universal property of [F1]. The comparison $π^{'} φ_{- r} = φ^{P} π$ of the projections holds because both sides become equal after composition with the monomorphism $i^{'}$ , where $φ^{P} : P^{- r} \to P^{' - r}$ is the factorization of $φ_{- r} i$ through $i^{'}$ ; and $φ_{- r} s = s^{'} φ_{r + 2}$ holds by the displayed commutation with the inverses of $L^{r + 2}, L^{' r + 2}$ . So $φ$ preserves the decomposition of step 2.1, and by the same chain of identities at the parameter $r + 2 j + 2$ it maps each summand $L^{j} P^{- r - 2 j}$ into $L^{' j} P^{' - r - 2 j}$ and intertwines the two finite decompositions of step 5.1; the second decompositions, obtained in step 6.1 from the first by the isomorphisms $L^{r}, L^{' r}$ , are intertwined as well.

8.1step 3.1step 4.1step 5.1step 6.1step 7.1discharge-induction∎

The base case of step 3.1 and the induction step of step 4.1 establish the hypothesis of step 3.2 for every $j \geq 0$ , so step 5.1 gives the first displayed decomposition for every $r \geq 0$ , and steps 6.1 and 7.1 give the second decomposition, the monomorphism clause and naturality; the degenerate cases are included, since a zero object has all its summands zero and every argument above is an identity between finitely many morphisms.

Depends on

Used by

Dependency tree · two levels

23 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

M. A. A. de Cataldo and L. Migliorini, «The Hodge theory of algebraic maps», arXiv:math/0306030v2 (complete arXiv 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)