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 smooth projective surfaces

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$ , and let $H, L$ be invertible $O_{X}$ -modules (Invertible sheaves) with $H \cdot H > 0, 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).

No ampleness of $H$ is assumed, and the field $k$ is arbitrary; in particular the statement applies to classes with positive self-intersection that are not ample.

Facts & Assumptions

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

[F1]

Ample classes exist on $X$ : the projective hypothesis provides a closed immersion $X ↪ P_{k}^{n}$ in the H-projective convention, and $O_{X} (1) = i^{*} O_{P^{n}} (1)$ is closed H-very ample relative to $Spec k$ , hence H-very ample and ample (Relative very ampleness in the finite projective-space convention, Relative very ampleness implies relative ampleness, Absolute ampleness by affine section opens). Such an ample class $A$ satisfies $A \cdot A > 0$ (Ample divisors meet nonzero effective divisors positively).

[F2]

The ample case of the Hodge index theorem: for an ample invertible sheaf $A$ and an invertible sheaf $L^{'}$ with $L^{'} \cdot A = 0$ one has $L^{'} \cdot L^{'} \leq 0$ , with equality if and only if $L^{'}$ is numerically trivial (The Hodge index theorem for an ample class).

[F3]

Bilinearity: the intersection product is symmetric and $Z$ -bilinear, and intersection numbers depend only on isomorphism classes, so expressions such as $(H^{\otimes a} \otimes L^{\otimes b}) \cdot A = a (H \cdot A) + b (L \cdot A)$ and expansions of self-intersections of tensor products may be computed term by term (The surface intersection product is symmetric and bilinear, Invertible sheaves).

[F4]

Numerical triviality is characterized by vanishing against every invertible sheaf (Numerical equivalence and the Neron-Severi space of a surface).

[F5]

The Axiom of Choice is inherited from the ample-embedding and positivity suppliers of [F1]; all sheaves below are fixed tensor products of the given $H, L$ and of one ample class $A$ .

Proof

technique · direct: fix an ample reference class and reduce to the ample case, once directly and once through a perturbation $M$ depending on $H$ and $L$

1.1F1F2

The case $A \cdot L = 0$ . Let $A$ be an ample class as in [F1]. If $A \cdot L = 0$ , then [F2] applied to $A$ and $L$ gives $L \cdot L \leq 0$ with equality if and only if $L$ is numerically trivial; this is exactly (a) and (b) in this case.

2.1F1F2F3step 1.1

The case $A \cdot L \neq 0$ : a nonzero auxiliary class. Assume now $A \cdot L \neq 0$ . If $A \cdot H = 0$ , then [F2] applied to $A$ and $H$ gives $H \cdot H \leq 0$ , contradicting $H \cdot H > 0$ ; hence $A \cdot H \neq 0$ . Define $M : = H^{\otimes (A \cdot L)} \otimes L^{\otimes - (A \cdot H)},$ an invertible sheaf whose class is $(A \cdot L) [H] - (A \cdot H) [L]$ . By [F3], $M \cdot A = (A \cdot L) (H \cdot A) - (A \cdot H) (L \cdot A) = 0,$ so [F2] applies to $M$ and gives $M \cdot M \leq 0$ . Expanding with [F3] and using $H \cdot L = 0$ , $M \cdot M = (A \cdot L)^{2} (H \cdot H) + (A \cdot H)^{2} (L \cdot L) .$ Since $(A \cdot L)^{2} > 0$ and $H \cdot H > 0$ , if $L \cdot L \geq 0$ then $M \cdot M > 0$ , a contradiction. Hence $L \cdot L < 0$ in this case; in particular $L$ is not numerically trivial.

3.1F4F5step 1.1step 2.1∎

Parts (a) and (b). In the case of step 1.1, (a) and (b) are proved there. In the case of step 2.1 we have $L \cdot L < 0$ , so (a) holds, and (b) holds because a numerically trivial $L$ would have $L \cdot L = 0$ by definition, while conversely $L \cdot L = 0$ is false here. More explicitly, for (b) in the mixed case: if $L$ is numerically trivial then $L \cdot L = 0$ by [F4]; if $L \cdot L = 0$ then step 2.1 forces $A \cdot L = 0$ , so step 1.1 gives that $L$ is numerically trivial. Thus (b) holds in all cases. The Axiom of Choice is inherited from [F5].

Depends on

Used by

Dependency tree · two levels

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