Affine models: a place finite on a Dedekind subring is one of its height one primes #
An affine model of F / k is a Dedekind k-subalgebra R of F whose fraction field is F;
the standard example is the integral closure R_x of k[x] in F for a transcendental x. This
file proves the forward direction of the places ↔ height one primes correspondence: a place of
F / k whose valuation ring contains R is the adic place of a unique height one prime 𝔭 of
R, in the strong sense that the valuation of the place equals — not merely is equivalent to —
the normalized 𝔭-adic valuation. The prime in question is the centre {r : R | ord_P r > 0} of
the place on R, so the valuation ring of the place is the localization of R there. The converse
— that every height one prime of R arises this way, which upgrades this injection into a
bijection — is not proved here; it is proved in
TauCeti/FieldTheory/FunctionField/AffineModel/Prime.lean, using the place of a prime from
TauCeti/FieldTheory/FunctionField/Place/Adic.lean.
This is the "places → height one primes" half of the affine-model dictionary that reduces divisor
theory on the finite chart of a model to Mathlib's factorization calculus for fractional ideals.
Which places are finite on R_x is settled by the two order-of-x criteria below: k[x] lies in
the valuation ring of P exactly when x has no pole at P, and the valuation ring, being
integrally closed, then swallows everything integral over k[x].
Main results #
TauCeti.Place.adjoin_le_integers_iff:k[x] ⊆ 𝒪_Pexactly whenx ∈ 𝒪_P.TauCeti.Place.center: the height one prime of an affine model below a place finite on it, withTauCeti.Place.valuation_centeridentifying the adic valuation of that prime with the valuation of the place,TauCeti.Place.center_injectiveshowing that a place finite on a model is determined by its centre, andTauCeti.Place.comap_center_asIdealshowing that the centre on a larger model contracts to the centre on a smaller one.TauCeti.Place.existsUnique_valuation_eq: the uniqueness statement, andTauCeti.Place.valuationSubringAtPrime_eq_integers: the valuation ring of the place is the localization of the model at the centre.TauCeti.Place.ord_algebraMap_eq_multiplicity_center: the coefficient formulaord_P r = mult_(centre) (r), which reads an order at the place off the factorization of an ideal of the model.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.1 and III.2.
k[x] lies in the valuation ring of P exactly when x has no pole at P: the
criterion selecting the places on the finite chart of x. Its additive form is obtained from
TauCeti.Place.mem_integers_iff_ord_nonneg.
Every element of F integral over k[x] lies in the valuation ring of P, as soon as x
has no pole at P. This is what makes the integral closure of k[x] in F — the affine model
attached to x — an object of the finite chart of P.
The centre on R of a place P finite on R: the nonzero prime ideal consisting of
the elements with a zero at P, bundled as a HeightOneSpectrum R. For a Dedekind affine model,
this is a height one prime.
Equations
- P.center hR = Valuation.heightOneSpectrum R P.valuation ⋯
Instances For
The centre of P on R consists of the elements of R at which the valuation of P is
< 1.
The additive form of TauCeti.Place.mem_center_asIdeal: the centre of P on R consists of
the elements of R with a zero at P. The hypothesis r ≠ 0 guards the junk value
ord_P 0 = 0.
The centre is compatible with enlarging the model: if the model R sits inside a second
model B with the same fraction field F, the centre of P on B contracts to the centre of
P on R.
The valuation of a place finite on an affine model is the adic valuation of its centre. This is the exact, not merely up-to-equivalence, form of the correspondence between places and height one primes.
The coefficient formula at a place finite on an affine model: the order at P of a
nonzero element of the model is the multiplicity of the centre of P in the ideal it generates.
This is what turns a divisor supported on the finite chart of a model into a factorization of
ideals. The hypothesis r ≠ 0 guards the junk values ord_P 0 = 0 and mult_𝔭 ⊥ = 1.
A height one prime whose adic valuation is that of P is the centre of P.
A place of F / k whose valuation ring contains an affine model R is the adic place of a
unique height one prime of R (Stichtenoth, Section III.2).
The valuation ring of a place finite on an affine model is the localization of the model at the centre of the place.
Distinct places finite on an affine model have distinct centres: a place is recovered from its centre.
A place at which x has no pole is the adic place of a unique height one prime of any affine
model integral over k[x]: the finite chart of x is covered by the height one primes of the
model.