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

The Hodge index theorem for an ample class

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field, let $X$ be an integral smooth projective surface over $k$ , let $H$ be an ample invertible $O_{X}$ -module (Absolute ampleness by affine section opens) and let $L$ be an invertible $O_{X}$ -module with $L \cdot H = 0.$ Then:

(a) $L \cdot L \leq 0$ ; (b) $L \cdot L = 0$ if and only if $L$ is numerically trivial (Numerical equivalence and the Neron-Severi space of a surface).

Facts & Assumptions

Given: a field $k$ , an integral smooth projective surface $X$ over $k$ , an ample invertible sheaf $H$ , and an invertible sheaf $L$ with $L \cdot H = 0$ .

[F1]

The intersection product is symmetric and $Z$ -bilinear, so $(L \otimes H^{\otimes m}) \cdot (L \otimes H^{\otimes m}) = L \cdot L + m^{2} (H \cdot H)$ because $L \cdot H = 0$ , and $(L \otimes H^{\otimes m}) \cdot L = L \cdot L$ ; the product is trivial against the structure sheaf and depends only on isomorphism classes (Intersection numbers of Cartier divisors on a smooth projective surface, The surface intersection product is symmetric and bilinear, Invertible sheaves, Tensor product of sheaves of modules, Dual of a line bundle is its tensor inverse).

[F2]

Large ample twists of $L$ are very ample: there is $m_{0}$ such that $L \otimes H^{\otimes m}$ is closed H-very ample, hence H-very ample and ample, for every $m \geq m_{0}$ (Large ample twists of a line bundle are very ample, Relative very ampleness implies relative ampleness, Absolute ampleness by affine section opens). In particular $H \cdot H > 0$ (Ample divisors meet nonzero effective divisors positively).

[F3]

Positive square and positive ample intersection force an effective multiple: if $A$ is ample and $M$ is invertible with $M \cdot M > 0$ and $M \cdot A > 0$ , then $H^{0} (X, M^{\otimes n}) \neq 0$ for some $n \geq 1$ (Positive square and positive ample intersection force an effective multiple).

[F4]

Sections and positivity: a nonzero global section of an invertible sheaf $M$ on the integral $X$ is regular, its zero scheme $Z$ is an effective Cartier divisor with $O_{X} (Z) ≅ M$ , and if $Z = \emptyset$ then $M ≅ O_{X}$ (A regular global section of an invertible sheaf glues to an effective Cartier divisor, Zero scheme of a line-bundle section, Ample divisors meet nonzero effective divisors positively). A nonzero effective Cartier divisor $D$ satisfies $H \cdot D > 0$ , and $H \cdot D = \deg_{D} (H ∣_{D})$ (Ample divisors meet nonzero effective divisors positively, Intersection with a curve is the degree of the restriction).

[F5]

Numerical triviality: $L$ is numerically trivial exactly when $L \cdot N = 0$ for every invertible $N$ ; otherwise there is an invertible $Q$ with $Q \cdot L \neq 0$ (Numerical equivalence and the Neron-Severi space of a surface).

[F6]

The Axiom of Choice is inherited from the embedding, positive-square and positivity suppliers of [F2]–[F4]; the integer $m$ and the sign of $n$ below are chosen from finitely described data.

Proof

technique · direct: reduce part (a) to the positive-square lemma via a large ample twist, then handle the equality case of part (b) by a two-parameter perturbation

1.1F1F2F3

Part (a), first reduction. Suppose $L \cdot L > 0$ . By [F2] choose $m \geq m_{0}$ and put $L^{'} : = L \otimes H^{\otimes m}$ , an ample invertible sheaf. By [F1], $L^{'} \cdot L^{'} = L \cdot L + m^{2} (H \cdot H) > 0$ and $L^{'} \cdot L = L \cdot L > 0$ . Applying [F3] with the ample class $L^{'}$ and the sheaf $L$ , we obtain $n \geq 1$ with $H^{0} (X, L^{\otimes n}) \neq 0$ .

2.1F1F4step 1.1

Part (a), contradiction. Let $n \geq 1$ and let $s$ be a nonzero global section of $L^{\otimes n}$ ; by [F4] its zero scheme $Z$ is an effective Cartier divisor with $O_{X} (Z) ≅ L^{\otimes n}$ , and $L^{\otimes n} \cdot H = n (L \cdot H) = 0$ by [F1]. If $Z \neq \emptyset$ , then $H \cdot Z > 0$ by [F4], contradicting $H \cdot Z = L^{\otimes n} \cdot H = 0$ . Hence $Z = \emptyset$ and $L^{\otimes n} ≅ O_{X}$ by [F4]; then $L \cdot L = n^{- 2} (L^{\otimes n} \cdot L^{\otimes n}) = 0$ by [F1], contradicting $L \cdot L > 0$ . Therefore $L \cdot L \leq 0$ , proving (a).

3.1F1F2F5step 2.1

Part (b). If $L$ is numerically trivial then $L \cdot L = 0$ by definition [F5]. Conversely assume $L \cdot L = 0$ and suppose $L$ is not numerically trivial; by [F5] choose an invertible $Q$ with $Q \cdot L \neq 0$ . Put $R : = Q^{\otimes (H \cdot H)} \otimes H^{\otimes - (Q \cdot H)}$ , an invertible sheaf with $R \cdot H = (H \cdot H) (Q \cdot H) - (Q \cdot H) (H \cdot H) = 0, R \cdot L = (H \cdot H) (Q \cdot L) - (Q \cdot H) (H \cdot L) = (H \cdot H) (Q \cdot L) \neq 0,$ using $H \cdot L = 0$ , $H \cdot H > 0$ and bilinearity [F1, F2]. For an integer $n$ put $L^{'} : = L^{\otimes n} \otimes R$ ; then $L^{'} \cdot H = n (L \cdot H) + R \cdot H = 0$ and $L^{'} \cdot L^{'} = n^{2} (L \cdot L) + 2 n (L \cdot R) + R \cdot R = 2 n (L \cdot R) + R \cdot R$ , which is positive for a suitable sign of $n$ because $L \cdot R \neq 0$ . Part (a) applied to $L^{'}$ then gives $L^{'} \cdot L^{'} \leq 0$ , a contradiction. Hence $L$ is numerically trivial, and part (b) follows in both directions.

4.1F6step 2.1step 3.1∎

Conclusion and choice accounting. Step 2.1 proves (a) and step 3.1 proves (b); the Axiom of Choice is inherited from the suppliers recorded in [F6].

Depends on

Used by

The Hodge index theorem for smooth projective surfaces Theorem

Dependency tree · two levels

89 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

Ravi Vakil, The Rising Sea: Foundations of Algebraic Geometry, pre-publication version 2025-10-21 (standard reference, not scraped)
A. Kumar and K. Venkatram, MIT 18.727 Topics in Algebraic Geometry: Algebraic Surfaces, Spring 2008, Lecture 2 (standard reference, not scraped)