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

The residue is independent of the uniformizer

Statement

Assume the Axiom of Choice as inherited from the completion and power-series suppliers. Let $k$ be a field, let $C$ be a smooth integral curve over $k$ , and let $p$ be a closed point whose residue field $κ (p)$ is finite separable over $k$ . Use the $k$ -compatible coefficient field $κ (p) ↪ {\hat{O}}_{C, p}$ of Residue of a rational differential at a separable closed point, and let $t$ and $t^{'}$ be uniformizers of $O_{C, p}$ . Write $t^{'} = θ (t) = t u (t)$ with $u (t)$ a unit of $κ (p) [⁣ [t] ⁣]$ . For a rational differential $ω$ write $ω = a d t = a^{'} d t^{'}, a, a^{'} \in k (C),$ using A uniformizer differential generates the module of differentials, and expand $a$ in $κ (p) ((t))$ and $a^{'}$ in $κ (p) ((t^{'}))$ . Then $[t^{- 1}] a = [t^{' - 1}] a^{'},$ so the coefficient traces agree, ${Tr}_{κ (p) / k} ([t^{- 1}] a) = {Tr}_{κ (p) / k} ([t^{' - 1}] a^{'})$ , and the residue ${res}_{p} (ω)$ of Residue of a rational differential at a separable closed point does not depend on the choice of uniformizer. The formal change-of-parameter identity holds in every characteristic.

Facts & Assumptions

Given: a field $k$ , a smooth integral curve $C$ over $k$ , a closed point $p$ with $κ (p)$ finite separable over $k$ , uniformizers $t, t^{'}$ of $O_{C, p}$ , the coefficient field $κ = κ (p)$ of Residue of a rational differential at a separable closed point, and a rational differential $ω \in Ω_{k (C) / k}^{1}$ .

[F1]

The local construction of Residue of a rational differential at a separable closed point applies at $p$ : the maximal-adic completion ${\hat{O}}_{C, p}$ receives a unique $k$ -compatible coefficient field $κ = κ (p)$ , and for every uniformizer $s$ there is an isomorphism ${\hat{O}}_{C, p} ≅ κ [⁣ [s] ⁣]$ compatible with the coefficient field, so the function field $K = k (C) = Frac (O_{C, p})$ embeds in $κ ((s))$ ; the construction uses only the local ring at $p$ (Residue of a rational differential at a separable closed point, Local rings at closed points of smooth curves are discrete valuation rings).

[F2]

Every uniformizer of the discrete valuation ring $O_{C, p}$ generates its maximal ideal; hence $t^{'} = θ (t)$ for some $θ \in κ [⁣ [t] ⁣]$ with $θ = t u (t)$ , $u \in κ [⁣ [t] ⁣]^{\times}$ , and $θ$ has nonzero linear coefficient $u (0)$ ; conversely every such series defines a uniformizer of the completed DVR $κ [⁣ [t] ⁣]$ . The given $t^{'}$ is an actual uniformizer of $O_{C, p}$ , while the converse here is only about the completed DVR (Local rings at closed points of smooth curves are discrete valuation rings, $K ⟦ x ⟧$ embeds in $K ((x))$ as the nonnegative-order subring; every nonzero Laurent series is uniquely $x^{v_{x} (h)} u$ with $u \in K ⟦ x ⟧^{\times}$ and inverse $x^{- v_{x} (h)} u^{- 1}$ ).

[F3]

Formal calculus in $κ ((t))$ (Formal Laurent series $K ((x))$ , their order, derivative, and residue): the formal derivative $D$ acts coefficientwise by $D (t^{n}) = n t^{n - 1}$ and the formal residue is ${res}_{t} (f) = [t^{- 1}] f$ . For all $f, g \in κ ((t))$ one has ${res}_{t} (D f) = 0$ , and if the field contains $Q$ and $g \in t κ [⁣ [t] ⁣]$ has nonzero linear coefficient then ${res}_{t} ((F \circ g) D g) = {res}_{t} (F)$ for every Laurent series $F$ for which the substitution is defined (Formal residues satisfy integration by parts, logarithmic differentiation, and change of variables). Every nonzero $h \in κ ((t))$ factors as $t^{v} h_{0}$ with $h_{0}$ a unit of $κ [⁣ [t] ⁣]$ ( $K ⟦ x ⟧$ embeds in $K ((x))$ as the nonnegative-order subring; every nonzero Laurent series is uniquely $x^{v_{x} (h)} u$ with $u \in K ⟦ x ⟧^{\times}$ and inverse $x^{- v_{x} (h)} u^{- 1}$ ).

[F4]

The differential $d t$ is a $K$ -basis of $Ω_{K / k}^{1}$ , and likewise $d t^{'}$ is a $K$ -basis, so $ω$ has unique expressions $ω = a d t = a^{'} d t^{'}$ with $a, a^{'} \in K$ (A uniformizer differential generates the module of differentials).

[F5]

Let $j_{t} : K ↪ κ ((t))$ be the completion embedding and give $κ ((t))$ its $K$ -module structure through $j_{t}$ . Since the coefficient field is $k$ -compatible, the formal derivative $D_{t}$ kills $k$ , so $D_{t} \circ j_{t}$ is a $k$ -derivation of $K$ into this $K$ -module. By the universal property of algebraic Kähler differentials (Derivations are maps out of Ω) it is represented by a unique $K$ -linear map $Δ_{t} : Ω_{K / k}^{1} \to κ ((t))$ satisfying $Δ_{t} (d g) = D_{t} (j_{t} (g))$ . This does not assert a description of $Ω_{κ ((t)) / k}^{1}$ .

[F6]

For the finite extension $κ / k$ the field trace ${Tr}_{κ / k} : κ \to k$ is $k$ -linear (The norm $N_{K / F}$ and trace ${Tr}_{K / F}$ of a finite field extension).

[F7]

The Axiom of Choice is The Axiom of Choice.

Proof

technique · direct; type the change of parameter through algebraic differentials, then prove the Laurent coefficient identity by a universal integral-polynomial argument

1.1F1F2F4given

(Set-up.) With $K = k (C)$ and $κ = κ (p)$ , [F1] identifies the completion with $κ [⁣ [t] ⁣]$ and embeds $K$ in $κ ((t))$ ; [F2] gives $t^{'} = θ (t) = t u (t)$ with $u$ a unit and $θ$ of order one. Write $ω = a d t = a^{'} d t^{'}$ by [F4], and let $a^{'} = ψ (t^{'}) = \sum_{n \geq N} c_{n} t^{' n}$ be its $t^{'}$ -expansion, so $[t^{' - 1}] a^{'} = c_{- 1}$ .

2.1F3F5step 1.1algebra

(Change of variables for the coefficient.) Since $j_{t} (t^{'}) = θ (t)$ , [F5] gives $Δ_{t} (d t^{'}) = D_{t} (j_{t} (t^{'})) = θ^{'} (t)$ , while $Δ_{t} (d t) = 1$ ; applying the same $K$ -linear map to $a d t = a^{'} d t^{'}$ yields $j_{t} (a) = j_{t} (a^{'}) θ^{'} (t)$ . The $t$ -expansion of $a^{'}$ is $ψ (θ (t))$ , so $j_{t} (a) = ψ (θ (t)) θ^{'} (t)$ ; this derives the comparison through the universal property without differentiating a formal-series identity in $Ω_{K / k}^{1}$ .

2.2F2F3step 1.1algebra

(Monomials with exponent at least $- 1$ .) For $n \geq 0$ , $θ^{n} θ^{'}$ has no negative powers; for $n = - 1$ , $θ^{'} / θ = (t u)^{'} / (t u) = t^{- 1} + u^{'} / u$ and $u^{'} / u \in κ [⁣ [t] ⁣]$ , so $[t^{- 1}] (θ^{n} θ^{'})$ is $0$ for $n \geq 0$ and $1$ for $n = - 1$ , in every characteristic.

3.1F2F3step 2.2algebra

(Negative exponents in every characteristic.) For $n \leq - 2$ , write $θ^{n} θ^{'} = t^{n} u^{n} (u + t u^{'})$ ; only the coefficient of $t^{- n - 1}$ in the latter power series contributes, so $d_{n} : = [t^{- 1}] (θ^{n} θ^{'})$ is a Laurent polynomial over $Z$ in finitely many coefficients $u_{0}, u_{0}^{- 1}, u_{1}, \dots$ , where $u_{0} \neq 0$ . Let $U_{0}, U_{1}, \dots$ be algebraically independent over $Q$ , put $R = Q (U_{0}, U_{1}, \dots)$ , and use $u (t) = \sum_{j \geq 0} U_{j} t^{j}$ in $R [⁣ [t] ⁣]$ ; [F3] applies over $R$ to $F (U) = U^{n}$ and $g = θ = t u$ , giving $d_{n} = {res}_{t} (θ^{n} θ^{'}) = {res}_{t} (t^{n}) = 0$ . The Laurent polynomial therefore vanishes in $R$ and, since $Z [U_{0}, U_{0}^{- 1}, U_{1}, \dots] ↪ R$ is injective, is identically zero over $Z$ ; specializing the $U_{j}$ to coefficients of any unit in $κ [⁣ [t] ⁣]$ proves $[t^{- 1}] (θ^{n} θ^{'}) = 0$ over every field, including positive characteristic.

4.1F2step 1.1step 2.1step 3.1algebra

(Laurent series.) The negative-power tail $\sum_{N \leq n < 0} c_{n} θ^{n} θ^{'}$ is finite, and steps 2.2–3.1 show that its $t^{- 1}$ coefficient is exactly $c_{- 1}$ ; each term with $n \geq 0$ has no negative powers, so $[t^{- 1}] (ψ (θ (t)) θ^{'} (t)) = c_{- 1} = [t^{' - 1}] a^{'}$ . By step 2.1 this is $[t^{- 1}] a = [t^{' - 1}] a^{'}$ .

5.1F6F7step 4.1∎

(Traces and conclusion.) Applying the $k$ -linear trace ${Tr}_{κ / k}$ of [F6] to step 4.1 gives equality of the coefficient-trace residues defined by Residue of a rational differential at a separable closed point for $t$ and $t^{'}$ ; since $t^{'}$ was arbitrary, the residue is uniformizer-independent at every closed point with finite separable residue field, and the proof divided by no integers, so the identity holds in every characteristic. The Axiom of Choice [F7] is inherited from the completion and power-series suppliers.

Depends on

Used by

Cited to discharge well-definedness by Residue of a rational differential at a separable closed point.

Dependency tree · two levels

56 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

MIT 18.725 Algebraic Geometry (Fall 2015) course notes, Lectures 24-25 (standard reference, not scraped)
John Tate, Residues of differentials on curves, Ann. Sci. E.N.S. (4) 1 (1968) 149-159 (standard reference, not scraped)
Joseph Lipman, Residues, duality, and the fundamental class of a scheme-map (2011) (standard reference, not scraped)