The Weil divisor of an invertible fractional ideal #
For a Dedekind domain R with fraction field K,
TauCeti.AlgebraicGeometry.WeilDivisor.Dedekind.Basic turns the height-one spectrum of R into the
points of an affine curve and packages the order of vanishing of a rational function as the order
system OrderSystem.ofDedekindDomain R K. This basic module adds the Cartier side of that
picture: invertible fractional ideals of R are the Cartier divisors of the affine curve, and this
file identifies them with Weil divisors.
Concretely, a nonzero fractional ideal I has a well-defined v-adic multiplicity
FractionalIdeal.count K v I at each height-one prime v, zero for all but finitely many v, so
the assignment v ↦ count K v I is a Weil divisor. Because count is additive on products, this
gives a homomorphism
fractionalIdealDivisor : Additive (FractionalIdeal R⁰ K)ˣ →+ WeilDivisor (HeightOneSpectrum R)
from the group of invertible fractional ideals (every nonzero fractional ideal of a Dedekind domain
is invertible, FractionalIdeal R⁰ K being a semifield) to the free Weil-divisor group. This
homomorphism is an isomorphism: a fractional ideal is recovered from its multiplicities by the
factorization I = ∏_v v^(count K v I) (injectivity), and every finite integer combination of
primes is the divisor of the corresponding product of prime ideals (surjectivity). This is the
scheme-free, affine-chart form of the roadmap's Weil ≃ Cartier dictionary.
We also connect it to the order system already built: the divisor of the principal fractional ideal
(x) is exactly the principal divisor of the rational function x, so the isomorphism carries the
principal fractional ideals to the principal divisors. This is the compatibility on principal
elements needed before passing to quotient-level statements, which are not proved in this file.
The divisor of a prime v is the point divisor [v], the sanity check that rules out a
vacuous map.
This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve",
specifically the "(smooth curve) Weil ≃ Cartier" dictionary realized here for the affine
Dedekind model. It reuses
Mathlib's FractionalIdeal.count factorization API (count_mul, count_finsuppProd,
finprod_heightOneSpectrum_factorization', count_maximal_coprime) and Tau Ceti's WeilDivisor
and OrderSystem.ofDedekindDomain API; no external mathematics is vendored.
The Weil divisor of an invertible fractional ideal: the formal sum Σ_v count K v I · [v]
of the v-adic multiplicities of I over the height-one primes v of R, as a homomorphism from
the group of invertible fractional ideals to the free Weil-divisor group. The multiplicity is zero
for all but finitely many v (FractionalIdeal.finite_factors), and the multiplicativity of
FractionalIdeal.count makes this additive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coefficient of fractionalIdealDivisor R K I at a height-one prime v is the
v-adic multiplicity FractionalIdeal.count K v I of the invertible fractional ideal I.
The divisor map is injective: an invertible fractional ideal is recovered from its
multiplicities through the factorization I = ∏_v v^(count K v I).
The product ∏_v v^(D v) of prime fractional ideals v.asIdeal raised to the multiplicities
D v of a Weil divisor D is nonzero, hence an invertible fractional ideal. This is the value of
the inverse of fractionalIdealDivisor.
The divisor map is surjective: a Weil divisor D is the divisor of the invertible fractional
ideal ∏_v v^(D v).
The Weil ≃ Cartier dictionary for the affine Dedekind chart. The group of invertible
fractional ideals of a Dedekind domain R is isomorphic to the free Weil-divisor group on the
height-one primes of R, by taking v-adic multiplicities. The inverse sends a divisor D to the
fractional ideal ∏_v v^(D v).
Equations
Instances For
On forward application the packaged equivalence fractionalIdealDivisorAddEquiv agrees with the
underlying homomorphism fractionalIdealDivisor.
The inverse of fractionalIdealDivisorAddEquiv sends a Weil divisor D to the invertible
fractional ideal ∏_v v^(D v): the product of the prime ideals v.asIdeal raised to the
multiplicities D v. This gives the canonical formula for the inverse, which
AddEquiv.ofBijective otherwise leaves as an unspecified choice inverse.
The divisor of the principal fractional ideal (x) of a nonzero rational function x is the
principal divisor of x: the isomorphism carries principal fractional ideals to principal divisors.
This is the compatibility on principal elements needed to later identify the ideal class group with
the divisor class group Cl(X); that quotient-level isomorphism is not proved here.
Applying the isomorphism fractionalIdealDivisorAddEquiv to the principal fractional ideal
(x) of a nonzero rational function x yields the principal divisor of x, restating
fractionalIdealDivisor_toPrincipalIdeal for the packaged equivalence.
The divisor of a prime v, regarded as an invertible fractional ideal, is the point divisor
[v]. This is the non-vacuity check identifying the divisor map on generators.