DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Path integral of a holomorphic differential on a Riemann surface

Definition

Let $X$ be a Riemann surface, let $ω$ be a holomorphic differential on $X$ , and let $γ : [a, b] \to X$ be a continuous path. In a holomorphic chart $z : U \to D$ , write $ω = h (z) d z$ . A local primitive of $ω$ on a coordinate disk $U$ is a holomorphic function $H_{U} : U \to C$ of the form $H_{U} = G \circ z$ , where $G^{'} = h$ on $D$ . For any finite subdivision $a = t_{0} < \dots < t_{N} = b$ and local primitives $H_{j}$ defined on coordinate disks $U_{j}$ with $γ ([t_{j - 1}, t_{j}]) \subseteq U_{j}$ , set $\int_{γ} ω : = \sum_{j = 1}^{N} (H_{j} (γ (t_{j})) - H_{j} (γ (t_{j - 1}))) .$ For $a = b$ define the integral to be zero. The value is independent of the subdivision, charts, and local primitives, and is called the path integral of $ω$ along $γ$ .

The path integral is additive under concatenation, changes sign under path reversal, is zero on a constant path, and is $C$ -linear in $ω$ . When $γ$ is piecewise $C^{1}$ , it agrees in every chart with the usual complex contour integral of the local coefficient $h (z) d z$ . Continuous paths are included so that the topological side loops of a polygonal homology model can be integrated without assuming that a chosen topological representative is already piecewise smooth.

Facts & Assumptions

Given: A Riemann surface $X$ , a holomorphic differential $ω$ on $X$ , and a continuous path $γ : [a, b] \to X$ .

[F1]

In a holomorphic chart, a meromorphic differential is $h (z) d z$ ; for a holomorphic differential $h$ is holomorphic, and the coefficients obey the differential transition law (Meromorphic differentials, orders and residues).

[F2]

A holomorphic coefficient equals its convergent Taylor series locally, and an analytic function has a primitive on a neighborhood of each point (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain, Every complex analytic function has a primitive on a neighbourhood of each point).

[F3]

A holomorphic function with zero derivative on a connected plane domain is constant (A holomorphic function with zero derivative on a domain is constant, A complex domain is a nonempty connected open subset of $C$ ).

[F4]

The image of a connected space under a continuous map is connected (A continuous image of a connected space is connected, and connectedness is a topological property).

[F5]

The interval $[a, b]$ is compact when $a < b$ , and every open cover of a compact metric space has a Lebesgue number (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover).

[F6]

Under $C ≅ R^{2}$ , a piecewise- $C^{1}$ complex path is rectifiable; a continuous coefficient has a complex line integral on every rectifiable contour (Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations, Rectifiable complex contours, reversal, concatenation, closedness, and orientation, $C$ is the real coordinate plane, with coordinate arithmetic, A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces, Continuous integrands have complex and absolute line integrals along every rectifiable path, The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral).

[F7]

If $H^{'} = h$ on a neighborhood of the trace of a rectifiable contour, then $\int_{γ} h (z) d z = H (γ (b)) - H (γ (a))$ (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

[F8]

Holomorphic coordinate changes are smooth in real coordinates, so a piecewise- $C^{1}$ path on $X$ has piecewise- $C^{1}$ coordinate paths (Riemann surfaces and holomorphic atlases, Holomorphic functions are real analytic and smooth in their two real coordinates).

[F9]

The derivative of a composite of complex-differentiable maps obeys the complex chain rule (The chain rule for complex derivatives).

[F10]

Finite choice is a theorem of ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Verification

Given: The data above and, when relevant, a finite collection of paths and holomorphic differentials.

Proof technique: direct local construction and comparison on overlaps.

1.1F1F2F5F10given

If $a < b$ , around each point of the compact trace $γ ([a, b])$ choose a coordinate disk on which [F2] gives a local primitive of the coefficient in [F1]. The preimages of these disks cover $[a, b]$ ; [F5] supplies a Lebesgue number, so a finite subdivision can be chosen with each subpath contained in one primitive disk. There are only finitely many disk and primitive choices, so [F10] suffices and no unrestricted choice is used. If $a = b$ , the empty subdivision gives the stated zero convention.

1.2F1F3given

On a fixed coordinate disk, two local primitives have the same derivative $h$ in its coordinate; their difference has zero derivative and is constant by [F3]. Therefore replacing a chosen primitive on one subinterval does not change its endpoint increment.

1.3F1F3F4F9given

Suppose a connected subpath lies in two coordinate disks $U, V$ , with coordinates $z, w$ and local primitives $H_{U}, H_{V}$ . Its image lies in one connected component of $U \cap V$ by [F4]. Put $G_{U} = H_{U} \circ z^{- 1}$ and $G_{V} = H_{V} \circ w^{- 1}$ . In the $z$ coordinate, [F1] and [F9] give $\frac{d}{d z} (G_{V} (w (z)) - G_{U} (z)) = h_{V} (w (z)) w^{'} (z) - h_{U} (z) = 0$ , so [F3] makes this difference constant on that component. The two endpoint increments are equal.

2.1step 1.1step 1.2step 1.3algebra

Compare any two admissible subdivisions by taking the finite common refinement of their breakpoints. On each refined subinterval, the two original primitive disks both contain the path image, so step 1.3 identifies their increments; splitting an increment inside one disk changes nothing because the same primitive values telescope. Thus the two defining sums agree, proving independence of subdivision, chart, and local primitive.

3.1step 2.1algebra

Splitting the defining sum at a join proves additivity under concatenation; reversing each subinterval swaps the two endpoint values and negates the sum; for a constant path every endpoint increment is zero. If $λ, μ \in C$ , local primitives for $λ ω_{1} + μ ω_{2}$ are $λ H_{1} + μ H_{2}$ , so the formula is complex-linear.

4.1F6F7F8step 2.1∎

If $γ$ is piecewise $C^{1}$ , refine the partition so each coordinate subpath is piecewise $C^{1}$ . By [F6] it is a rectifiable contour, and [F7] identifies its usual contour integral with the increment of the local primitive. Summing the finitely many chart segments gives exactly the path integral defined above.

Remarks

For a continuous path, this definition uses only local primitives and endpoint differences, not a derivative of the path. For a piecewise- $C^{1}$ path it recovers the usual contour integral in local coordinates. No choice principle beyond finite choice is used.

Depends on

Used by

The Abel-Jacobi map Definition
The period pairing and the period subgroup Definition
Base-point cancellation for degree-zero divisors Example
Period matrix and Jacobian of the pentagon curve Example
Periods of a complex torus Example
Principal divisors have vanishing Abel-Jacobi class Lemma
The Abel-Jacobi map is well defined and its degree-zero extension is base-point independent Lemma
The period pairing is well defined and computed by integration Lemma
Abel's theorem for divisors Theorem
Jacobi inversion Theorem
The Abel-Jacobi map embeds a positive-genus surface Theorem

Dependency tree · two levels

118 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

Eduard Looijenga, Riemann Surfaces (2007 author lecture notes) (standard reference, not scraped)
Karl Otto Forster, Lectures on Riemann Surfaces (GTM 81) (standard reference, not scraped)