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.

References #

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

Tags #

dedekind domain, dedekind ring, adic valuation

Adic valuations on the Dedekind domain R #

source

noncomputable def is_dedekind_domain.height_one_spectrum.int_valuation_def {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (r : R) :

with_zero (multiplicative ℤ)

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

v.int_valuation_def r = ite (r = 0) 0 ↑(⇑multiplicative.of_add (-↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {r})).factors)))

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_def_if_pos {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) {r : R} (hr : r = 0) :

v.int_valuation_def r = 0

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_def_if_neg {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) {r : R} (hr : r ≠ 0) :

v.int_valuation_def r = ↑(⇑multiplicative.of_add (-↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {r})).factors)))

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_ne_zero {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x : R) (hx : x ≠ 0) :

v.int_valuation_def x ≠ 0

Nonzero elements have nonzero adic valuation.

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_ne_zero' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x : ↥(non_zero_divisors R)) :

v.int_valuation_def ↑x ≠ 0

Nonzero divisors have nonzero valuation.

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_zero_le {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x : ↥(non_zero_divisors R)) :

0 < v.int_valuation_def ↑x

Nonzero divisors have valuation greater than zero.

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_le_one {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x : R) :

v.int_valuation_def x ≤ 1

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_lt_one_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (r : R) :

v.int_valuation_def r < 1 ↔ v.as_ideal ∣ ideal.span {r}

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_le_pow_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (r : R) (n : ℕ) :

v.int_valuation_def r ≤ ↑(⇑multiplicative.of_add (-↑n)) ↔ v.as_ideal ^ n ∣ ideal.span {r}

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_zero' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

v.int_valuation_def 0 = 0

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_one' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

v.int_valuation_def 1 = 1

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_mul' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x y : R) :

v.int_valuation_def (x * y) = v.int_valuation_def x * v.int_valuation_def y

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

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation.le_max_iff_min_le {a b c : ℕ} :

⇑multiplicative.of_add (-↑c) ≤ linear_order.max (⇑multiplicative.of_add (-↑a)) (⇑multiplicative.of_add (-↑b)) ↔ linear_order.min a b ≤ c

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_add_le_max' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) (x y : R) :

v.int_valuation_def (x + y) ≤ linear_order.max (v.int_valuation_def x) (v.int_valuation_def y)

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

source

noncomputable def is_dedekind_domain.height_one_spectrum.int_valuation {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

valuation R (with_zero (multiplicative ℤ))

The v-adic valuation on R.

Equations

v.int_valuation = {to_monoid_with_zero_hom := {to_fun := v.int_valuation_def, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

source

theorem is_dedekind_domain.height_one_spectrum.int_valuation_exists_uniformizer {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

∃ (π : R), v.int_valuation_def π = ↑(⇑multiplicative.of_add (-1))

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

Adic valuations on the field of fractions `K` #

source

noncomputable def is_dedekind_domain.height_one_spectrum.valuation {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] (v : is_dedekind_domain.height_one_spectrum R) :

valuation K (with_zero (multiplicative ℤ))

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

v.valuation = v.int_valuation.extend_to_localization _ K

source

theorem is_dedekind_domain.height_one_spectrum.valuation_def {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] (v : is_dedekind_domain.height_one_spectrum R) (x : K) :

⇑(v.valuation) x = ⇑(v.int_valuation.extend_to_localization _ K) x

source

theorem is_dedekind_domain.height_one_spectrum.valuation_of_mk' {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] (v : is_dedekind_domain.height_one_spectrum R) {r : R} {s : ↥(non_zero_divisors R)} :

⇑(v.valuation) (is_localization.mk' K r s) = ⇑(v.int_valuation) r / ⇑(v.int_valuation) ↑s

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

source

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

⇑(v.valuation) (⇑(algebra_map R K) r) = ⇑(v.int_valuation) r

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

source

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

⇑(v.valuation) (⇑(algebra_map R K) r) ≤ 1

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

source

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

⇑(v.valuation) (⇑(algebra_map R K) r) < 1 ↔ v.as_ideal ∣ ideal.span {r}

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

source

theorem is_dedekind_domain.height_one_spectrum.valuation_exists_uniformizer {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] (v : is_dedekind_domain.height_one_spectrum R) :

∃ (π : K), ⇑(v.valuation) π = ↑(⇑multiplicative.of_add (-1))

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

source

theorem is_dedekind_domain.height_one_spectrum.valuation_uniformizer_ne_zero {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] (v : is_dedekind_domain.height_one_spectrum R) :

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

source