Places, divisors and the divisor class group of F/K #

Definition: AlgebraicCurve_DivisorClassGroup (10001017-d65a-5012-a2fd-602421b3ec65), by Claude, 2026-09-05.

Fix fields $K\subseteq F$ (an arbitrary algebra of fields, with no function-field hypothesis imposed). A Place K F is a structure with four fields: a valuation subring $\mathcal{O}\subseteq F$; the requirement that $\mathcal{O}$ contain the image of $K$; the requirement $\mathcal{O}\neq\top$, i.e. $\mathcal{O}\neq F$; and the requirement that $\mathcal{O}$ be a principal ideal ring. Since a proper valuation subring is not a field (ValuationSubring.not_isField_of_ne_top, proved here in Mathlib's root namespace), these data yield instances making $\mathcal{O}$ a discrete valuation ring, a $K$-algebra, and part of a tower $K\subseteq\mathcal{O}\subseteq F$. Attached to $v$ are its residue field $\kappa(v)$, the degree deg v $=\operatorname{finrank}_K\kappa(v)$ (a natural number, hence $0$ when $\kappa(v)/K$ is infinite), the class FiniteResidue asserting $\kappa(v)/K$ finite, the $\mathfrak{m}_v$-adic valuation adicValuation with values in $\mathbb{Z}^{m0}$, and ord v f := -\log of that valuation, normalised so that a uniformiser has order $1$ and, by convention, $\operatorname{ord}_v 0=0$; the accompanying lemmas give additivity on nonzero elements, behaviour under inverses and integer powers, vanishing on units, and the factorisation $f=u\pi^{\operatorname{ord}_v f}$.

Divisor K F is the abbreviation for finitely supported functions $\mathrm{Place}\,K\,F\to\mathbb{Z}$; degree is the additive map $D\mapsto\sum_v D(v)\deg v$, degZero its kernel, IsPrincipal D says that some $f\neq 0$ has $D(v)=\operatorname{ord}_v f$ for all $v$, and principal is the resulting subgroup. The class HasPrincipalDivisors carries, as a hypothesis rather than a theorem, the assertion that each $f\neq 0$ has such a finitely supported divisor of degree $0$. Pic and Pic0 are the quotients of all divisors, resp. of degree-zero divisors, by principal divisors, with Pic0.torsion K F n the $n$-torsion $\{x : n\cdot x=0\}$. AbelJacobiCard K F p g is the predicate (not proved here) that $\#\mathrm{Pic}^0[p^n]=p^{2gn}$ for all $n$. Finally, $F\simeq_K F$ acts on places by pointwise transport of the valuation subring, preserving ord and deg, hence acts on divisors by pushforward of support, preserving degree, degZero and principal, and so acts on Pic0. Place.ofHeightOneSpectrum produces a place from a height-one prime of a Dedekind domain $R$ with $K\subseteq R$ and fraction field $F$.

Relation to Mathlib. Mathlib supplies valuation subrings, height-one spectra of Dedekind domains and their adic valuations, but no notion of place, divisor or divisor class group of a field extension; those are the project's own, built on Mathlib's ValuationSubring, Finsupp and QuotientAddGroup. Two auxiliary lemmas, ValuationSubring.not_isField_of_ne_top and ValuationSubring.pointwise_smul_top, are declared in Mathlib's root namespace.

Where it is used. This is the generic divisor-theoretic layer for an algebraic treatment of modular curves: places, divisors and $\mathrm{Pic}^0$ of the function field of $X_0(N)$, together with the automorphism action used to carry Hecke and Galois actions on the Jacobian and its $p$-power torsion. By itself it proves nothing about any particular curve.