The valuation of a discrete valuation ring on its own elements

Let R be a discrete valuation ring with fraction field K, and let v be the valuation on K attached to the maximal ideal of R (IsDiscreteValuationRing.maximalIdeal). Mathlib's IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem reads v r < 1, for r : R, as membership in the ideal underlying that height-one prime. This file restates it with the local ring's maximal ideal, and with divisibility by a uniformiser. On R itself, the 𝔪-adic valuation intValuation compares elements by divisibility and vanishes only at 0.

It also compares the valuation of a discrete valuation ring S with that of a valued field K whose valuation ring maps to S through a local homomorphism: the valuation of S, restricted along K → Frac(S), is equivalent to the valuation of K.

Main results

• TauCeti.IsDiscreteValuationRing.valuation_algebraMap_lt_one_iff_mem: v r < 1 exactly when r lies in the maximal ideal.
• TauCeti.IsDiscreteValuationRing.intValuation_le_intValuation_iff_dvd: on R, the 𝔪-adic valuation satisfies v x ≤ v y exactly when y ∣ x.
• IsDedekindDomain.HeightOneSpectrum.supp_intValuation: the adic valuation of a height-one prime of a Dedekind domain has zero support.
• Irreducible.valuation_algebraMap_lt_one_iff_dvd and Irreducible.valuation_algebraMap_eq_one_iff_not_dvd: for a uniformiser ϖ, v r < 1 exactly when ϖ ∣ r, and v r = 1 exactly when ϖ ∤ r.
• TauCeti.isEquiv_comap_valuation_maximalIdeal_of_isLocalHom: a discrete valuation ring dominating the valuation ring of K restricts to the valuation class of K.

theorem TauCeti.IsDiscreteValuationRing.valuation_algebraMap_lt_one_iff_mem {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (r : R) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) r) < 1 ↔ r ∈ IsLocalRing.maximalIdeal R

An element of a discrete valuation ring has valuation less than one in the fraction field exactly when it lies in the maximal ideal.

@[simp]

theorem TauCeti.IsDiscreteValuationRing.intValuation_le_intValuation_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x y : R) : (IsDiscreteValuationRing.maximalIdeal R).intValuation x ≤ (IsDiscreteValuationRing.maximalIdeal R).intValuation y ↔ y ∣ x

The 𝔪-adic valuation of a discrete valuation ring compares elements by divisibility: v x ≤ v y exactly when y ∣ x.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.supp_intValuation {A : Type u_3} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) : v.intValuation.supp = ⊥

The adic valuation of a height-one prime of a Dedekind domain vanishes only at 0.

theorem Irreducible.valuation_algebraMap_lt_one_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} (hϖ : Irreducible ϖ) (r : R) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) r) < 1 ↔ ϖ ∣ r

An element of a discrete valuation ring has valuation less than one in the fraction field exactly when the uniformiser divides it.

theorem Irreducible.valuation_algebraMap_eq_one_iff_not_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} (hϖ : Irreducible ϖ) (r : R) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) r) = 1 ↔ ¬ϖ ∣ r

An element of a discrete valuation ring has valuation one in the fraction field exactly when the uniformiser does not divide it.

theorem TauCeti.isEquiv_comap_valuation_maximalIdeal_of_isLocalHom {K : Type u_3} [Field K] [ValuativeRel K] {M : Type u_4} [Field M] [Algebra K M] {S : Type u_5} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra S M] [IsFractionRing S M] [Algebra (↥(ValuativeRel.valuation K).integer) S] [IsLocalHom (algebraMap (↥(ValuativeRel.valuation K).integer) S)] (h : (algebraMap S M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) S) = (algebraMap K M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) K)) : (Valuation.comap (algebraMap K M) (IsDedekindDomain.HeightOneSpectrum.valuation M (IsDiscreteValuationRing.maximalIdeal S))).IsEquiv (ValuativeRel.valuation K)

The valuation of a discrete valuation ring S with fraction field M, dominating the valuation ring of K, restricts to the valuation class of K: an element of K is integral at S exactly when it lies in the valuation ring of K.