Places of rational function fields, and transport along field isomorphisms #

Definition: AlgebraicCurve_RatFuncPlaces (07390cff-bcbe-57c5-95cb-48ea897f5c4d), by Claude, 2026-09-05.

Throughout, a Place of a field extension $F/K$ is (as defined in the divisor class group module) a valuation subring $V \subseteq F$ containing the image of $K$, distinct from $F$, and a principal ideal ring; adicValuation is the $\mathbb{Z}^{\mathrm{m}0}$-valued valuation attached to the maximal ideal of $V$, ord is $-\log$ of it, and deg is $\dim_K$ of the residue field of $V$. The first group of results is the dictionary between these data: the valuation subring of adicValuation is $V$ itself, so $f \in V \iff v(f) \le 1$, an element of $V$ lies in the maximal ideal iff its value is $<1$, any valuation on $F$ with valuation subring $V$ is equivalent to adicValuation, and for $f \ne 0$ one has $\operatorname{ord}_v f = 0 \iff v(f) = 1$; adicValuation is registered as rank-one discrete and as trivial on $K$. For a Dedekind domain $R$ with fraction field $F$ sitting in a tower $K \to R \to F$, the place ofHeightOneSpectrum w attached to a height-one prime $w$ has $w$-adic valuation equivalent to its adicValuation; the map $w \mapsto$ place is injective, and for $q \in R$ nonzero, $\operatorname{ord}(q) \ne 0 \iff q \in w$.

Specialising to $R = K[X]$ and $F = K(X)$: heightOneSpectrumOfIrreducible is the height-one prime $(p)$ of an irreducible $p$, every height-one prime of $K[X]$ arises this way, and finitePlace hp is the corresponding place of $K(X)$. The composite of $K[X] \to V \to V/\mathfrak m$ has kernel $w$ and is surjective, giving a $K$-algebra isomorphism $K[X]/w \cong$ residue field, whence $\deg = \deg p$ when $w = (p)$. placeOfPoint a is the place at $X - a$; it is injective in $a$ and has degree $1$.

Finally, for a ring isomorphism $e : F \cong F'$ commuting with the structure maps from $K$, congrRingEquiv transports a place to the place with valuation subring the preimage of $V$ under $e^{-1}$ (i.e. $e(V)$), with $\operatorname{ord}_{e_*v}(e f) = \operatorname{ord}_v f$, a $K$-algebra isomorphism of residue fields, equality of degrees, and congrEquiv, the resulting bijection $\mathrm{Place}\,K\,F \simeq \mathrm{Place}\,K\,F'$ with inverse induced by $e^{-1}$.

Relation to Mathlib. Mathlib supplies the $w$-adic valuations of a Dedekind domain (IsDedekindDomain.HeightOneSpectrum), valuation subrings and RatFunc; the Place structure is the project's own, and this module provides the comparison between the two descriptions, the classification of places of $K(X)$ coming from $K[X]$, and the transport of places along an isomorphism of extensions of $K$.

Where it is used. These places supply the local data on rational function fields used when a genus-zero modular curve is presented as a $j$-line: the places of $K(j)$ at $K$-rational points are obtained from placeOfPoint and carried across the identification of the function field with $K(X)$ by congrEquiv, feeding the divisor and degree computations built on the divisor class group module.