LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Euler polynomial for an arbitrary ample polarization

Statement

Assume AC and DC. Let $X$ be projective over a field $k$ , let $L$ be an ample invertible sheaf, and let $F$ be coherent. There is a unique polynomial $P_{F, L} \in Q [t]$ such that $χ (X, F \otimes L^{\otimes r}) = P_{F, L} (r)$ for every integer $r$ , with degree at most $\dim Supp F$ when $F \neq 0$ . For sufficiently large $r$ this also equals $h^{0} (X, F \otimes L^{\otimes r})$ . Therefore fibrewise eventual equality to a specified polynomial $P$ is equivalent to equality of the fibre Hilbert polynomial with $P$ , and also equivalent here to the all-integer Euler-characteristic characterization. Extension of the field preserves this polynomial. No very-ampleness assumption on $L$ is imposed.

Facts & Assumptions

Given: AC and DC, a projective scheme over a field, an ample invertible $L$ , and coherent $F$ .

[F1]

All sufficiently large powers of $L$ give closed projective-space embeddings (High powers of an ample line bundle embed a proper scheme). For an induced very ample polarization over an infinite field the regular-hyperplane lemma supplies an exact restriction sequence whose cokernel has support dimension one smaller, or is zero when the support has dimension zero (Regular hyperplane step for coherent support induction). Ample bundles restrict to ample bundles on closed subschemes (Finite pullback preserves absolute ampleness).

[F2]

Euler characteristic is additive in short exact sequences (Euler characteristic is additive in short exact sequences). Cohomology and Euler characteristic commute with field extension (Flat field extension commutes with coherent cohomology), and support dimension is preserved (Support dimension under field extension). Serre vanishing for an arbitrary ample bundle is Serre vanishing for coherent sheaves and ample twists. For the embedding-induced polarization the all-integer Euler-polynomial assertion is also Euler characteristic is a Hilbert polynomial, Statement 1, whereas its eventual $h^{0}$ assertion is Statement 2.

Proof

1.1F1F2construct

Extend to an infinite field by [F2]. Induct on $d = \dim Supp F$ , starting with the zero sheaf and its zero polynomial. By [F1] choose consecutive integers $a, a + 1$ for which $L^{a}$ and $L^{a + 1}$ are very ample. In each of these two embeddings choose a hyperplane avoiding the associated points of $F$ . For $b = a, a + 1$ the induced section of $L^{b}$ gives $0 \to F \otimes L^{- b} \to F \to G_{b} \to 0$ , where $G_{b}$ is supported on the hyperplane and has support dimension $d - 1$ , or is zero if $d = 0$ . Its restricted $L$ is ample. By induction $χ (G_{b} \otimes L^{r})$ is a rational polynomial $g_{b} (r)$ of degree at most $d - 1$ ; for $d = 0$ it is zero. The exact sequence stays exact after every integer twist.

2.1F2step 1.1algebra

Put $f (r) = χ (F \otimes L^{r})$ . Additivity gives $f (r) - f (r - b) = g_{b} (r)$ for $b = a, a + 1$ and every integer $r$ . Subtract the $b = a$ identity at $r - 1$ from the $b = a + 1$ identity at $r$ to get $f (r) - f (r - 1) = g_{a + 1} (r) - g_{a} (r - 1)$ , a polynomial of degree at most $d - 1$ . Every rational polynomial of that degree has a polynomial discrete antiderivative of degree at most $d$ : in the binomial basis use $(\binom{r}{j}) - (\binom{r - 1}{j}) = (\binom{r - 1}{j - 1})$ . Choose its additive constant to agree with $f (0)$ . The difference from $f$ is then invariant under $r \mapsto r - 1$ and zero at zero, hence zero for all integers, positive and negative. This proves the polynomial assertion and its degree bound; uniqueness follows because a polynomial vanishing on all sufficiently large integers is zero.

3.1F2step 2.1algebra∎

By [F2], Euler characteristics over the original field equal those over the infinite extension, so the same polynomial works there and under any further field extension. Serre vanishing makes its value equal $h^{0}$ in a sufficiently large tail. Equality in any such tail determines the polynomial uniquely by step 2.1, which gives precisely the claimed equivalences. The zero sheaf and empty source have zero polynomial and satisfy the same statements.

Depends on

Used by

Dependency tree · two levels

170 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

Nitsure, Section 1, Stratification by Hilbert Polynomials, page 4 (Euler polynomial; Snapper formulation) (standard reference, not scraped)