Adic valuations on the fraction field of a Dedekind domain

Mathlib attaches to every height one prime 𝔭 of a Dedekind domain R a normalized ℤᵐ⁰-valued valuation 𝔭.valuation K of the fraction field K, and shows that distinct primes give inequivalent valuations. This file proves the converse: a normalized valuation of K whose valuation ring contains R is 𝔭.valuation K for a unique height one prime 𝔭 of R, namely the centre of the valuation on R.

The adic valuation is trivial on any semifield of constants acting on R: every nonzero constant is a unit of R, so it lies outside every prime ideal.

The general centre construction and its membership lemmas are in TauCeti.RingTheory.Valuation.Center. There, Valuation.heightOneSpectrum bundles a nonzero prime ideal as HeightOneSpectrum R; the Dedekind assumption here makes it a height one prime.

The value group of the adic valuation itself is read off from Mathlib's definition, and this file records the one conversion the rest of the library needs: an element has order of vanishing 1 at v exactly when its adic value is WithZero.exp (-1), so the additive order of vanishing used by the class-group interface and the multiplicative value can be read off from one another.

Main results

• Valuation.eq_valuation_of_forall_mem_asIdeal_iff: a normalized valuation bounded by 1 on R and of positive value exactly on a height one prime 𝔭 is the adic valuation of 𝔭.
• Valuation.valuation_heightOneSpectrum: the adic valuation of the centre of w on R is w.
• Valuation.existsUnique_heightOneSpectrum_valuation_eq: the centre is the only height one prime whose adic valuation is w.
• IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_eq_one_iff: order of vanishing 1 at v is the value WithZero.exp (-1), which relates the multiplicative value group of the adic valuation to the additive order of vanishing used by the class-group interface.
• IsDedekindDomain.HeightOneSpectrum.isTrivialOn_valuation: adic valuations are trivial on semifield constants.

Implementation notes

The comparison goes through Valuation.isEquiv_iff_val_le_one and the normalization lemma Valuation.eq_of_isEquiv_of_surjective: both valuations are surjective onto ℤᵐ⁰, so it is enough to see that they have the same valuation ring. That in turn uses only that the two valuations are bounded by 1 on R and are < 1 on the same elements of R, together with Mathlib's IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq, which writes an arbitrary element of K as a fraction with denominator outside 𝔭, in one of the two possible directions.

The comparison theorems assume R is Dedekind and w is surjective. Surjectivity supplies nontriviality through Valuation.isNontrivial_of_surjective, allowing the nonzero prime centre to be bundled using the general construction.

theorem Valuation.eq_valuation_of_forall_mem_asIdeal_iff {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {w : Valuation K (WithZero (Multiplicative ℤ))} [IsFractionRing R K] [IsDedekindDomain R] {𝔭 : IsDedekindDomain.HeightOneSpectrum R} (hw : Function.Surjective ⇑w) (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) (h𝔭 : ∀ (r : R), r ∈ 𝔭.asIdeal ↔ w ((algebraMap R K) r) < 1) : IsDedekindDomain.HeightOneSpectrum.valuation K 𝔭 = w

A normalized valuation of the fraction field of a Dedekind domain R that is bounded by 1 on R and of positive value exactly at a height one prime 𝔭 is the adic valuation of 𝔭.

@[simp]

theorem Valuation.valuation_heightOneSpectrum {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {w : Valuation K (WithZero (Multiplicative ℤ))} [IsFractionRing R K] [IsDedekindDomain R] (hw : Function.Surjective ⇑w) (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : IsDedekindDomain.HeightOneSpectrum.valuation K (heightOneSpectrum R w hR) = w

The adic valuation of the centre of w on R is w itself: a normalized valuation of the fraction field of a Dedekind domain whose valuation ring contains that domain is adic.

theorem Valuation.eq_heightOneSpectrum {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {w : Valuation K (WithZero (Multiplicative ℤ))} [IsFractionRing R K] [IsDedekindDomain R] {𝔮 : IsDedekindDomain.HeightOneSpectrum R} (hw : Function.Surjective ⇑w) (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) (h : IsDedekindDomain.HeightOneSpectrum.valuation K 𝔮 = w) : 𝔮 = heightOneSpectrum R w hR

A height one prime whose adic valuation is w is the centre of w.

theorem Valuation.existsUnique_heightOneSpectrum_valuation_eq (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {w : Valuation K (WithZero (Multiplicative ℤ))} [IsFractionRing R K] [IsDedekindDomain R] (hw : Function.Surjective ⇑w) (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : ∃! 𝔭 : IsDedekindDomain.HeightOneSpectrum R, IsDedekindDomain.HeightOneSpectrum.valuation K 𝔭 = w

A normalized valuation of the fraction field of a Dedekind domain R whose valuation ring contains R is the adic valuation of a unique height one prime of R.

theorem Valuation.exists_heightOneSpectrum_isEquiv_of_le_one (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (u : Valuation K (WithZero (Multiplicative ℤ))) [u.IsNontrivial] (hR : ∀ (r : R), u ((algebraMap R K) r) ≤ 1) : ∃ (𝔭 : IsDedekindDomain.HeightOneSpectrum R), (IsDedekindDomain.HeightOneSpectrum.valuation K 𝔭).IsEquiv u ∧ ∀ (r : R), r ∈ 𝔭.asIdeal ↔ u ((algebraMap R K) r) < 1

A nontrivial valuation of K bounded by 1 on R is adic up to equivalence. It is equivalent to the adic valuation of the centre of its normalization, and that centre collects exactly the elements of R whose value drops below 1.

Normalizing is what makes the centre's adic valuation equal the valuation rather than merely equivalent to it (valuation_heightOneSpectrum); a valuation that is only bounded, not normalized, still picks out the same prime, which is what this states.

theorem IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_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) (x : K) : -((valuation K v) x).log = 1 ↔ (valuation K v) x = WithZero.exp (-1)

An element has order of vanishing exactly 1 at v exactly when its adic value is WithZero.exp (-1).

The value group of HeightOneSpectrum.valuation is WithZero (Multiplicative ℤ), whose multiplicative identity 1 is the value zero, that is, order of vanishing zero; an element of order of vanishing 1 is instead written WithZero.exp (-1), the value of a generator of v.asIdeal. So v.valuation K x = 1 says that x is a local unit at v, which an element of nonzero order of vanishing is not. This is the equivalence that relates the multiplicative value of an element to the additive order of vanishing used by the class-group interface, whose adicOrd is -WithZero.log of this valuation.

instance IsDedekindDomain.HeightOneSpectrum.isTrivialOn_valuation (k : Type u_1) (F : Type u_2) {R : Type u_3} [Semifield k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : HeightOneSpectrum R) : Valuation.IsTrivialOn k (valuation F p)

The adic valuation of a height-one prime of a Dedekind k-algebra is trivial on the semifield k: a nonzero constant is a unit of R, hence lies outside every prime ideal.