# Adic valuations on Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.adic_completion,and its ring of integers, denoted v.adic_completion_integers.

## Main definitions #

• is_dedekind_domain.height_one_spectrum.int_valuation v is the v-adic valuation on R.
• is_dedekind_domain.height_one_spectrum.valuation v is the v-adic valuation on K.
• is_dedekind_domain.height_one_spectrum.adic_completion v is the completion of K with respect to its v-adic valuation.
• is_dedekind_domain.height_one_spectrum.adic_completion_integers v is the ring of integers of v.adic_completion.

## Main results #

• is_dedekind_domain.height_one_spectrum.int_valuation_le_one : The v-adic valuation on R is bounded above by 1.
• is_dedekind_domain.height_one_spectrum.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).
• is_dedekind_domain.height_one_spectrum.int_valuation_le_pow_iff_dvd : The v-adic valuation of r ∈ R is less than or equal to multiplicative.of_add (-n) if and only if vⁿ divides the ideal (r).
• is_dedekind_domain.height_one_spectrum.int_valuation_exists_uniformizer : There exists π ∈ R with v-adic valuation multiplicative.of_add (-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.
• is_dedekind_domain.height_one_spectrum.valuation_of_algebra_map : The v-adic valuation on K extends the v-adic valuation on R.
• is_dedekind_domain.height_one_spectrum.valuation_exists_uniformizer : There exists π ∈ K with v-adic valuation multiplicative.of_add (-1).

## Implementation notes #

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

## Tags #

dedekind domain, dedekind ring, adic valuation

### Adic valuations on the Dedekind domain R #

noncomputable def is_dedekind_domain.height_one_spectrum.int_valuation_def {R : Type u_1} [comm_ring R] [is_domain R] (r : 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. int_valuation_def is the corresponding multiplicative valuation.

Equations

Nonzero elements have nonzero adic valuation.

Nonzero divisors have nonzero valuation.

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

The v-adic valuation of r ∈ R is less than multiplicative.of_add (-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.

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

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

The v-adic valuation on R.

Equations

There exists π ∈ R with v-adic valuation multiplicative.of_add (-1).

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

noncomputable def is_dedekind_domain.height_one_spectrum.valuation {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ 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.

Equations
theorem is_dedekind_domain.height_one_spectrum.valuation_def {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] (x : K) :
theorem is_dedekind_domain.height_one_spectrum.valuation_of_mk' {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {r : R} {s : } :

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

theorem is_dedekind_domain.height_one_spectrum.valuation_of_algebra_map {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] (r : R) :

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

theorem is_dedekind_domain.height_one_spectrum.valuation_le_one {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] (r : R) :
(v.valuation) ( K) r) 1

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

theorem is_dedekind_domain.height_one_spectrum.valuation_lt_one_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] (r : R) :

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

There exists π ∈ K with v-adic valuation multiplicative.of_add (-1).

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.adic_completion, and its ring of integers, denoted v.adic_completion_integers.

noncomputable def is_dedekind_domain.height_one_spectrum.adic_valued {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K]  :

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

Equations
theorem is_dedekind_domain.height_one_spectrum.adic_valued_apply {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {x : K} :
def is_dedekind_domain.height_one_spectrum.adic_completion {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Type u_2

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

Equations
Instances for is_dedekind_domain.height_one_spectrum.adic_completion
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion.field {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion.inhabited {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.valued_adic_completion {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion.has_lift_t {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion_integers {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :

The ring of integers of adic_completion.

Equations
Instances for ↥is_dedekind_domain.height_one_spectrum.adic_completion_integers
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion_integers.inhabited {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion.algebra' (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[simp]
theorem is_dedekind_domain.height_one_spectrum.coe_smul_adic_completion (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] (r : R) (x : K) :
(r x) = r x
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion.algebra (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def is_dedekind_domain.height_one_spectrum.adic_completion_integers.algebra (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K]  :
Equations
@[simp]
theorem is_dedekind_domain.height_one_spectrum.coe_smul_adic_completion_integers (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] (r : R)  :
(r x) = r x
@[protected, instance]
@[protected, instance]