LemmaStatement: 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.

Fibre degree sum with ramification and residue degrees

Statement

Assume the Axiom of Choice. Let $f : C \to D$ be a nonconstant morphism of smooth proper geometrically integral curves over a field $k$ , put $n = \deg (f)$ , and let $q$ be a closed point of $D$ . Then the fibre $f^{- 1} (q)$ is finite and $\sum_{p \in f^{- 1} (q)} e_{p} [κ (p) : κ (q)] = n,$ where $e_{p}$ is the ramification index of $f$ at $p$ .

Facts & Assumptions

Given: AC, a nonconstant morphism $f : C \to D$ of smooth proper geometrically integral curves over $k$ , $n = \deg (f)$ , and a closed point $q \in D$ .

[F1]

Under AC, such a morphism is finite and surjective, and its degree definition establishes the weighted fibre formula $\sum_{p \in f^{- 1} (q)} {ord}_{p} (f^{*} t_{q}) [κ (p) : κ (q)] = \deg (f),$ where $t_{q}$ is a uniformizer at $q$ . The fibre is finite: on an affine neighbourhood of $q$ it is the spectrum of a finite-dimensional residue-field algebra, whose Artinian decomposition has finitely many local factors. (Degree of a nonconstant morphism of curves)

[F2]

Under the same hypotheses and AC, the ramification index is $e_{p} = {ord}_{p} (f^{*} t_{q})$ , independently of the chosen uniformizer. (Ramification index of a morphism of curves)

[A1]

Assume the Axiom of Choice, inherited from the finite curve-map, smooth-curve DVR and algebraic suppliers in [F1] and [F2]. (The Axiom of Choice)

Proof

technique · direct; apply the fibre formula already established in the degree definition, with the ramification-index notation

1.1F1A1

The hypotheses and AC license [F1], so $f^{- 1} (q)$ is finite and its weighted order sum equals $\deg (f) = n$ .

2.1F2step 1.1∎

At each point $p$ of this finite fibre, [F2] identifies ${ord}_{p} (f^{*} t_{q})$ with $e_{p}$ . Substitution in step 1.1 gives $\sum_{p \in f^{- 1} (q)} e_{p} [κ (p) : κ (q)] = n$ . This uses no separability assumption and no further Choice.

Depends on

Used by

Dependency tree · two levels

29 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)
Jiahui Gao and Shouwu Zhang, Lectures on Algebraic Geometry (December 14, 2019), Ch. 7 (standard reference, not scraped)
Ravi Vakil, The Rising Sea (version of October 21, 2025), Chs. 19 and 21 (standard reference, not scraped)