TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Negative-degree line bundles have no nonzero sections

Statement

Assume the Axiom of Choice. It supplies Dependent Choice by AC implies DC implies countable choice for the curve Cartier-to-Weil interface. Let $C$ be a smooth proper geometrically integral curve over a field $k$ and let $L$ be an invertible sheaf on $C$ whose degree $\deg (L)$ is represented by $\deg_{k} (D)$ for any divisor $D$ with $L ≅ O_{C} (D)$ . If $\deg (L) < 0$ then $H^{0} (C, L) = 0$ . Consequently a line bundle with a nonzero global section has nonnegative degree.

Current supplier interfaces. Under AC, The degree of a divisor descends to the Picard group of a normal proper curve defines the degree of an invertible sheaf through its Picard class. The current Rational sections of line bundles are Cartier divisors body associates to a nonzero rational section $s$ the Cartier divisor $D_{s} = {div}_{C} (s)$ and an isomorphism $O_{C} (D_{s}) ≅ L$ carrying its canonical section to $s$ ; Effective cartier divisor characterizes when this section divisor is effective, and Invertible sheaf of cartier divisor gives the associated invertible sheaf. The actual passage to the finite closed-point divisor and its coefficientwise effectivity uses Cartier and Weil divisors agree on a smooth curve, whose AC premise supplies its Dependent Choice premise. These current interfaces support the proof below.

Facts & Assumptions

Given: A smooth proper geometrically integral curve $C$ over a field $k$ , an invertible sheaf $L$ on $C$ with degree $\deg (L)$ defined as $\deg_{k} (D)$ for any divisor $D$ with $L ≅ O_{C} (D)$ , and the Axiom of Choice.

[F1]

A divisor on $C$ is a finite formal $Z$ -linear combination $D = \sum_{x} n_{x} [x]$ of closed points; its degree is $\deg_{k} (D) = \sum_{x} n_{x} [κ (x) : k]$ , the residue field of a closed point being a finite extension of $k$ ; and $\deg_{k}$ is additive. (Divisors on a smooth proper curve, Curves over a field)

[F2]

For an effective divisor $D$ on the proper geometrically integral curve $C$ the degree $\deg_{k} (D) = \sum_{x} n_{x} [κ (x) : k]$ is nonnegative, and it vanishes only for $D = 0$ ; equivalently, sufficiently, the degree of an effective divisor is at least $0$ . (Effective divisors have nonnegative degree)

[F3]

Under the Axiom of Choice, the current supplier The degree of a divisor descends to the Picard group of a normal proper curve defines $\deg (L)$ through the Picard class of an invertible sheaf. For a nonzero rational section $s$ of $L$ , Rational sections of line bundles are Cartier divisors supplies the Cartier divisor $D_{s} = {div}_{C} (s)$ and an isomorphism $O_{C} (D_{s}) ≅ L$ ; a global section has effective $D_{s}$ by Effective cartier divisor. The associated sheaf $O_{C} (D_{s})$ is given by Invertible sheaf of cartier divisor. (The degree of a divisor descends to the Picard group of a normal proper curve, Invertible sheaf of cartier divisor, Effective cartier divisor, Rational sections of line bundles are Cartier divisors)

[F4]

In ZF, AC implies DC by AC implies DC implies countable choice. Under AC and this DC premise, the current Cartier and Weil divisors agree on a smooth curve body identifies Cartier divisors with finite closed-point Weil divisors and preserves principal divisors. In particular an effective Cartier divisor is an effective divisor in the sense of [F1] and conversely. (Cartier and Weil divisors agree on a smooth curve, AC implies DC implies countable choice, Divisors on a smooth proper curve)

Proof

technique · direct; a nonzero global section would exhibit the bundle as the sheaf of an effective divisor, whose degree is nonnegative, contradicting the negative degree hypothesis

1.1F3F4

A nonzero section gives an effective divisor. Assume that $\deg (L) < 0$ and that $H^{0} (C, L) \neq 0$ , and choose a nonzero global section $s \in H^{0} (C, L)$ ; it is a nonzero rational section. By [F3], the section $s$ determines the effective Cartier divisor $D_{s} = {div}_{C} (s)$ with $O_{C} (D_{s}) ≅ L$ , and by [F4] this Cartier divisor is the effective Weil divisor $D_{s} = \sum_{x} n_{x} [x]$ with $n_{x} \geq 0$ on $C$ .

2.1F1F2step 1.1

Degree contradiction. By the definition of the degree in the hypothesis of the Statement and the isomorphism $O_{C} (D_{s}) ≅ L$ of step 1.1, $\deg (L) = \deg_{k} (D_{s})$ ; by [F2] applied to the effective divisor $D_{s}$ of step 1.1 this degree is nonnegative, in contradiction with $\deg (L) < 0$ . Hence no nonzero global section exists and $H^{0} (C, L) = 0$ .

3.1F2F3F4step 1.1step 2.1∎

The consequence. Conversely, if $L$ has a nonzero global section, the argument of steps 1.1 and 2.1 — which derives a contradiction from $\deg (L) < 0$ — shows that $\deg (L) \geq 0$ ; this is the second assertion. AC is used through the degree homomorphism [F3] and through the Cartier-to-Weil route [F4], with AC supplying DC as stated there. The section-divisor interface used at step 1.1 is the current supplier in [F3].

Depends on

Used by

Dependency tree · two levels

75 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

The Stacks Project, Algebraic Curves (tag 0BRV) (standard reference, not scraped)
William Fulton, Algebraic Curves (Internet Archive copy), Chs. 6-8 (standard reference, not scraped)