Places attached to the height-one primes of a Dedekind model #
Let k be a field and R a Dedekind domain which is a k-algebra, with fraction field F.
Every height-one prime p of R gives a place of F / k: the normalized p-adic valuation
is surjective onto ℤᵐ⁰ by IsDedekindDomain.HeightOneSpectrum.valuation_surjective, and it is
trivial on k because the nonzero constants are units of R. Distinct primes give distinct
places, and the residue field of the place is the residue field R ⧸ p of the prime, so the
degree of the place is [R ⧸ p : k].
This is the affine half of the place vocabulary: applied to R = k[X] and F = k(x) it produces
the finite places of the rational function field (Stichtenoth, Algebraic Function Fields and
Codes, second edition, Proposition 1.2.1(a)), and applied to the integral closure of k[x] in a
function field it produces the places of a chosen affine model.
Main definitions #
TauCeti.Place.adic: the place ofF / kattached top : IsDedekindDomain.HeightOneSpectrum R.TauCeti.Place.integersAdicEquiv: the valuation ring of that place is the localization ofRatp.TauCeti.Place.adicResidueHom: reductionR → F_Pat that place.
Main results #
TauCeti.Place.adic_injective: distinct height-one primes give distinct places.TauCeti.Place.adicResidueFieldEquiv: the residue field ofPlace.adic k F pisR ⧸ p, as ak-algebra;TauCeti.Place.adicResidueFieldEquiv_mkcomputes this equivalence on quotient representatives, andTauCeti.Place.degree_adicreads off the degree of the place. The valuation ring of the place is the localization ofRatp, so this is Mathlib'sIsLocalization.AtPrime.equivQuotMaximalIdeal.TauCeti.Place.ord_algebraMap_adic: the order ofr : Rat the place is the multiplicity ofpin(r);TauCeti.Place.isUniformizer_algebraMap_adicspecializes this to a generator ofp, which is therefore a prime element for the place.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.1 and III.2.
- The adic valuation of a height-one prime, its valuation subring and the identification of that
subring with the localization at the prime are
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean(María Inés de Frutos-Fernández); the residue field of a localization at a prime isMathlib/RingTheory/Localization/AtPrime/Basic.lean.
The adic valuation of a height-one prime of a Dedekind k-algebra is trivial on k: a
nonzero constant is a unit of R, hence lies outside every prime ideal.
The place of F / k attached to a height-one prime p of a Dedekind k-algebra R with
fraction field F: the normalized p-adic valuation.
Equations
- TauCeti.Place.adic k F p = { valuation := IsDedekindDomain.HeightOneSpectrum.valuation F p, valuation_surjective := ⋯, isTrivialOn := ⋯ }
Instances For
Distinct height-one primes give distinct places: the place remembers its prime.
Orders of elements of R #
An element of R has positive order at adic k F p exactly when it lies in p.
The order of an element of R at the place adic k F p is the multiplicity of p in the
principal ideal it generates.
A generator of p is a prime element for the place adic k F p, i.e. a uniformizer for its
normalized valuation.
The residue field #
R maps into the valuation ring of adic k F p, every element of R being integral there.
Equations
- TauCeti.Place.instAlgebraSubtypeMemValuationSubringIntegersAdic k F p = ((algebraMap R F).codRestrict (TauCeti.Place.adic k F p).integers ⋯).toAlgebra
The valuation ring of an adic place is the localization at its prime, by
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring.
Equations
Instances For
The equivalence from the localization at p to the integers of the adic place preserves
the underlying element of F.
Reduction at the place adic k F p, as a ring homomorphism from R to its residue field.
Equations
- TauCeti.Place.adicResidueHom k F p = (IsLocalRing.residue ↥(TauCeti.Place.adic k F p).integers).comp (algebraMap R ↥(TauCeti.Place.adic k F p).integers)
Instances For
Reduction at an adic place is the residue of the image in its valuation ring.
The residue field of an adic place is the residue field of its prime: reduction at
adic k F p identifies R ⧸ p with F_P, as k-algebras. Since the valuation ring of the place
is the localization of R at p, this is Mathlib's
IsLocalization.AtPrime.equivQuotMaximalIdeal, upgraded to a k-algebra equivalence.
Equations
Instances For
The degree of an adic place is the degree of the residue field of its prime.