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.

Residues of exact differentials vanish

Statement

Assume the Axiom of Choice as inherited from the completion and coefficient-field/residue suppliers. Let $k$ be a field, $C$ a smooth integral curve over $k$ , and $p$ a closed point whose residue field $κ (p)$ is finite separable over $k$ . For every $f \in k (C)$ , the exact differential $d f$ has residue zero at $p$ : ${res}_{p} (d f) = 0.$ Consequently the residue functional kills the image of $d ⁣ : k (C) \to Ω_{k (C) / k}^{1}$ , and adding an exact differential does not change the residue at any point where the coefficient-trace residue is defined. This 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$ , the local coefficient-trace residue of Residue of a rational differential at a separable closed point at $p$ , and a rational function $f \in K = k (C)$ .

[F1]

The local construction of Residue of a rational differential at a separable closed point applies at $p$ and uses only the local ring $O_{C, p}$ : choosing a uniformizer $t$ of the discrete valuation ring $O_{C, p}$ gives a $k$ -compatible coefficient field $κ (p) ↪ {\hat{O}}_{C, p}$ and an isomorphism ${\hat{O}}_{C, p} ≅ κ (p) [⁣ [t] ⁣]$ , so that $K = Frac (O_{C, p})$ embeds in $κ (p) ((t))$ and every rational differential $ω$ is written $ω = a d t$ with $a \in K$ whose Laurent expansion in $κ (p) ((t))$ has a residue of its $- 1$ -coefficient; the residue is ${res}_{p} (ω) = {Tr}_{κ (p) / k} ([t^{- 1}] a) \in k,$ it is $k$ -linear in $ω$ , and it depends only on the local data 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]

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

[F3]

Formal calculus in $κ (p) ((t))$ (Formal Laurent series $K ((x))$ , their order, derivative, and residue): the formal derivative $D$ is defined coefficientwise by $D (t^{n}) = n t^{n - 1}$ , so $D (\sum_{n} a_{n} t^{n}) = \sum_{n} n a_{n} t^{n - 1}$ with no division by integers; the formal residue is ${res}_{t} (g) = [t^{- 1}] g$ . The coefficient field $κ (p)$ is embedded compatibly with $k$ by Residue of a rational differential at a separable closed point, so $D$ kills the image of $k$ and the composition $D \circ j_{t}$ is a $k$ -derivation of $K$ into $κ (p) ((t))$ , where $j_{t} : K ↪ κ (p) ((t))$ is the completion embedding. This is the derivation passed through the universal property in [F6]; no differential-module identification for the completed field is asserted.

[F4]

The residue ${res}_{p} (ω)$ of [F1] does not depend on the choice of uniformizer $t$ (The residue is independent of the uniformizer).

[F5]

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

[F6]

The universal property of algebraic Kähler differentials (Derivations are maps out of Ω): for a ring map $k \to K$ and a $K$ -module $M$ , every $k$ -derivation $δ : K \to M$ is uniquely of the form $Δ \circ d$ for a $K$ -linear map $Δ : Ω_{K / k}^{1} \to M$ .

[F7]

The Axiom of Choice is The Axiom of Choice.

Proof

Proof technique: direct; expand $f$ as a formal Laurent series in a uniformizer and compute the $- 1$ -coefficient of its formal derivative.

1.1F1F2given

(Set-up.) Let $t$ be a uniformizer of $O_{C, p}$ , let $j_{t} : K ↪ κ (p) ((t))$ be the completion embedding, and write $j_{t} (f) = \sum_{n \geq N} a_{n} t^{n}$ . By [F2] the exact differential is $d f = a d t$ for a unique $a \in K$ , and by [F1] its residue is ${res}_{p} (d f) = {Tr}_{κ (p) / k} ([t^{- 1}] j_{t} (a))$ .

2.1F2F3F6step 1.1

(The derivative is formal through the universal property.) Give $M = κ (p) ((t))$ its $K$ -module structure through $j_{t}$ . By [F3], $δ_{t} : = D \circ j_{t} : K \to M$ is a $k$ -derivation; [F6] therefore gives a unique $K$ -linear map $Δ_{t} : Ω_{K / k}^{1} \to M$ with $Δ_{t} (d g) = D (j_{t} (g))$ for every $g \in K$ . Since $j_{t} (t) = t$ , one has $Δ_{t} (d t) = 1$ . By [F2], $d f = a d t$ , so $Δ_{t} (d f) = j_{t} (a)$ and also $Δ_{t} (d f) = D (j_{t} (f))$ . Thus the Laurent expansion of the algebraic coefficient $a$ is exactly $D (j_{t} (f))$ . This comparison uses only the universal property for $Ω_{K / k}^{1}$ and makes no claim that $Ω_{κ (p) ((t)) / k}^{1} = κ (p) ((t)) d t$ .

3.1F3step 2.1algebra

(The critical coefficient.) The coefficient of $t^{- 1}$ in $D (j_{t} (f)) = \sum_{n} n a_{n} t^{n - 1}$ receives a contribution only from $n = 0$ , and that contribution is $0 \cdot a_{0} = 0$ ; every other index contributes to a different power. By step 2.1, $[t^{- 1}] j_{t} (a) = 0$ .

4.1F1F5step 1.1step 3.1

(Residue of the exact differential.) Applying the trace of [F1] to the vanishing coefficient just found and using [F5], ${res}_{p} (d f) = {Tr}_{κ (p) / k} (0) = 0$ ; this is the asserted vanishing at $p$ .

5.1F3F4step 4.1

(Independence of the uniformizer, all characteristics.) The vanishing just proved was computed in the uniformizer $t$ , and by [F4] the residue does not depend on that choice, so ${res}_{p} (d f) = 0$ for every uniformizer of $O_{C, p}$ ; the computation of the formal derivative used the integer coefficients $n$ literally, with no division by an integer at any point, so it is valid in every characteristic, including characteristics dividing an exponent occurring in $f$ .

6.1F1F7step 4.1step 5.1∎

(Consequences.) Since $f \in K$ was arbitrary, the residue functional kills the image of $d ⁣ : K \to Ω_{K / k}^{1}$ ; if a rational differential is changed by an exact differential, $ω^{'} = ω + d f$ , then ${res}_{p} (ω^{'}) = {res}_{p} (ω) + {res}_{p} (d f) = {res}_{p} (ω)$ by the $k$ -linearity of ${res}_{p}$ in [F1]. This includes $f = 0$ and $f \in k$ , for which $d f = 0$ . The Axiom of Choice [F7] is inherited from the completion and power-series suppliers used in [F1] and [F3].

Depends on

Used by

The residue pairing is well defined on cohomology Lemma

Dependency tree · two levels

53 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)