Principal divisors on a normal proper curve have degree zero

Given: A field $k$, a normal proper curve $C$ over $k$ with generic point $\eta$ and function field $K={\mathcal{O}}_{C,\eta }=k(C)$, the Axiom of Choice, and an element $f\in K^{\times }$.

$C$ is an integral, proper, one-dimensional $k$-scheme of finite type over $k$, hence Noetherian; it is a normal locally Noetherian integral scheme. Its prime divisors are exactly its closed points, and for every closed point $x$ the local ring ${\mathcal{O}}_{C,x}$ is a discrete valuation ring with fraction field $K$, whose normalized valuation at $f$ is ${\mathrm{ord}}_x(f)$; in particular ${\mathrm{ord}}_x(f)=0$ if and only if $f$ is a unit of ${\mathcal{O}}_{C,x}$. The residue field $\kappa (x)$ is finite over $k$ (Degree divisor proper curve, Weil divisor normal noetherian scheme, Order codimension one rational function, Height-one localizations of normal Noetherian domains are DVRs).

The principal Weil divisor ${\mathrm{div}}_W(f)={\sum }_Z{\mathrm{ord}}_Z(f)[Z]$, summed over the prime divisors $Z$ of $C$, is a well-defined element of the free abelian group $\mathrm{Div}(C)$ generated by the prime divisors, and on the integral curve $C$ it is the finite sum ${\sum }_x{\mathrm{ord}}_x(f)[x]$ over the closed points $x$; its $k$-degree is computed coefficientwise as ${\sum }_x{\mathrm{ord}}_x(f)[\kappa (x):k]$, which is a finite sum with values in $\mathbb{Z}$ (Principal weil divisor and class group, Degree divisor proper curve).

The Axiom of Choice implies the Axiom of Dependent Choice, and the finiteness statement just used by [F2] is proved from Dependent Choice (AC implies DC implies countable choice, The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain).

If $f$ is algebraic over $k$, then $f$ and $f^{-1}$ are global units of $C$, that is, $f\in \mathrm{\Gamma }(C,{\mathcal{O}}_C{)}^{\times }$ (Proper normal curve rational function map).

If $f$ is transcendental over $k$, then there is a finite locally free morphism ${\phi }_f:C\to {\mathbb{P}}_k^1$ of degree $d=[K:k(f)]$ with ${\phi }_f^{\mathrm{\#}}(t)=f$ on the standard chart $t$, and: the fibre ${\phi }_f^{-1}(0)$ consists exactly of the closed points $x$ with ${\mathrm{ord}}_x(f)>0$, the fibre ${\phi }_f^{-1}(\mathrm{\infty })$ consists exactly of the closed points $x$ with ${\mathrm{ord}}_x(f)<0$, and ${\sum }_{{\phi }_f(x)=0}{\mathrm{ord}}_x(f)[\kappa (x):k]=d,{\sum }_{{\phi }_f(x)=\mathrm{\infty }}(-{\mathrm{ord}}_x(f))[\kappa (x):k]=d\mathrm{.}$ Both sums are finite and every summand is a positive integer (Proper normal curve rational function map, Fibre degree of the finite locally free map to the projective line).