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.intValuation_le_one : The v-adic valuation on R is bounded above by 1.
• IsDedekindDomain.HeightOneSpectrum.intValuation_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.intValuation_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.intValuation_exists_uniformizer : There exists π ∈ R with v-adic valuation Multiplicative.ofAdd (-1).
• IsDedekindDomain.HeightOneSpectrum.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

def IsDedekindDomain.HeightOneSpectrum.intValuationDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : WithZero (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. intValuationDef is the corresponding multiplicative valuation.

Equations

• v.intValuationDef r = if r = 0 then 0 else ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))

theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r = 0) : v.intValuationDef r = 0

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuationDef 0 = 0

theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r ≠ 0) : v.intValuationDef r = ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (hx : x ≠ 0) : v.intValuationDef x ≠ 0

Nonzero elements have nonzero adic valuation.

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (hx : x ≠ 0) : v.intValuationDef x ≠ 0

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero.

---

Nonzero elements have nonzero adic valuation.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(nonZeroDivisors R)) : v.intValuationDef ↑x ≠ 0

Nonzero divisors have nonzero valuation.

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero' (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(nonZeroDivisors R)) : v.intValuationDef ↑x ≠ 0

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'.

---

Nonzero divisors have nonzero valuation.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(nonZeroDivisors R)) : 0 < v.intValuationDef ↑x

Nonzero divisors have valuation greater than zero.

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(nonZeroDivisors R)) : 0 < v.intValuationDef ↑x

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le.

---

Nonzero divisors have valuation greater than zero.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) : v.intValuationDef x ≤ 1

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_le_one (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) : v.intValuationDef x ≤ 1

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_one.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.intValuationDef 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).

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.intValuationDef r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (n : ℕ) : v.intValuationDef r ≤ ↑(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).

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd (since := "2024-07-09")]

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

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuationDef 0 = 0

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero' (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuationDef 0 = 0

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_one' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuationDef 1 = 1

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_one' (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_one' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuationDef 1 = 1

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R) : v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul' (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R) : v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'.

---

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 : ℕ} : Multiplicative.ofAdd (-↑c) ≤ Multiplicative.ofAdd (-↑a) ⊔ Multiplicative.ofAdd (-↑b) ↔ a ⊓ b ≤ c

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.le_max_iff_min_le {a b c : ℕ} : Multiplicative.ofAdd (-↑c) ≤ Multiplicative.ofAdd (-↑a) ⊔ Multiplicative.ofAdd (-↑b) ↔ a ⊓ b ≤ c

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R) : v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max' (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R) : v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'.

---

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

def IsDedekindDomain.HeightOneSpectrum.intValuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : Valuation R (WithZero (Multiplicative ℤ))

The v-adic valuation on R.

Equations

• v.intValuation = { toFun := v.intValuationDef, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.intValuation r = v.intValuationDef r

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {r : R} (v : IsDedekindDomain.HeightOneSpectrum R) : v.intValuation r = v.intValuationDef r

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : ∃ (π : R), v.intValuationDef π = ↑(Multiplicative.ofAdd (-1))

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer (since := "2024-07-09")]

theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) : ∃ (π : R), v.intValuationDef π = ↑(Multiplicative.ofAdd (-1))

Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer.

---

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

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_singleton {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r ≠ 0) (hv : v.asIdeal = Ideal.span {r}) : v.intValuation r = ↑(Multiplicative.ofAdd (-1))

The I-adic valuation of a generator of I equals (-1 : ℤₘ₀)

Adic valuations on the field of fractions K

def IsDedekindDomain.HeightOneSpectrum.valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Valuation K (WithZero (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.intValuation.extendToLocalization ⋯ K

theorem IsDedekindDomain.HeightOneSpectrum.valuation_def {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K) : v.valuation x = (v.intValuation.extendToLocalization ⋯ K) x

theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} {s : ↥(nonZeroDivisors R)} : v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s

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} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.valuation ((algebraMap R K) r) = v.intValuation r

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

theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.valuation ↑r = v.intValuationDef r

theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.valuation ((algebraMap R K) 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} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : v.valuation ((algebraMap R K) 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} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : ∃ (π : K), v.valuation π = ↑(Multiplicative.ofAdd (-1))

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

theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Classical.choose ⋯ ≠ 0

Uniformizers are nonzero.

theorem IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (x : K) (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.valuation x ≤ 1) : x ∈ (algebraMap R K).range

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} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Valued K (WithZero (Multiplicative ℤ))

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

Equations

• v.adicValued = Valued.mk' v.valuation

theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : K} : Valued.v x = v.valuation x

def IsDedekindDomain.HeightOneSpectrum.adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Type u_2

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

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion K v = UniformSpace.Completion K

instance IsDedekindDomain.HeightOneSpectrum.instFieldAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Field (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.instFieldAdicCompletion K v = inferInstanceAs (Field (UniformSpace.Completion K))

instance IsDedekindDomain.HeightOneSpectrum.instInhabitedAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Inhabited (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.instInhabitedAdicCompletion K v = { default := 0 }

instance IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Valued (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (WithZero (Multiplicative ℤ))

Equations

• IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion K v = inferInstanceAs (Valued (UniformSpace.Completion K) (WithZero (Multiplicative ℤ)))

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} : Valued.v x = Valued.extension x

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion_completeSpace {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : CompleteSpace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Coe K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe K v = inferInstanceAs (Coe K (UniformSpace.Completion K))

def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : ValuationSubring (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

The ring of integers of adicCompletion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v = Valued.v.valuationSubring

instance IsDedekindDomain.HeightOneSpectrum.instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Inhabited ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers K v = { default := 0 }

theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ Valued.v x ≤ 1

theorem IsDedekindDomain.HeightOneSpectrum.not_mem_adicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} : x ∉ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ 1 < Valued.v x

@[instance 100]

instance IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : UniformContinuousConstSMul R K

instance IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : UniformContinuousConstSMul K K

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.algebra' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Algebra R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.algebra' R K v = inferInstanceAs (Algebra R (UniformSpace.Completion K))

theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (x : K) : ↑(r • x) = r • ↑x

instance IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Algebra K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Equations

• IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion R K v = UniformSpace.Completion.algebra' K

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : ⇑(algebraMap R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = UniformSpace.Completion.coe' ∘ ⇑(algebraMap R K)

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : ⇑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = UniformSpace.Completion.coe'

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsScalarTower R K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : ↑((algebraMap R K) r) ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

instance IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Algebra R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

Equations

• One or more equations did not get rendered due to their size.

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : Valued.v ↑r = v.valuation ↑r

The valuation on the completion agrees with the global valuation on elements of the integer ring.

theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K) : Valued.v ↑k = v.valuation k

The valuation on the completion agrees with the global valuation on elements of the field.

theorem IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : ↑r ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

A global integer is in the local integers.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) : ↑(r • x) = r • ↑x

instance IsDedekindDomain.HeightOneSpectrum.instNoZeroSMulDivisorsSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : NoZeroSMulDivisors R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

instance IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower' (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsScalarTower R (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : ∃ b ∈ nonZeroDivisors R, a * ↑b ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v