TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 surface intersection product is symmetric and bilinear

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field, let $X$ be an integral regular projective surface over $k$ (Intersection numbers of Cartier divisors on a smooth projective surface) and let $L, M, N$ be invertible $O_{X}$ -modules (Invertible sheaves). Then $(L \otimes M) \cdot N = L \cdot N + M \cdot N, L \cdot (M \otimes N) = L \cdot M + L \cdot N;$ consequently the intersection product is a symmetric $Z$ -bilinear pairing $Pic (X) \times Pic (X) \to Z$ and $L \cdot O_{X} = 0$ . Equivalently, for Cartier divisors on $X$ : $(C + C^{'}) \cdot D = C \cdot D + C^{'} \cdot D, C \cdot (D + D^{'}) = C \cdot D + C \cdot D^{'}, C \cdot D = D \cdot C .$

Facts & Assumptions

Given: a field $k$ , an integral regular projective surface $X$ over $k$ , invertible $O_{X}$ -modules $L, M, N$ , and Cartier divisors $C, D$ on $X$ .

[F1]

The surface: $X$ is proper over $k$ (Projective morphisms are proper), integral, and of finite type over $k$ , hence Noetherian and locally Noetherian (Every algebra of finite type over a Noetherian ring is a Noetherian ring, Locally Noetherian and Noetherian schemes, Integral schemes); $χ (X, -)$ is defined on coherent modules and the intersection product on invertible modules and Cartier divisors is defined, symmetric in its two arguments, vanishes against $O_{X}$ , and depends only on the isomorphism classes of the line bundles, equivalently only on the linear equivalence classes of the divisors (Intersection numbers of Cartier divisors on a smooth projective surface).

[F2]

Ample and very ample twists: fix a projective embedding of $X$ in the H-projective convention and let $O_{X} (1)$ be the pullback of the twisting sheaf of projective space; then $O_{X} (1)$ is H-very ample relative to $Spec k$ , hence ample (Projective morphisms before Proj, Relative very ampleness in the finite projective-space convention, Relative very ampleness implies relative ampleness, Absolute ampleness by affine section opens).

[F3]

Effective Cartier divisors: an effective Cartier divisor $H$ has invertible ideal sheaf $O_{X} (- H)$ , closed immersion $i : H ↪ X$ , and short exact sequence $0 \to O_{X} (- H) \to O_{X} \to i_{*} O_{H} \to 0$ ; twisting by an invertible $N$ gives $0 \to N (- H) \to N \to i_{*} (N ∣_{H}) \to 0$ (Effective cartier divisor, Invertible sheaf of cartier divisor, Effective Cartier divisors give a short exact sequence, Twisting the exact sequence of an effective Cartier divisor). Moreover $H$ is a proper $k$ -scheme of dimension at most one (A minimal prime over a principal nonzerodivisor has height one, Chain dimension and the empty-space convention, Projective morphisms are proper), so the degree and the quadratic identity of Degree is additive on invertible sheaves over a proper curve apply on $H$ .

[F4]

Additivity of $χ$ and the projection formula: for a short exact sequence of coherent modules on $X$ the Euler characteristic is additive (Euler characteristic is additive in short exact sequences), and $χ (X, i_{*} F) = χ (H, F)$ for coherent $F$ on $H$ (Projection formula for a closed immersion and an invertible sheaf).

[F5]

Global generation: since $X$ is projective over the Noetherian field $k$ with $O_{X} (1)$ ample, for every coherent $F$ there is $m_{0}$ with $F \otimes O_{X} (1)^{\otimes m}$ globally generated for all $m \geq m_{0}$ (Eventual generation of coherent projective twists); on the integral nonempty $X$ a nonzero global section of an invertible sheaf is regular, and its zero scheme is an effective Cartier divisor $Z (s)$ with $O_{X} (Z (s)) ≅ L$ (A regular global section of an invertible sheaf glues to an effective Cartier divisor, Zero scheme of a line-bundle section).

[F6]

Divisor dictionary on the integral surface: $D \mapsto [O_{X} (D)]$ induces an isomorphism $CaDiv (X) / {Prin}_{C} (X) \tilde{\to} Pic (X)$ , so $D$ is linearly equivalent to $D^{'}$ exactly when $O_{X} (D) ≅ O_{X} (D^{'})$ , and $O_{X} (D + D^{'}) ≅ O_{X} (D) \otimes O_{X} (D^{'})$ , $O_{X} (- D) ≅ O_{X} (D)^{\lor}$ (On an integral scheme, Cartier divisors modulo principal divisors compute the Picard group, Addition of Cartier divisors is tensor product of their sheaves, Dual of a line bundle is its tensor inverse).

[F7]

The Axiom of Choice is inherited through the properness and ampleness suppliers [F1]–[F2], the curve identity of [F3] (via devissage), the Euler-characteristic and cohomology suppliers of [F4], and eventual global generation in [F5]. The divisor dictionary [F6] uses no choice principle; the tensor computations below make no selection.

Proof

technique · direct; prove the shift identity for an effective divisor by substituting two twisting sequences into the defining four-term expression, then reduce arbitrary divisors to differences of effective ones via global generation

1.1F1F3F4F6

Set-up and the shift identity. For invertible modules $L_{1}, L_{2}$ write $Φ (L_{1}, L_{2})$ for the defining expression $χ (X, O_{X}) - χ (X, L_{1}^{\lor}) - χ (X, L_{2}^{\lor}) + χ (X, L_{1}^{\lor} \otimes L_{2}^{\lor})$ , so that $L_{1} \cdot L_{2} = Φ (L_{1}, L_{2})$ ; for an effective Cartier divisor $H$ write $L_{2} (H) = L_{2} \otimes O_{X} (H)$ and set $e (N) : = χ (X, N) - χ (X, N (- H))$ for invertible $N$ , so that $e (N) = χ (H, N ∣_{H})$ by the twisting sequence, additivity of $χ$ and the projection formula. Expanding the four terms and using $L_{2} (H)^{\lor} = L_{2}^{\lor} (- H)$ gives $Φ (L_{1}, L_{2} (H)) - Φ (L_{1}, L_{2}) - Φ (L_{1}, O_{X} (H)) = e (L_{1}^{\lor}) + e (L_{2}^{\lor}) - e (O_{X}) - e (L_{1}^{\lor} \otimes L_{2}^{\lor}),$ and substituting $e (N) = χ (H, N ∣_{H})$ the right-hand side becomes the negative of $χ (H, O_{H}) - χ (H, L_{1}^{\lor} ∣_{H}) - χ (H, L_{2}^{\lor} ∣_{H}) + χ (H, L_{1}^{\lor} ∣_{H} \otimes L_{2}^{\lor} ∣_{H})$ , which vanishes by part 3 of Degree is additive on invertible sheaves over a proper curve applied to the proper curve $H$ and the invertible sheaves $L_{1}^{\lor} ∣_{H}$ , $L_{2}^{\lor} ∣_{H}$ . Hence $Φ (L_{1}, L_{2} (H)) = Φ (L_{1}, L_{2}) + Φ (L_{1}, O_{X} (H))$ for every effective Cartier divisor $H$ . The defining expression is symmetric, $Φ (L, O_{X}) = 0$ , and $Φ$ depends only on isomorphism classes; writing $Φ (C, D) : = Φ (O_{X} (C), O_{X} (D))$ for Cartier divisors, the divisor dictionary shows that $Φ (C, D)$ depends only on the linear equivalence classes of $C$ and $D$ .

1.2F2F5F6

Differences of effective divisors. Every Cartier divisor on $X$ is linearly equivalent to a difference $E - F$ of effective Cartier divisors: since $X$ is projective over the Noetherian field $k$ and $O_{X} (1)$ is ample, there is an integer $m$ for which both $O_{X} (D) \otimes O_{X} (1)^{\otimes m}$ and $O_{X} (1)^{\otimes m}$ are globally generated; choosing nonzero global sections $s$ and $t$ and using that $X$ is integral, the zero schemes $E = Z (s)$ and $F = Z (t)$ are effective Cartier divisors with $O_{X} (E) ≅ O_{X} (D) \otimes O_{X} (1)^{\otimes m}$ and $O_{X} (F) ≅ O_{X} (1)^{\otimes m}$ , so $O_{X} (E - F) ≅ O_{X} (D)$ and $D$ is linearly equivalent to $E - F$ .

2.1F6step 1.1

Effective additivity. Let $H$ be an effective Cartier divisor and let $C, D$ be Cartier divisors. By the shift identity of step 1.1 and the dictionary of [F6], $Φ (C, D + H) = Φ (C, D) + Φ (C, H)$ . In particular, for effective $C, D_{1}, D_{2}$ the identity $Φ (C, D_{1} + D_{2}) = Φ (C, D_{1}) + Φ (C, D_{2})$ holds by taking $D = D_{1}$ and $H = D_{2}$ .

3.1step 1.2step 2.1

Additivity in the second variable. Let $D_{1}, D_{2}$ be arbitrary Cartier divisors and choose, by step 1.2, effective $E_{1}, E_{2}, F_{1}, F_{2}$ with $D_{i}$ linearly equivalent to $E_{i} - F_{i}$ . Then $D_{1} + F_{1}$ is linearly equivalent to $E_{1}$ , and $D_{2} + F_{2}$ to $E_{2}$ ; since the values of $Φ$ depend only on linear equivalence classes, applying step 2.1 twice with the effective divisors $F_{1}, F_{2}$ gives $Φ (C, D_{1} + D_{2}) + Φ (C, F_{1}) + Φ (C, F_{2}) = Φ (C, D_{1} + D_{2} + F_{1} + F_{2}) = Φ (C, E_{1} + E_{2}) = Φ (C, E_{1}) + Φ (C, E_{2}),$ while applying step 2.1 to each pair $(D_{i}, F_{i})$ gives $Φ (C, E_{i}) = Φ (C, D_{i}) + Φ (C, F_{i})$ . Substituting and cancelling $Φ (C, F_{1}) + Φ (C, F_{2})$ yields $Φ (C, D_{1} + D_{2}) = Φ (C, D_{1}) + Φ (C, D_{2})$ for all Cartier divisors $C, D_{1}, D_{2}$ .

4.1F1F6step 3.1

Additivity in the first variable and vanishing at zero. The defining expression is symmetric in its two arguments, so $Φ (C_{1} + C_{2}, D) = Φ (D, C_{1} + C_{2}) = Φ (D, C_{1}) + Φ (D, C_{2}) = Φ (C_{1}, D) + Φ (C_{2}, D)$ by step 3.1 applied with first argument $D$ ; hence $Φ$ is additive in each variable, and $Φ (C, 0) = Φ (0, D) = 0$ because $O_{X} (0) = O_{X}$ and $Φ (L, O_{X}) = 0$ .

5.1F7step 2.1step 3.1step 4.1∎

Translation to line bundles and conclusion. Since $X$ is integral, every invertible sheaf on $X$ is isomorphic to $O_{X} (C)$ for a Cartier divisor $C$ , well defined modulo linear equivalence; under this dictionary tensor products and duals of line bundles correspond to sums and negatives of divisors, and $Φ$ depends only on the classes. Hence the divisor identities of steps 2.1, 3.1 and 4.1 translate into $(L \otimes M) \cdot N = L \cdot N + M \cdot N, L \cdot (M \otimes N) = L \cdot M + L \cdot N, L \cdot M = M \cdot L, L \cdot O_{X} = 0$ for all invertible $L, M, N$ : the intersection product is a symmetric $Z$ -bilinear pairing $Pic (X) \times Pic (X) \to Z$ . The Axiom of Choice enters only through the suppliers of [F7], in particular the eventual global generation of [F5], the Euler-characteristic additivity and projection formula of [F4] and the curve identity of [F3] used in step 1.1; the two sections chosen in step 1.2 are single sections of specific sheaves, not a family, and no further selection is made.

Depends on

Used by

Dependency tree · two levels

126 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)
The Stacks Project, Varieties, Section 33.45 (Numerical intersections) (standard reference, not scraped)