# 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.

## References #

• [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

### Adic valuations on the Dedekind domain R #

The additive v-adic valuation of r ∈ R is the exponent of v in the factorization of the ideal (r), if r is nonzero, or infinity, if r = 0. intValuationDef is the corresponding multiplicative valuation.

Instances For
theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos {R : Type u_1} [] [] [] {r : R} (hr : r = 0) :
theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg {R : Type u_1} [] [] [] {r : R} (hr : r 0) :
= ↑(Multiplicative.ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) ())))
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero {R : Type u_1} [] [] [] (x : R) (hx : x 0) :

Nonzero elements have nonzero adic valuation.

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero' {R : Type u_1} [] [] [] (x : { x // }) :

Nonzero divisors have nonzero valuation.

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le {R : Type u_1} [] [] [] (x : { x // }) :

Nonzero divisors have valuation greater than zero.

The v-adic valuation on R is bounded above by 1.

The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd {R : Type u_1} [] [] [] (r : R) (n : ) :
↑(Multiplicative.ofAdd (-n)) v.asIdeal ^ n Ideal.span {r}

The v-adic valuation of r ∈ R is less than Multiplicative.ofAdd (-n) if and only if vⁿ divides the ideal (r).

The v-adic valuation of 0 : R equals 0.

The v-adic valuation of 1 : R equals 1.

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul' {R : Type u_1} [] [] [] (x : R) (y : R) :

The v-adic valuation of a product equals the product of the valuations.

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.le_max_iff_min_le {a : } {b : } {c : } :
theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max' {R : Type u_1} [] [] [] (x : R) (y : R) :

The v-adic valuation of a sum is bounded above by the maximum of the valuations.

The v-adic valuation on R.

Instances For
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer {R : Type u_1} [] [] [] :

There exists π ∈ R with v-adic valuation Multiplicative.ofAdd (-1).

### Adic valuations on the field of fractions K#

def IsDedekindDomain.HeightOneSpectrum.valuation {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] :

The v-adic valuation of x ∈ K is the valuation of r divided by the valuation of s, where r and s are chosen so that x = r/s.

Instances For
theorem IsDedekindDomain.HeightOneSpectrum.valuation_def {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] (x : K) :
= ↑(Valuation.extendToLocalization () (_ : ∀ (r : R), ) K) x
theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk' {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] {r : R} {s : { x // }} :

The v-adic valuation of r/s ∈ K is the valuation of r divided by the valuation of s.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] (r : R) :

The v-adic valuation on K extends the v-adic valuation on R.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] (r : R) :
↑() (↑() r) 1

The v-adic valuation on R is bounded above by 1.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] (r : R) :
↑() (↑() r) < 1 v.asIdeal Ideal.span {r}

The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).

theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :

There exists π ∈ K with v-adic valuation Multiplicative.ofAdd (-1).

theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
Classical.choose (_ : π, = ↑(Multiplicative.ofAdd (-1))) 0

Uniformizers are nonzero.

### Completions with respect to adic valuations #

Given a Dedekind domain R with field of fractions K and a maximal ideal v of R, we define the completion of K with respect to its v-adic valuation, denoted v.adicCompletion, and its ring of integers, denoted v.adicCompletionIntegers.

def IsDedekindDomain.HeightOneSpectrum.adicValued {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] :

K as a valued field with the v-adic valuation.

Instances For
theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply {R : Type u_1} [] [] [] {K : Type u_2} [] [Algebra R K] [] {x : K} :
Valued.v x =
def IsDedekindDomain.HeightOneSpectrum.adicCompletion {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
Type u_2

The completion of K with respect to its v-adic valuation.

Instances For
instance IsDedekindDomain.HeightOneSpectrum.instFieldAdicCompletion {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
instance IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
Valued.v x =
instance IsDedekindDomain.HeightOneSpectrum.AdicCompletion.instCoe {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :
def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers {R : Type u_1} [] [] [] (K : Type u_2) [] [Algebra R K] [] :

The ring of integers of adicCompletion.

Instances For
theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] :
Valued.v x 1
instance IsDedekindDomain.HeightOneSpectrum.AdicCompletion.algebra' (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] :
@[simp]
theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] (r : R) (x : K) :
K (r x) = r K x
theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion' (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] :
= K ↑()
theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] :
@[simp]
theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers (R : Type u_1) [] [] [] (K : Type u_2) [] [Algebra R K] [] (r : R) (x : ) :
↑(r x) = r x