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.

A degree-n line bundle on a genus-one curve has an n-dimensional space of sections for n > 0

Example

Assume the Axiom of Choice; it supplies Dependent Choice through AC implies DC implies countable choice. Let $C$ be a smooth proper geometrically integral curve of genus one over a field $k$ , and let $L$ be an invertible sheaf of degree $n \geq 1$ , with associated divisor $D$ under the divisor--invertible-sheaf dictionary.

Since $n \geq 1 > 0 = 2 g - 2$ , the line bundle $L$ is nonspecial: $H^{1} (C, L) = 0, ℓ (D) = h^{0} (C, L) = \deg_{k} D + 1 - g = n .$ Equivalently, since $ω_{C} ≅ O_{C}$ for a genus-one curve, Serre duality reads $h^{1} (C, L) = h^{0} (C, ω_{C} \otimes L^{- 1}) = h^{0} (C, L^{- 1}) = 0,$ because $\deg L^{- 1} = - n < 0$ forces the vanishing of the sections of the negative-degree dual.

For $n = 1$ the space of sections is one-dimensional. Under an isomorphism $L ≅ O_{C} (D)$ , a nonzero section corresponds to a nonzero rational function $f \in L (D)$ , and its zero divisor is $E = D + div (f)$ . This is effective by the definition of $L (D)$ and has degree $1$ , since principal divisors have degree zero. Thus $E = [p]$ for a closed point $p$ with $[κ (p) : k] = 1$ , so $p$ is $k$ -rational. The same argument applies to every degree-one divisor $D$ ; its complete linear system has the single effective member $[p]$ . The dimension formula $\dim ∣ D ∣ = \deg_{k} D - g + i (D) = n - 1 + 0$ recovers this for $n = 1$ and shows that the complete linear system grows by exactly one dimension for each added degree.

Facts & Assumptions

Given: the Axiom of Choice and its consequence Dependent Choice; a smooth proper geometrically integral curve $C$ of genus one over a field $k$ , an invertible sheaf $L$ of degree $n \geq 1$ , and the associated divisor $D$ .

[F1]

For an invertible sheaf of degree $> 2 g - 2$ on a smooth proper geometrically integral curve of genus $g$ , $H^{1} (C, L) = 0$ and $h^{0} (C, L) = \deg L + 1 - g$ ; equivalently $ℓ (D) = \deg_{k} D + 1 - g$ for divisors of degree $> 2 g - 2$ . (H^1 of a line bundle vanishes above degree 2g - 2, Riemann-Roch in exact form for divisors of degree above 2g - 2)

[F2]

The full Riemann-Roch theorem reads $ℓ (D) - ℓ (K_{C} - D) = \deg_{k} D + 1 - g$ ; the line bundle associated with $D$ has $h^{0} (C, O (D)) = ℓ (D)$ , and the degree of $L^{- 1}$ is $- \deg L$ . (The full Riemann-Roch theorem for divisors on a smooth proper curve, The Riemann-Roch dimension l(D), Invertible sheaf of cartier divisor, Cartier and Weil divisors agree on a smooth curve)

[F3]

On a genus-one curve $ω_{C} ≅ O_{C}$ , and Serre duality for invertible sheaves gives $h^{1} (C, L) = h^{0} (C, ω_{C} \otimes L^{- 1})$ ; a line bundle of degree $< 0$ has no nonzero global section. (The canonical bundle of a genus-one curve is trivial, Serre duality for line bundles on a smooth proper curve, and the residue realization, Negative-degree line bundles have no nonzero sections)

[F4]

The dimension of the complete linear system of a divisor is $\dim ∣ D ∣ = ℓ (D) - 1 = \deg_{k} D - g + i (D)$ , where $i (D) = ℓ (K_{C} - D)$ is the index of speciality. Under an isomorphism $L ≅ O_{C} (D)$ , a nonzero global section corresponds to a nonzero $f \in L (D)$ ; its zero divisor is the effective divisor $D + div (f)$ , of degree $\deg_{k} D$ because principal divisors have degree zero. (The dimension of a complete linear system, Complete linear system, The space L(D), Degree divisor proper curve, Rational sections of line bundles are Cartier divisors, Principal divisors on a normal proper curve have degree zero)

[F5]

The Axiom of Choice: every family of nonempty sets has a choice function. (The Axiom of Choice)

[F6]

In ZF, the Axiom of Choice implies Dependent Choice; this supplies the Dependent Choice premise of the Cartier-to-Weil dictionary used in [F2] and [F4]. (AC implies DC implies countable choice, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

Verification

Proof technique: apply the nonspecial Riemann-Roch formula and check the degree-one case separately, with Serre duality as an independent computation of $H^{1}$ .

1.1F1

Since $g = 1$ we have $2 g - 2 = 0$ , and $n \geq 1$ gives $\deg L = n > 0$ ; by [F1] applied to $L$ , $H^{1} (C, L) = 0$ and $ℓ (D) = h^{0} (C, L) = n + 1 - 1 = n$ .

2.1F3step 1.1

Independently, [F3] gives $h^{1} (C, L) = h^{0} (C, L^{- 1})$ up to the identification $ω_{C} ≅ O_{C}$ , and $\deg L^{- 1} = - n < 0$ , so [F3] again gives $h^{0} (C, L^{- 1}) = 0$ ; this agrees with Step 1.1 and confirms that $L$ is nonspecial.

2.2F4F5step 1.1

For $n = 1$ , Step 1.1 gives $ℓ (D) = 1$ . Choose a nonzero section $s \in H^{0} (C, L)$ and an isomorphism $L ≅ O_{C} (D)$ ; the section corresponds to a nonzero $f \in L (D)$ , and [F4] gives the effective zero divisor $E = D + div (f)$ . By [F4] and the degree-zero theorem for principal divisors, $\deg_{k} (E) = \deg_{k} (D) = 1$ . Hence $E = [p]$ for a closed point with residue degree one, so $p$ is $k$ -rational and $D \sim [p]$ . Since $ℓ (D) = 1$ , the complete linear system has exactly the single effective member $[p]$ . This argument applies to every degree-one divisor.

3.1F4step 1.1step 2.2algebra

The dimension formula of [F4] gives $\dim ∣ D ∣ = \deg_{k} D - g + i (D) = n - 1 + 0 = n - 1$ , with $i (D) = h^{1} (C, L) = 0$ by Step 1.1; for $n = 1$ this says $\dim ∣ D ∣ = 0$ in agreement with Step 2.2, and each increase of the degree by one increases $\dim ∣ D ∣$ by exactly one.

4.1F5F6F2F3step 3.1∎

The Axiom of Choice is used through the duality, degree, and divisor suppliers; [F6] supplies the Dependent Choice premise required by the Cartier-to-Weil divisor dictionary.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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