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
• J. Neukirch, Algebraic Number Theory

Tags

dedekind domain, dedekind ring, adic valuation

Adic valuations on the Dedekind domain R

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

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

@[simp]

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

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

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.

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.

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.

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

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.

noncomputable 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' := ⋯ }

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

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

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

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

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.

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.

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.

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.

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

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.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (r : R) : v.intValuation r = 1 ↔ r ∈ v.asIdeal.primeCompl

The v-adic valuation of r : R is equal to 1 if and only if r ∈ vᶜ.

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

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

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

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

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

instance IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntIntValuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : v.intValuation.IsNontrivial

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) (π : v.intValuation.Uniformizer) : v.intValuation ↑π.val = WithZero.exp (-1)

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 : ℤᵐ⁰)

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {v : HeightOneSpectrum R} {x : R} : v.intValuation x = 1 ↔ x ∉ v.asIdeal

Adic valuations on the field of fractions K

noncomputable 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

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

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.

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.

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.

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

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.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem {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) ((algebraMap R K) r) = 1 ↔ r ∉ v.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.valuation_div_le_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) (a : R) {b : R} (hb : b ≠ 0) (h : b ∈ v.asIdeal → a ∉ v.asIdeal) : (valuation K v) (↑a / ↑b) ≤ 1 ↔ b ∉ v.asIdeal

The v adic valuation of a / b : K is ≤ 1 if and only if b ∉ v, provided that a and b are coprime at v.

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

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

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

instance IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation {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 v).IsNontrivial

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)

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.

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

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

theorem IsDedekindDomain.HeightOneSpectrum.instSubtypeMemSubalgebraOfFieldPrimeComplAsIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsDedekindDomain ↥(Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)

theorem IsDedekindDomain.HeightOneSpectrum.instIsLocalRingSubtypeMemSubalgebraOfFieldPrimeComplAsIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsLocalRing ↥(Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)

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

Given a Dedekind domain R in K, its field of fractions, the localization of R at a nonzero prime is a valuation subring of K.

Equations

• IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v = ValuationSubring.ofSubring (Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring ⋯

theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_toSubring {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (valuationSubringAtPrime K v).toSubring = (Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring

theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_le_valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : valuationSubringAtPrime K v ≤ (valuation K v).valuationSubring

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeMemValuationSubringValuationSubringAtPrime {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 ↥(valuationSubringAtPrime K v)

Equations

• v.instAlgebraSubtypeMemValuationSubringValuationSubringAtPrime = (Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯).algebra'

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerSubtypeMemValuationSubringValuationSubringAtPrime {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 (↥(valuationSubringAtPrime K v)) K

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

instance IsDedekindDomain.HeightOneSpectrum.instKrullDimLEOfNatNatSubtypeMemValuationSubringValuationSubringAtPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Ring.KrullDimLE 1 ↥(valuationSubringAtPrime K v)

instance IsDedekindDomain.HeightOneSpectrum.instIsLocalizationPrimeComplAsIdealSubtypeMemValuationSubringValuationSubringAtPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsLocalization v.asIdeal.primeCompl ↥(valuationSubringAtPrime K v)

theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : valuationSubringAtPrime K v = (valuation K v).valuationSubring

Given v : HeightOneSpectrum R, the valuation associated to v has the localization of R at v as valuation subring.

theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq {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) : ∃ (n : R) (d : ↥v.asIdeal.primeCompl), x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

All x : K can be written as n / d or d / n with n : R and d ∈ v.asIdealᶜ.

theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer {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) (hv : (valuation K v) x ≤ 1) : ∃ (n : R) (d : ↥v.asIdeal.primeCompl), x * (algebraMap R K) ↑d = (algebraMap R K) n

All x ∈ 𝓞[K] can be written as n / d with n : R and d ∈ v.asIdealᶜ.

theorem IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_lt {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {a b : R} (hv : v.intValuation b ≤ v.intValuation a) (γ : Multiplicative ℤ) : ∃ (y : R), v.intValuation (b - y * a) < ↑γ

Given a, b ∈ A and v b ≤ v a we can find y : A such that y * a is close to b by the valuation v.

theorem IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integer {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} (hv : (valuation K v) x ≤ 1) (γ : (WithZero (Multiplicative ℤ))ˣ) : ∃ (a : R), (valuation K v) ((algebraMap R K) a - x) < ↑γ

Given x ∈ 𝒪[K] we can find a : A such that a is close to x by the valuation v.

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.

@[instance_reducible]

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

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

@[deprecated IsDedekindDomain.HeightOneSpectrum.adicValued_apply (since := "2026-01-28")]

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 ((WithVal.equiv (valuation K v)) x) = (valuation K v) ((WithVal.equiv (valuation K v)) x)

structure 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, defined as a one-field structure wrapping the uniform-space completion (v.valuation K).Completion.

• ofCompletion :: (
• toCompletion : (HeightOneSpectrum.valuation K v).Completion

  The underlying element of the completion (v.valuation K).Completion.

• )

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

adicCompletion.toCompletion and adicCompletion.ofCompletion as an equivalence.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (self : adicCompletion K v) : (equivCompletion K v) self = self.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_symm_apply_toCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (toCompletion : (HeightOneSpectrum.valuation K v).Completion) : ((equivCompletion K v).symm toCompletion).toCompletion = toCompletion

@[instance_reducible]

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

Equations

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

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : adicCompletion K v ≃+* (HeightOneSpectrum.valuation K v).Completion

adicCompletion.toCompletion as a ring isomorphism onto the underlying completion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv K v = { toEquiv := IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion K v, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (self : adicCompletion K v) : (equiv K v) self = self.toCompletion

@[simp]

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion {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) : { toCompletion := x.toCompletion } = x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : toCompletion 0 = 0

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : toCompletion 1 = 1

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : adicCompletion K v) : (x + y).toCompletion = x.toCompletion + y.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : adicCompletion K v) : (x * y).toCompletion = x.toCompletion * y.toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_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 toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_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 ofCompletion

@[instance_reducible]

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

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.instUniformSpace K v = UniformSpace.comap IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion inferInstance

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

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

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.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 (adicCompletion K v) (WithZero (Multiplicative ℤ))

The v-adic valuation on adicCompletion K v, transported from the completion along equiv.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v = Valuation.comap (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv K v).toRingHom Valued.v

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (MonoidWithZeroHom.ofClass (valuation K v)).valueGroup = (MonoidWithZeroHom.ofClass Valued.v).valueGroup

def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ↥(MonoidWithZeroHom.ofClass (valuation K v)).valueGroup ≃* ↥(MonoidWithZeroHom.ofClass Valued.v).valueGroup

The multiplicative equivalence between the value group of the completion's valuation, pulled back along equiv, and that of the completion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv K v = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(MonoidWithZeroHom.ofClass (valuation K v)).valueGroup) : ↑((valueGroupEquiv K v) a) = ↑a

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀

The order-preserving multiplicative equivalence between the ValueGroup₀ of the completion's valuation, pulled back along equiv, and that of the completion.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : ↥(MonoidWithZeroHom.ofClass (valuation K v)).valueGroup) : (valueGroupOrderIso K v) ↑a = ↑((valueGroupEquiv K v) a)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (g : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀) : MonoidWithZeroHom.ValueGroup₀.embedding ((valueGroupOrderIso K v) g) = MonoidWithZeroHom.ValueGroup₀.embedding g

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict {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) : (valueGroupOrderIso K v) ((valuation K v).restrict x) = Valued.v.restrict x.toCompletion

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Coercion of an element of WithVal (v.valuation K) into the adic completion.

Equations

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

@[instance_reducible, instance 99]

noncomputable 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 : HeightOneSpectrum R) : Coe K (adicCompletion K v)

Coercion of an element of K into the adic completion.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe K v = { coe := fun (k : K) => { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k) } }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion {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) : { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm k) }.toCompletion = ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm k)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.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.extensionValuation x.toCompletion

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion {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.toCompletion = Valued.v x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (y : (HeightOneSpectrum.valuation K v).Completion) : Valued.v { toCompletion := y } = Valued.v y

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe {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 { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm k) } = (HeightOneSpectrum.valuation K v) k

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x y : adicCompletion K v} (h : x.toCompletion = y.toCompletion) : x = y

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : HeightOneSpectrum R} {x y : adicCompletion K v} : x = y ↔ x.toCompletion = y.toCompletion

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 0) } = 0

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) } = 1

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : K) : { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) } = { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } + { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x y : K) : { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) } = { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } * { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

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

toCompletion as a uniform-space isomorphism onto the underlying completion.

Equations

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

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

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

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

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

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

noncomputable 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

@[instance_reducible]

noncomputable 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 }

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

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

@[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))

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

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraCompletion (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 (valuation K v).Completion

The S-algebra structure on the underlying completion.

Equations

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

@[instance_reducible]

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

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion (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) : ((algebraMap S (adicCompletion K v)) r).toCompletion = (algebraMap S (valuation K v).Completion) r

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerCompletionWithZeroMultiplicativeIntValuation (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] {S₀ : Type u_4} [CommSemiring S₀] [Algebra S₀ S] [Algebra S₀ K] [IsScalarTower S₀ S K] : IsScalarTower S₀ S (valuation K v).Completion

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerAdicCompletion (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] {S₀ : Type u_4} [CommSemiring S₀] [Algebra S₀ S] [Algebra S₀ K] [IsScalarTower S₀ S K] : IsScalarTower S₀ S (adicCompletion K v)

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)) : { toCompletion := ↑(r • x) } = r • { toCompletion := ↑x }

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)) = (fun (x : K) => { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap S K)

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : DenseRange ⇑(algebraMap K (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 : HeightOneSpectrum R) (r : R) : { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) } ∈ adicCompletionIntegers K v

@[instance_reducible]

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

@[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) = { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }

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)

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.

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 { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) } = (valuation K v) 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 : HeightOneSpectrum R) (r : R) : ↑r ∈ 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 : HeightOneSpectrum R) (r : R) (x : ↥(adicCompletionIntegers K v)) : ↑(r • x) = r • ↑x

instance IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Module.IsTorsionFree R ↥(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 : HeightOneSpectrum R) : IsScalarTower R (↥(adicCompletionIntegers K v)) (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 : HeightOneSpectrum R) (a : adicCompletion K v) : ∃ b ∈ nonZeroDivisors R, a * ↑b ∈ adicCompletionIntegers K v

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

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valued.v.Integers ↥(adicCompletionIntegers K v)

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : HeightOneSpectrum R} {a : ↥(adicCompletionIntegers K v)} : IsUnit a ↔ Valued.v ↑a = 1

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one {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)ˣ} : a ∈ (adicCompletionIntegers K v).units ↔ Valued.v ↑a = 1

noncomputable def IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) : NNReal

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

Equations

• v.intAdicAbvDef hb r = (WithZeroMulInt.toNNReal ⋯) (v.intValuation r)

theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) : IsNonarchimedean (v.intAdicAbvDef hb)

noncomputable def IsDedekindDomain.HeightOneSpectrum.intAdicAbv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) : AbsoluteValue R ℝ

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

Equations

• v.intAdicAbv hb = { toFun := fun (r : R) => ↑(v.intAdicAbvDef hb r), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) : IsNonarchimedean ⇑(v.intAdicAbv hb)

The v-adic absolute value is nonarchimedean

theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) : (v.intAdicAbv hb) r ≤ 1

theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) : (v.intAdicAbv hb) r < 1 ↔ r ∈ v.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (r : R) : (v.intAdicAbv hb) r = 1 ↔ r ∉ v.asIdeal

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

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 (v.adicAbvDef hb)

noncomputable 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' := ⋯ }

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

theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_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) {b : NNReal} (hb : 1 < b) (r : R) {s : ↥(nonZeroDivisors R)} : (v.adicAbv hb) (IsLocalization.mk' K r s) = (v.intAdicAbv hb) r / (v.intAdicAbv hb) ↑s

The v-adic absolute value of r / s : K is the absolute value of r divided by the absolute value of s.

theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_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) {b : NNReal} (hb : 1 < b) (r : R) : (v.adicAbv hb) ((algebraMap R K) r) = (v.intAdicAbv hb) r

The v-adic absolute value on K extends the v-adic absolute value on R.

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

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

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

theorem Rat.valuation_le_one_iff_den {R : Type u_4} [CommRing R] [IsDedekindDomain R] [Algebra R ℚ] [IsFractionRing R ℚ] {𝔭 : IsDedekindDomain.HeightOneSpectrum R} {x : ℚ} : (IsDedekindDomain.HeightOneSpectrum.valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal