# 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`.
- `IsDedekindDomain.HeightOneSpectrum.adicAbv v`is the `v`-adic absolute value on `K` defined as `b` raised to negative `v`-adic valuation, for some `b` in `ℝ≥0`.

## 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 `WithZero.exp (-n)` if and only if `vⁿ` divides the ideal `(r)`.
- `IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer` : There exists `π ∈ R` with `v`-adic valuation `WithZero.exp (-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 `WithZero.exp (-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öhlich, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]

## Tags #

dedekind domain, dedekind ring, adic valuation

### Adic valuations on the Dedekind domain R #

source
def IsDedekindDomain.HeightOneSpectrum.intValuationDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : 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 WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))

Instances For

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {r : R} (hr : r = 0) :
v.intValuationDef r = 0
source
@[simp]
theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) :
v.intValuationDef 0 = 0
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {r : R} (hr : r ≠ 0) :
v.intValuationDef r = WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) :
v.intValuationDef 0 = 0

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

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

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

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : 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.

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le {a b c : ℕ} :
Multiplicative.ofAdd (-↑c) ≤ max (Multiplicative.ofAdd (-↑a)) (Multiplicative.ofAdd (-↑b)) ↔ min a b ≤ c
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (x y : R) :
v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

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

source
def IsDedekindDomain.HeightOneSpectrum.intValuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : 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' := ⋯ }

Instances For

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {r : R} (v : HeightOneSpectrum R) :
v.intValuation r = v.intValuationDef r
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_def {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {r : R} :
v.intValuation r = if r = 0 then 0 else WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
source
@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_apply (since := "2025-04-26")]
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (r : R) :
v.intValuation r = v.intValuationDef r
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {r : R} (hr : r ≠ 0) :
v.intValuation r = WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (x : R) (hx : x ≠ 0) :
v.intValuation x ≠ 0

Nonzero elements have nonzero adic valuation.

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

Nonzero divisors have nonzero valuation.

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

Nonzero divisors have valuation greater than zero.

source
@[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt (since := "2025-05-11")]
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (x : ↥(nonZeroDivisors R)) :
0 < v.intValuation ↑x

Alias of `IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt`.

Nonzero divisors have valuation greater than zero.

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

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

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

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (r : R) :
v.intValuation r < 1 ↔ r ∈ v.asIdeal

The `v`-adic valuation of `r ∈ R` is less than 1 if and only if `r ∈ v`.

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (r : R) (n : ℕ) :
v.intValuation r ≤ WithZero.exp (-↑n) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

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

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (r : R) (n : ℕ) :
v.intValuation r ≤ WithZero.exp (-↑n) ↔ r ∈ v.asIdeal ^ n

The `v`-adic valuation of `r ∈ R` is less than `WithZero.exp (-n)` if and only if `r ∈ vⁿ`.

source
theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) :
∃ (π : R), v.intValuation π = WithZero.exp (-1)

There exists `π ∈ R` with `v`-adic valuation `WithZero.exp (-1)`.

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

The `I`-adic valuation of a generator of `I` equals `(-1 : ℤᵐ⁰)`

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

source
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 : 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

- IsDedekindDomain.HeightOneSpectrum.valuation K v = v.intValuation.extendToLocalization ⋯ K

Instances For

source
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 : HeightOneSpectrum R) (x : K) :
(valuation K v) x = (v.intValuation.extendToLocalization ⋯ K) x
source
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 : HeightOneSpectrum R) {r : R} {s : ↥(nonZeroDivisors R)} :
(valuation K v) (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`.

source
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 : HeightOneSpectrum R) (r : R) :
(valuation K v) ↑r = v.intValuation r

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

source
@[deprecated IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap (since := "2025-05-11")]
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 : HeightOneSpectrum R) (r : R) :
(valuation K v) ↑r = v.intValuationDef r
source
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 : HeightOneSpectrum R) (r : R) :
(valuation K v) ↑r ≤ 1

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

source
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 : HeightOneSpectrum R) (r : R) :
(valuation K v) ↑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)`.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (r : R) :
(valuation K v) ↑r < 1 ↔ r ∈ v.asIdeal

The `v`-adic valuation of `r ∈ R` is less than 1 if and only if `r ∈ v`.

source
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 : HeightOneSpectrum R) :
∃ (π : K), (valuation K v) π = WithZero.exp (-1)

There exists `π ∈ K` with `v`-adic valuation `WithZero.exp (-1)`.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuation_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
Function.Surjective ⇑(valuation K v)
source
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 : HeightOneSpectrum R) :
Classical.choose ⋯ ≠ 0

Uniformizers are nonzero.

source
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 : HeightOneSpectrum R), (valuation K v) x ≤ 1) :
x ∈ (algebraMap R K).range
source
theorem IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {p q : HeightOneSpectrum R} (hpq : (valuation K p).IsEquiv (valuation K q)) :
p = q

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

source
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 : HeightOneSpectrum R) :
Valued K (WithZero (Multiplicative ℤ))

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

Equations

- v.adicValued = Valued.mk' (IsDedekindDomain.HeightOneSpectrum.valuation K v)

Instances For

source
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 : HeightOneSpectrum R) {x : K} :
Valued.v x = (valuation K v) x
source
@[simp]
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 : HeightOneSpectrum R) (x : WithVal (valuation K v)) :
Valued.v x = (valuation K v) x
source
@[reducible, inline]
abbrev IsDedekindDomain.HeightOneSpectrum.adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
Type u_2

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

Equations

- IsDedekindDomain.HeightOneSpectrum.adicCompletion K v = (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion

Instances For

source
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 : HeightOneSpectrum R) {x : adicCompletion K v} :
Valued.v x = Valued.extension x
source
theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
Function.Surjective ⇑Valued.v
source
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 : HeightOneSpectrum R) :
ValuationSubring (adicCompletion K v)

The ring of integers of `adicCompletion`.

Equations

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

Instances For

source
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 : HeightOneSpectrum R) :
Inhabited ↥(adicCompletionIntegers K v)
Equations

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

source
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 : HeightOneSpectrum R) {x : adicCompletion K v} :
x ∈ adicCompletionIntegers K v ↔ Valued.v x ≤ 1
source
theorem IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : adicCompletion K v} :
x ∉ adicCompletionIntegers K v ↔ 1 < Valued.v x
source
@[deprecated IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers (since := "2025-05-23")]
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 : HeightOneSpectrum R) {x : adicCompletion K v} :
x ∉ adicCompletionIntegers K v ↔ 1 < Valued.v x

Alias of `IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers`.

source
@[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 : HeightOneSpectrum R) :
UniformContinuousConstSMul R (WithVal (valuation K v))
source
instance IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] :
UniformContinuousConstSMul S (WithVal (valuation K v))
source
instance IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] :
Algebra S (adicCompletion K v)
Equations

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

source
theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] (r : S) (x : WithVal (valuation K v)) :
↑(r • x) = r • ↑x
source
theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [Field K] [CommSemiring S] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Algebra S K] :
⇑(algebraMap S (adicCompletion K v)) = UniformSpace.Completion.coe' ∘ ⇑(algebraMap S K)
source
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 : HeightOneSpectrum R) (r : R) :
↑((algebraMap R K) r) ∈ adicCompletionIntegers K v
source
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 : HeightOneSpectrum R) :
Algebra R ↥(adicCompletionIntegers K v)
Equations

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

source
@[simp]
theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (r : R) :
↑((algebraMap R ↥(adicCompletionIntegers K v)) r) = ↑((algebraMap R K) r)
source
instance IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [FaithfulSMul R K] :
FaithfulSMul R ↥(adicCompletionIntegers K v)
source
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 : HeightOneSpectrum R) (r : R) :
Valued.v ↑r = (valuation K v) ↑r

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

source
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 : HeightOneSpectrum R) (k : K) :
Valued.v ↑k = (valuation K v) k

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

source
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 : HeightOneSpectrum R) (r : R) :
↑r ∈ adicCompletionIntegers K v

A global integer is in the local integers.

source
@[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 : HeightOneSpectrum R) (r : R) (x : ↥(adicCompletionIntegers K v)) :
↑(r • x) = r • ↑x
source
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 : HeightOneSpectrum R) :
NoZeroSMulDivisors R ↥(adicCompletionIntegers K v)
source
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 : HeightOneSpectrum R) :
IsScalarTower R (↥(adicCompletionIntegers K v)) (adicCompletion K v)
source
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 : HeightOneSpectrum R) (a : adicCompletion K v) :
∃ b ∈ nonZeroDivisors R, a * ↑b ∈ adicCompletionIntegers K v
source
def IsDedekindDomain.HeightOneSpectrum.adicAbvDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (x : K) :
NNReal

The `v`-adic absolute value function on `K` defined as `b` raised to negative `v`-adic valuation, for some `b` in `ℝ≥0`

Equations

- v.adicAbvDef hb x = (WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x)

Instances For

source
theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) :
IsNonarchimedean fun (x : K) => v.adicAbvDef hb x
source
def IsDedekindDomain.HeightOneSpectrum.adicAbv {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) :
AbsoluteValue K ℝ

The `v`-adic absolute value on `K` defined as `b` raised to negative `v`-adic valuation, for some `b` in `ℝ≥0`

Equations

- v.adicAbv hb = { toFun := fun (x : K) => ↑(v.adicAbvDef hb x), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

Instances For

source
theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) :
IsNonarchimedean ⇑(v.adicAbv hb)

The `v`-adic absolute value is nonarchimedean

source
theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) :
(v.adicAbv hb) ((algebraMap R K) r) ≤ 1
source
theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) :
(v.adicAbv hb) ((algebraMap R K) r) < 1 ↔ r ∈ v.asIdeal
source
theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) :
(v.adicAbv hb) ((algebraMap R K) r) = 1 ↔ r ∉ v.asIdeal