Places above a place via primes of the integral closure #

Definition: AlgebraicCurve_PlacesOverDVR (71585f74-5f90-5e62-b565-e6e34df02a7a), by Claude, 2026-09-05.

Throughout, $K \subseteq F \subseteq F'$ are fields with $F'/F$ finite and separable (compatible algebra structures and scalar tower), and a place of $F/K$ means an element of the project's structure Place K F: a valuation subring $\mathcal{O}_v \subsetneq F$ containing the image of $K$ whose ideals are all principal, so that $\mathcal{O}_v$ is a discrete valuation ring with normalised order function $v.\mathrm{ord}$ and residue field.

The first construction is an affine chart. For a Dedekind domain $R$ with $R \subseteq F$ as fraction field and a place $w$, given the hypothesis that every $r \in R$ maps into $\mathcal{O}_w$, center R w hw is the contraction $\mathfrak{m}_w \cap R$, i.e. the preimage of the maximal ideal of $\mathcal{O}_w$ under the induced map $R \to \mathcal{O}_w$; it is prime, nonzero, hence a height-one prime centerHeightOneSpectrum R w hw, and $\mathcal{O}_w$ coincides with the localisation $\mathcal{O}_{R,\mathfrak{p}}$ attached to it by Mathlib's valuationSubringAtPrime. Membership in the centre is characterised by $0 < w.\mathrm{ord}$, and for fixed $r_0 \neq 0$ only finitely many places satisfy both conditions.

For a place $v$ of $F/K$, integralClosureAt F' v is the integral closure $C_v$ of $\mathcal{O}_v$ in $F'$, which is a Dedekind domain, module-finite over $\mathcal{O}_v$, with fraction field $F'$. For $w$ a place of $F'/K$ with $w|_F = v$ (equality of $w.\mathrm{restrict}\,F$, the contraction of $\mathcal{O}_w$ to $F$, with $v$), fiberCenter F' v hw is the centre $\mathfrak{m}_w \cap C_v$ as a height-one prime of $C_v$; it lies over $\mathfrak{m}_v$, and $\mathcal{O}_w$ is its localisation. Conversely placeOfPrime P is the place of $F'/K$ with valuation ring $(C_v)_{\mathfrak{P}}$, and it restricts to $v$. These are mutually inverse: fiberEquiv F' v is the resulting bijection between $\{w : w|_F = v\}$ and the height-one spectrum of $C_v$. Consequently the set of places above $v$ is finite, and fiberOver F' v is it as a finset, with membership criterion $w|_F = v$, cardinality equal to that of Mathlib's primesOverFinset of $\mathfrak{m}_v$ in $C_v$, and agreement with the fibre finset fiber of the divisor push/pull module under HasPrincipalDivisors K F'. Auxiliary results record that $\mathcal{O}_w$ is integrally closed (a root of a monic polynomial with coefficients in $\mathcal{O}_w$ lies in $\mathcal{O}_w$), the translation of maximal-ideal membership into positivity of $\mathrm{ord}$, and the identity $w.\mathrm{ord}(r) = e(w/F)\cdot v.\mathrm{ord}(r)$ for $r \in \mathcal{O}_v$.

Relation to Mathlib. Place is the project's own structure; Mathlib's height-one spectrum of a Dedekind domain, its valuationSubringAtPrime, primesOverFinset, and the theorems that the integral closure in a finite separable extension is Dedekind, module-finite and has the larger field as fraction field are used to identify the fibre of places above a place with a set of primes.

Where it is used. The fibre finset fiberOver and the ramification data it supports underlie the pullback and pushforward maps on divisors, the fundamental identity relating ramification indices and residue degrees, and hence the degree-zero divisor class groups of curves used in the formalisation.