TheoremStatement: 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.

Relative hard Lefschetz and perverse splitting for compact projective algebraic maps

Statement

Assume the inherited Axiom of Choice. Let $f : X \to Y$ be a projective morphism of complex projective varieties, with $X$ smooth of pure complex dimension $n$ , and let $η$ be the first Chern class of an ample line bundle on $X$ . For $K = R f_{*} Q_{X} [n]$ , the maps $η^{i} :^{p} H^{- i} K \to^{p} H^{i} K$ are isomorphisms for all $i \geq 0$ , and $K ≅ ⨁_{i}^{p} H^{i} K [- i]$ is a finite perverse splitting. Every $^{p} H^{i} K$ is a finite direct sum of intersection complexes of simple rational local systems on smooth dense opens of irreducible supports. The complexifications of those local systems are semisimple. This compact-source theorem will be used on explicit quiver-incidence projective compactifications; it does not assert a general nonprojective-source reduction.

Facts & Assumptions

Given: The projective morphism $f : X \to Y$ of complex projective varieties with $X$ smooth of pure dimension $n$ , the ample line bundle on $X$ with first Chern class $η$ , the Axiom of Choice inherited from the suppliers, and the perverse direct image $K = R f_{*} Q_{X} [n]$ .

[F1]

The exact simultaneous-induction supplier Simultaneous projective Lefschetz, Hodge and perverse induction step proves the following stronger induction step. The projective Hodge/perverse package consists of relative hard Lefschetz $η^{i} : P_{- i} ≃ P_{i}$ , a finite normalized splitting $K ≃ ⨁_{b} P_{b} [- b]$ , perverse semisimplicity with semisimple complexifications of the constituent IC local systems, base hard Lefschetz on the canonical graded perverse cohomology groups, purity of those graded groups and their double primitive polarizations. If the package holds for all smooth connected projective-source maps of lexicographically smaller pair $(r (g), \dim g (Z))$ , with $r$ primary, then it holds for the given map.

[F2]

For maps to a point the package is ordinary pure Hodge theory, hard Lefschetz, primitive Hodge–Riemann and finite-dimensional vector-space semisimplicity (Polarized Hodge and hard Lefschetz package for smooth projective varieties); abstract hard Lefschetz gives the finite derived splitting in the bounded $t$ -category (Hard Lefschetz splits a bounded t-structure complex), and on a point the perverse heart is the category of finite-dimensional vector spaces in ordinary degree zero.

[F3]

Proper direct image, finite component sums, the perverse heart and its simple objects as intersection complexes, and closed-support extension are the constructed functors and $t$ -structure of Actual analytic constructible sheaves admit coherent six operations and Ordinary middle perverse t structure, recollement and intersection complexes. In particular the direct sum decomposition of $X$ into finitely many smooth connected components is preserved by the direct image, and $i_{*}$ for the closed immersion of the projective image with reduced structure is perverse exact.

Proof

technique · lexicographic well-founded induction on the pair $(r(f),\dim f(X))$, with defect the primary integer, using the simultaneous induction step of [F1]

1.1F1F2F3givenbaseih

It suffices to treat a connected component of $X$ : the connected components of the smooth variety $X$ are open and closed and there are finitely many of them, and the direct image of their direct sum is the direct sum of the direct images by [F3]. Such a component is irreducible. Replace $Y$ by the projective image of the component with reduced structure; a closed immersion is perverse exact by [F3], so extending by closed support later preserves the splitting and the IC description. For the reduced image the pair $(r, m) = (r (f), \dim f (X))$ consists of nonnegative integers, as in the induction-step supplier [F1]. If $m = 0$ , the map factors through a point, and [F2] proves the entire asserted package directly, including the semisimplicity of the complexified local systems (which are finite-dimensional vector spaces on a point). The empty source gives the zero complex and is covered by the same statement. For a remaining map fix its pair and assume the package of [F1] for every lexicographically smaller pair.

2.1F1F2F3step 1.1discharge-induction∎

The exact induction step [F1] now gives the package for the fixed map. The hypothesis of [F1] is the induction hypothesis recorded in step 1.1, and lexicographic order on pairs of nonnegative integers is well-founded, so with the image-dimension-zero base case the package holds for every smooth connected projective-source map. The clauses asserted in the Statement are the relative hard Lefschetz isomorphisms, the finite splitting and the IC description with semisimplicity of the complexified local systems, all of which are clauses of that package. It remains to replace the very ample class used by [F1] by the given ample class $η$ : by High powers of an ample line bundle embed a proper scheme a sufficiently high power of the given ample bundle is very ample, and if its class is $η_{0} = m η$ then the relative hard Lefschetz isomorphisms for $η_{0}$ scale to those for $η$ because $η^{i} = m^{- i} η_{0}^{i}$ ; the splitting, the IC description and semisimplicity are independent of the chosen ample class. Finally reassemble the finitely many connected components using the direct sums of [F3]. This proves the Statement; no statement about nonprojective sources is made.

Remarks

The proof extracts the asserted compact-source clauses from the simultaneous projective induction step; the induction step itself, including its ordered hyperplane, Hodge, refined-intersection and moving-family constructions, is proved in Simultaneous projective Lefschetz, Hodge and perverse induction step. No general nonprojective-source reduction is asserted, and no finite-ADE, affine-paving or arithmetic-purity hypothesis is used.

Depends on

Used by

Compact smooth projective pushforwards have semisimple perverse cohomology in characteristic zero Theorem

Dependency tree · two levels

107 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)