LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 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.

Effective divisors have nonnegative degree

Statement

Let $k$ be a field and let $C$ be a proper geometrically integral curve over $k$ . Let $D = \sum_{x} n_{x} [x]$ be an effective divisor on $C$ . Then $\deg_{k} (D) = \sum_{x} n_{x} [κ (x) : k]$ is a nonnegative integer, and $\deg_{k} (D) = 0$ if and only if $D = 0$ . The residue field of every closed point is a finite extension of $k$ , so each degree $[κ (x) : k]$ is at least one.

Facts & Assumptions

Given: A field $k$ , a proper geometrically integral curve $C$ over $k$ , and an effective divisor $D = \sum_{x} n_{x} [x]$ on $C$ .

[F1]

A curve over $k$ is geometrically integral, separated and of finite type of chain dimension one; a proper curve over $k$ is in particular an integral $k$ -scheme whose structure morphism is proper and whose underlying space has chain dimension one, hence of dimension one. (Curves over a field, Degree divisor proper curve)

[F2]

A divisor on the proper curve $C$ is a finite formal sum $D = \sum_{x} n_{x} [x]$ over the closed points $x$ of $C$ with integer coefficients all but finitely many of which vanish; for each closed point the residue field $κ (x)$ is a finite extension of $k$ , and the degree is $\deg_{k} D = \sum_{x} n_{x} [κ (x) : k]$ , a group homomorphism $Div (C) \to Z$ . (Degree divisor proper curve)

[F3]

The support, positive part and negative part of $D$ are defined by $Supp (D) = {x : n_{x} \neq 0}$ , $D^{+} = \sum_{x} \max (n_{x}, 0) [x]$ and $D^{-} = \sum_{x} \max (- n_{x}, 0) [x]$ , so that $D = D^{+} - D^{-}$ ; all coefficients of $D^{+}$ and $D^{-}$ are nonnegative, their supports are disjoint, and $D$ is effective if and only if $D^{-} = 0$ . (Divisor support positive negative parts)

[F4]

A divisor on a smooth proper geometrically integral curve over $k$ is a finite $Z$ -linear combination of closed points, its degree is $\deg_{k} (D) = \sum_{x} n_{x} [κ (x) : k]$ over the finite support, with $[κ (x) : k]$ finite, and $D$ is effective, written $D \geq 0$ , when $n_{x} \geq 0$ for every $x$ . (Divisors on a smooth proper curve)

Proof

technique · direct; unfold effectiveness as nonnegativity of coefficients and bound each term of the finite degree sum below

1.1F2F3

Unwinding hypotheses. By [F2] the divisor $D$ has finite support, so the sum in the definition of $\deg_{k} D$ is a finite sum over the finite set $Supp (D)$ . By [F3] effectiveness of $D$ means $n_{x} \geq 0$ for every $x$ .

1.2F2

Residue degrees are positive. For each closed point $x$ of $C$ the residue field $κ (x)$ is a finite extension of $k$ [F2], and the structure map $k \to κ (x)$ is injective with image a subfield, so $\dim_{k} κ (x) \geq 1$ ; being finite over $k$ , that dimension is an integer at least one. Therefore $[κ (x) : k] \geq 1$ for every $x$ .

2.1F2step 1.1step 1.2

Nonnegativity. Every summand of $\deg_{k} D = \sum_{x} n_{x} [κ (x) : k]$ is a product of the nonnegative integer $n_{x}$ from step 1.1 and the positive integer $[κ (x) : k]$ from step 1.2, hence is nonnegative; the sum is finite by step 1.1, so $\deg_{k} D \geq 0$ .

3.1F2step 1.2step 2.1

Vanishing. If $D = 0$ then all coefficients $n_{x}$ vanish and $\deg_{k} D$ is the empty sum $0$ ; conversely if $\deg_{k} D = 0$ while $D$ is effective, then step 2.1 exhibits $\deg_{k} D$ as a sum of finitely many nonnegative terms, so every summand vanishes, and since each $[κ (x) : k] \geq 1$ by step 1.2 we get $n_{x} = 0$ for all $x \in Supp (D)$ ; hence $D = 0$ .

4.1

Conclusion. For an effective divisor $D$ on a proper geometrically integral curve $C$ over $k$ the degree $\deg_{k} (D) = \sum_{x} n_{x} [κ (x) : k]$ is a nonnegative integer by step 2.1, and it vanishes exactly when $D$ is the zero divisor by step 3.1. The claim was stated for the proper curve $C$ , whose underlying space has dimension one by [F1], so the residue fields entering the sum are those of the closed points as in [F2] and the alternative smooth-case description of [F4] is not needed here. ∎

Depends on

Used by

A degree-zero line bundle with a nonzero section is trivial Corollary
No sections in negative degree Corollary
A nontrivial degree-zero line bundle has no nonzero section Counterexample
Adding points never raises h¹, and h¹ stabilizes Lemma
An effective divisor of degree zero is empty Lemma
Euler characteristic changes by the residue degree Lemma
Every divisor is a finite signed sum of points Lemma
The exact sequence for adding one point to a divisor Lemma
Negative-degree line bundles have no nonzero sections Theorem

Dependency tree · two levels

27 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

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