Affine models: the place of a height one prime, and the two-way correspondence #
An affine model of F / k is a Dedekind k-subalgebra R of F whose fraction field is F.
TauCeti/FieldTheory/FunctionField/AffineModel/Place.lean sends a place of F / k that is finite
on R to a height one prime of R, its centre. This file supplies the other direction: the
normalized 𝔭-adic valuation of F attached to a height one prime 𝔭 of R is trivial on the
constants — every nonzero constant is a unit of R, hence lies outside 𝔭 — so it is a place
of F / k. The two constructions are mutually inverse, which packages the correspondence as a
bijection
{P : Place k F | R ⊆ 𝒪_P} ≃ HeightOneSpectrum R.
The correspondence is then made quantitative. On R the order function of the place of 𝔭 is
the multiplicity of 𝔭 in a principal ideal, so divisor coefficients on the finite chart are read
off from Mathlib's factorization calculus; and the residue field of the place of 𝔭 is R ⧸ 𝔭,
so the degree of the place is the residue degree [R ⧸ 𝔭 : k] of the prime. Together these say
that divisor theory on the finite chart of a model is exactly the ideal theory of the model.
Holomorphy rings supply the examples: once 𝒪_S is a Dedekind domain with fraction field F —
which TauCeti.isPrincipalIdealRing_holomorphyRing and TauCeti.isFractionRing_holomorphyRing
give for a finite S omitting some place — its finite chart is S itself, so the correspondence
above becomes the bijection S ≃ HeightOneSpectrum 𝒪_S.
Main definitions #
TauCeti.Place.ofPrime: the place ofF / kattached to a height one prime of an affine model.TauCeti.Place.residueHom: evaluation of the elements of the model at a place finite on it, ak-algebra mapR → F_Pwhose kernel is the centre of the place (TauCeti.Place.ker_residueHom).TauCeti.Place.heightOneSpectrumEquiv: the bijection between the places finite on a model and the height one primes of the model.TauCeti.holomorphyRingHeightOneSpectrumEquiv: that bijection for the model𝒪_S, whose finite chart isS, as the identification ofSwith the height one primes of𝒪_S.
Main results #
TauCeti.Place.center_ofPrimeandTauCeti.Place.ofPrime_center: the two constructions are mutually inverse, andTauCeti.Place.exists_eq_ofPrime_iffidentifies the places in the image as exactly the places finite on the model, withTauCeti.Place.range_ofPrimeandTauCeti.Place.compl_range_ofPrimethe same statement for the finite chart and its complement as sets of places.TauCeti.Place.ord_ofPrime_algebraMap: the coefficient formulaord_P r = mult_𝔭 (r), forr ≠ 0, the𝔭-form ofTauCeti.Place.ord_algebraMap_eq_multiplicity_center.TauCeti.Place.quotientAlgEquivResidueField: the residue field of a place finite on the model isRmodulo the centre of the place, whenceTauCeti.Place.degree_eq_finrank_quotient_center;TauCeti.Place.quotientAlgEquivResidueFieldOfPrimeandTauCeti.Place.degree_ofPrimeare the𝔭-forms,F_P = R ⧸ 𝔭anddeg P = [R ⧸ 𝔭 : k].
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.1 and III.2.
The place of F / k attached to a height one prime 𝔭 of an affine model R: its
valuation is Mathlib's normalized 𝔭-adic valuation of F. Triviality on the constants is the
only thing to check, and it holds because a nonzero constant is a unit of R and therefore
avoids 𝔭.
Equations
- TauCeti.Place.ofPrime k F 𝔭 = { valuation := IsDedekindDomain.HeightOneSpectrum.valuation F 𝔭, valuation_surjective := ⋯, isTrivialOn := ⋯ }
Instances For
An affine model is contained in the valuation ring of the place of each of its height one
primes: the place of 𝔭 is finite on R.
The valuation of the place of 𝔭 extends the 𝔭-adic valuation of the model.
The elements of the model with a zero at the place of 𝔭 are exactly the elements of 𝔭.
The centre on R of the place of a height one prime 𝔭 of R is 𝔭 itself.
The place of the centre on R of a place finite on R is that place.
The places of F / k finite on an affine model R are exactly the height one primes of
R (Stichtenoth, Section III.2): the centre of a place and the adic place of a prime are
mutually inverse bijections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Distinct height one primes of a model give distinct places.
A place of F / k is the place of a height one prime of an affine model R exactly when
it is finite on R: the image of TauCeti.Place.ofPrime is the finite chart of the model.
The finite chart of an affine model, as a set of places: the image of
TauCeti.Place.ofPrime consists of the places finite on R.
The places infinite on an affine model are the complement of its finite chart: a place
lies outside the image of TauCeti.Place.ofPrime exactly when some element of the model has a
pole there.
The coefficient formula on the finite chart: the order at the place of 𝔭 of a nonzero
element of the model is the multiplicity of 𝔭 in the ideal it generates. This is
TauCeti.Place.ord_algebraMap_eq_multiplicity_center at the place of 𝔭, whose centre is 𝔭,
and it is what turns a divisor supported on the finite chart into a factorization of ideals.
Evaluation of the elements of an affine model at a place finite on it, as a map of
k-algebras R → F_P. It is surjective with kernel the centre of the place, which is the
content of TauCeti.Place.quotientAlgEquivResidueField.
Equations
- P.residueHom hR = { toRingHom := (IsLocalRing.residue ↥P.integers).comp ((algebraMap R F).codRestrict P.integers hR), commutes' := ⋯ }
Instances For
The kernel of evaluation at P is the centre of P on the model: this is the
evaluation-map form of TauCeti.Place.mem_center_asIdeal, which says the same thing about the
valuation of P.
Every residue at a place finite on an affine model is the residue of an element of the
model. This is Mathlib's approximation theorem for the adic valuation of the centre, at the
accuracy 1: a function integral at the place is within 1 of an element of the model, so the
two have the same residue.
The residue field of a place finite on an affine model is the model modulo the centre of
the place, as k-algebras.
Equations
Instances For
The degree of a place finite on an affine model is the residue degree of its centre: the weight a divisor attaches to a place of the finite chart is the one Mathlib's ideal theory attaches to the corresponding prime.
The residue field of the place of a height one prime 𝔭 of an affine model is R ⧸ 𝔭,
as k-algebras: this is TauCeti.Place.quotientAlgEquivResidueField at the place of 𝔭, whose
centre is 𝔭.
Equations
Instances For
The degree of the place of 𝔭 is the residue degree of 𝔭: the weight a divisor
attaches to a place of the finite chart is the one Mathlib's ideal theory attaches to the
corresponding prime.
Holomorphy rings as affine models #
The height one primes of the affine model 𝒪_S are the places of S. Once 𝒪_S is a
Dedekind domain with fraction field F — which TauCeti.isPrincipalIdealRing_holomorphyRing and
TauCeti.isFractionRing_holomorphyRing supply for a finite S avoiding at least one place — the
finite chart of the model 𝒪_S is exactly S by
TauCeti.forall_algebraMap_mem_integers_holomorphyRing_iff, so this is
TauCeti.Place.heightOneSpectrumEquiv for 𝒪_S, read along that identification of subtypes.