ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Serre duality on the projective line, twist by twist

Example

Assume the Axiom of Choice as inherited from the cited cohomology and duality suppliers (The Axiom of Choice). Let $k$ be any field, let $P_{k}^{1}$ have homogeneous coordinates $x_{0}, x_{1}$ and affine coordinate $t = x_{1} / x_{0}$ on $U_{0}$ , fix $d \geq 0$ , and set $L = O (- d - 2)$ .

The groups $H^{1} (P_{k}^{1}, L)$ and $H^{0} (P_{k}^{1}, O (d))$ have dimension $d + 1$ ; all other cohomology groups of these two twists vanish. For $1 \leq j \leq d + 1$ , let $c_{j} = [t^{- j} \otimes x_{0}^{- d - 2}] \in H^{1} (P_{k}^{1}, L),$ where the displayed expression is the local principal part in the frame $x_{0}^{- d - 2}$ on $U_{0}$ . For $0 \leq m \leq d$ , the corresponding global section of $ω_{P^{1}} \otimes L^{- 1}$ is $σ_{m} = t^{m} d t \otimes x_{0}^{d + 2} on U_{0} .$ On $U_{1}$ , with $s = 1 / t$ , its expression is $σ_{m} = - s^{d - m} d s \otimes x_{1}^{d + 2},$ so it is regular for exactly the stated range $m \leq d$ ; under $d t \mapsto x_{0}^{- 2}$ and $d s \mapsto - x_{1}^{- 2}$ it corresponds to $x_{0}^{d - m} x_{1}^{m}$ .

At the rational origin, the positive local residue of the product is $[t^{- 1}] (t^{m - j}) = δ_{j, m + 1} .$ This is the identity matrix when the classes are ordered by $j = 1, \dots, d + 1$ and sections by $m = 0, \dots, d$ . Reversing the section order to $m = d, \dots, 0$ displays the same positive matrix as anti-diagonal. The fixed normalized Serre pairing is the negative of this matrix. This remains perfect over every field; for $d = 0$ its value is $- 1$ , which equals $1$ in characteristic two.

Facts & Assumptions

Given: the Axiom of Choice, a field $k$ , $P_{k}^{1}$ with coordinate $t = x_{1} / x_{0}$ , an integer $d \geq 0$ , and $L = O (- d - 2)$ .

[F1]

The Axiom of Choice is inherited from the projective cohomology, principal-parts, field-extension, and duality suppliers, and is used to take an algebraic closure in step 2.1. No other selection is made. (The Axiom of Choice)

[F2]

On $P_{k}^{1}$ , $H^{0} (O (d))$ has basis $x_{0}^{d - m} x_{1}^{m}$ for $0 \leq m \leq d$ , and $H^{1} (O (- d - 2))$ has Laurent basis $x_{0}^{e_{0}} x_{1}^{e_{1}}$ with $e_{0}, e_{1} < 0$ and $e_{0} + e_{1} = - d - 2$ ; both groups have dimension $d + 1$ . (Cohomology of O(d) on projective space)

[F3]

The standard frames satisfy $x_{0}^{d + 2} = s^{d + 2} x_{1}^{d + 2}$ on the overlap, $s = 1 / t$ , and $d t = - s^{- 2} d s$ . Also $d t$ maps to $x_{0}^{- 2}$ and $d s$ maps to $- x_{1}^{- 2}$ under $ω_{P^{1}} ≅ O (- 2)$ . Thus $t^{m} d t \otimes x_{0}^{d + 2} = - s^{d - m} d s \otimes x_{1}^{d + 2}$ and corresponds to $x_{0}^{d - m} x_{1}^{m}$ . The sheaves $O (r)$ are invertible and $O (r)^{- 1} ≅ O (- r)$ . (Twisting sheaf on Proj, Relative projective space from standard charts, Invertible sheaves, Canonical bundle and canonical divisors)

[F4]

Principal parts give the cokernel description of $H^{1}$ ; in particular, each finite-support tail $t^{- j}$ in the frame $x_{0}^{- d - 2}$ represents the class $c_{j}$ . (H^1 of a line bundle on a curve as principal parts modulo meromorphic and regular sections)

[F5]

At the rational origin with parameter $t$ , the local residue of $t^{m - j} d t$ is its $t^{- 1}$ coefficient. Over a perfect field, the positive residue pairing is the sum of these local residues. (Residue of a rational differential at a separable closed point, The residue pairing of a line bundle with the dual canonical twist)

[F6]

For a smooth proper geometrically integral curve, the fixed normalized Gysin trace and its Serre pairing are defined over every field. Over a perfect field the trace pairing is the negative of the positive residue pairing. (Serre duality for line bundles on a smooth proper curve, and the residue realization, Normalization of the trace for Serre duality on a curve)

[F7]

For a proper scheme, coherent cohomology commutes with arbitrary field extension. The fixed Gysin trace and its cup/evaluation pairing also commute with extension of the base field. (Flat field extension commutes with coherent cohomology, Embedding compatibility of smooth-projective Gysin traces)

[F8]

On $P_{k}^{1}$ , $ω_{P^{1}} ≅ O (- 2)$ : its canonical degree is $- 2$ , and the Picard group is classified by degree. (The canonical divisor has degree 2g - 2, The Picard group of the projective line, Divisors on the projective line are classified by degree, Degree divisor proper curve, Canonical bundle and canonical divisors)

Verification

Proof technique: identify the Laurent-tail and section bases, compute the positive residue matrix at the rational origin, then descend the fixed-trace sign from an algebraic closure.

1.1F2F4

By [F2], $H^{1} (P^{1}, L)$ and $H^{0} (P^{1}, O (d))$ have dimension $d + 1$ . For $1 \leq j \leq d + 1$ , the single tail $t^{- j}$ in the frame $x_{0}^{- d - 2}$ is a finite-support principal part at the rational origin, and by [F4] it represents the class $c_{j}$ .

1.2F2F3

By [F3], $σ_{m} = t^{m} d t \otimes x_{0}^{d + 2}$ has $U_{1}$ expression $- s^{d - m} d s \otimes x_{1}^{d + 2}$ , hence is regular for $0 \leq m \leq d$ . Under $d t \mapsto x_{0}^{- 2}$ and $d s \mapsto - x_{1}^{- 2}$ it corresponds to $x_{0}^{d - m} x_{1}^{m}$ , so these sections form the basis of the dual canonical twist.

2.1F1F5F6step 1.1step 1.2

At the rational point $0$ , the product of the local principal part and section is $t^{m - j} d t$ , whose positive local residue is $δ_{j, m + 1}$ by [F5]. Choose an algebraic closure $K = \overset{ˉ}{k}$ ; it is perfect, so [F6] gives $t_{P_{K}^{1}} (c_{j, K} \cup σ_{m, K}) = - δ_{j, m + 1}$ . The class and section defined over $k$ pull back to the same expressions over $K$ .

3.1F2F7step 1.1step 1.2step 2.1algebra

By [F7], cohomology classes, cup products and the fixed Gysin trace commute with $k \to K$ . Thus $t_{P_{k}^{1}} (c_{j} \cup σ_{m})$ maps to $- δ_{j, m + 1}$ in $K$ ; injectivity of $k ↪ K$ gives the same scalar over $k$ . In ascending orders the normalized matrix is $- I_{d + 1}$ ; reversing the section order to $m = d, \dots, 0$ makes it anti-diagonal with entries $- 1$ . Because the $σ_{m}$ form a basis by step 1.2, invertibility of this matrix proves that the $d + 1$ classes $c_{j}$ are independent; their number equals $\dim_{k} H^{1} = d + 1$ by step 1.1, so they form a basis.

4.1F6F8step 1.1step 1.2step 3.1∎

By [F8], $ω_{P^{1}} \otimes L^{- 1} ≅ O (d)$ , so the bases above are those of the two Serre-dual spaces. The explicit normalized matrix is perfect, in agreement with the arbitrary-field duality pairing [F6]. For $d = 0$ it is $[- 1]$ , and characteristic two identifies $- 1$ with $1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

205 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 (version of October 21, 2025) (standard reference, not scraped)
The Stacks Project, Algebraic Curves (tag 0BRV) (standard reference, not scraped)