The order system of a Dedekind domain #
The abstract OrderSystem of TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic packages the
order-of-vanishing data needed to build principal divisors and the divisor class group. This
file supplies the roadmap's intended concrete instance of that data: a Dedekind domain R
with fraction field K. Its height-one spectrum HeightOneSpectrum R is the set of
codimension-one points of Spec R (an affine model of a curve, or the ring of integers of a
number field), and the v-adic valuation gives each point an order-of-vanishing homomorphism
on the multiplicative group Kˣ of nonzero rational functions.
Concretely we build:
adicOrd R K v : Additive Kˣ →+ ℤ, the order of vanishingord_v(f) = -log v(f)of a nonzero rational functionfat the height-one primev(the sign makes a uniformizer have order+1, i.e. a simple zero);OrderSystem.ofDedekindDomain R K : OrderSystem (HeightOneSpectrum R) (Additive Kˣ), whose finiteness condition is exactly the statement that a nonzero rational function has zeros and poles at only finitely many primes;(OrderSystem.ofDedekindDomain R K).ClassGroup, the resulting Weil-divisor presentation of the class group (the quotient of Weil divisors by principal divisors; its isomorphism toClassGroup Ris not constructed here);- the sanity check that the principal divisor of a nonzero integral element is effective
(an element of
Rhas no poles).
The roadmap explicitly anticipates this instantiation: "Instantiate G with Additive Kˣ
for the multiplicative group of a function field K: then ord x is the order of vanishing
ord_x(f)". This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A ("Divisors on
a curve: Weil divisors ⊕_x ℤ", "principal divisors", "Cl(X)"), grounding the abstract
order-system API in Mathlib's Dedekind-domain adic valuations.
We do not claim the weighted-degree-zero property here: for a general Dedekind domain (e.g.
ℤ) there is no product formula, so a principal divisor need not have degree zero. That holds
only for proper curves over a field (and number fields with the archimedean places included),
and is later geometric input.
This reuses Mathlib's IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero (the multiplicative
v-adic valuation Kˣ →* Multiplicative ℤ, whose multiplicativity adicOrd inherits), the
WithZero.log logarithm on ℤᵐ⁰, and IsDedekindDomain.HeightOneSpectrum.Support.finite
(finiteness of the support of a rational function); no external mathematics is vendored.
The order of vanishing ord_v(f) = -log v(f) of a nonzero rational function f : Kˣ at a
height-one prime v of a Dedekind domain R, as a homomorphism Additive Kˣ →+ ℤ. It is the
additive, sign-flipped form of Mathlib's multiplicative valuation
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero v : Kˣ →* Multiplicative ℤ; the sign is
chosen so that a uniformizer at v has order +1 (a simple zero) and a pole has negative
order.
Equations
Instances For
The computational form of adicOrd: the order at v of an element u : Additive Kˣ is the
sign-flipped logarithm -log v(u) of its v-adic valuation, where the underlying rational
function is (Additive.toMul u : Kˣ) : K. The minus sign makes a uniformizer have order +1.
The computational form of adicOrd applied to Additive.ofMul u for a multiplicative unit
u : Kˣ: it is the sign-flipped logarithm -log v(u) of the v-adic valuation of u : K.
The order ord_v(f) is nonnegative exactly when f is integral at v, i.e. has
valuation at most one.
Mathlib's exponent of a principal fractional ideal is the sign-flipped logarithm of the
corresponding height-one valuation. Stated at the multiplicative-units level u : Kˣ, matching
Mathlib's toPrincipalIdeal R K : Kˣ →* _; the order-system/Additive form is recovered by
adicOrd_eq_fractionalIdeal_count.
The v-adic order of a rational function agrees with Mathlib's exponent of the
corresponding principal fractional ideal.
The order system of a Dedekind domain R with fraction field K: its points are the
height-one primes v of R, the group is the multiplicative group Kˣ of nonzero rational
functions, and the order at v is the v-adic order of vanishing. The finiteness condition is
exactly the statement that a nonzero rational function has zeros and poles at only finitely many
primes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The order map of the Dedekind-domain order system at a height-one prime v is the v-adic
order of vanishing adicOrd R K v.
The coefficient of the principal divisor of f : Kˣ at a height-one prime v is the
v-adic order of vanishing -log v(f).
The coefficient of a Dedekind-domain principal divisor agrees with Mathlib's exponent of the corresponding principal fractional ideal.
A height-one prime lies in the support of a principal divisor exactly when the corresponding valuation is not one.
A coefficient of a principal divisor is positive exactly when the corresponding valuation is strictly less than one.
The principal divisor of a nonzero integral element is effective: an element of R has
no poles, only zeros. The element is presented as any unit u : Kˣ whose value is
algebraMap R K r. This is the divisor-of-functions sanity check that rules out a vacuous
order system.
The divisor of a nonzero integral element r : R, presented as a unit u : Kˣ with value
algebraMap R K r, has a strictly positive coefficient (a genuine zero) at v exactly when r
lies in the prime v.
The support of the divisor of a nonzero integral element r : R, presented as a unit
u : Kˣ with value algebraMap R K r, is the set of height-one primes containing r.