# Adic valuations on Dedekind domains #

Given a Dedekind domain R of Krull dimension 1 and a maximal ideal v of R, we define the v-adic valuation on R and its extension to the field of fractions K of R. We prove several properties of this valuation, including the existence of uniformizers.

We define the completion of K with respect to the v-adic valuation, denoted v.adicCompletion, and its ring of integers, denoted v.adicCompletionIntegers.

## Main definitions #

• IsDedekindDomain.HeightOneSpectrum.intValuation v is the v-adic valuation on R.
• IsDedekindDomain.HeightOneSpectrum.valuation v is the v-adic valuation on K.
• IsDedekindDomain.HeightOneSpectrum.adicCompletion v is the completion of K with respect to its v-adic valuation.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers v is the ring of integers of v.adicCompletion.

## Main results #

• IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one : The v-adic valuation on R is bounded above by 1.
• IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd : The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).
• IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd : The v-adic valuation of r ∈ R is less than or equal to Multiplicative.ofAdd (-n) if and only if vⁿ divides the ideal (r).
• IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer : There exists π ∈ R with v-adic valuation Multiplicative.ofAdd (-1).
• is_dedekind_domain.height_one_spectrum.valuation_of_mk' : The v-adic valuation of r/s ∈ K is the valuation of r divided by the valuation of s.
• IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap : The v-adic valuation on K extends the v-adic valuation on R.
• IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer : There exists π ∈ K with v-adic valuation Multiplicative.ofAdd (-1).

## Implementation notes #

We are only interested in Dedekind domains with Krull dimension 1.

• [G. J. Janusz, Algebraic Number Fields][janusz1996]
• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

dedekind domain, dedekind ring, adic valuation