Valuations associated to discrete valuation rings

Given a discrete valuation ring A with field of fractions K, the maximal ideal of A is a height-one prime, and the associated valuation (maximalIdeal A).valuation K is a rank-one discrete valuation on K.

Main Definitions

• IsDiscreteValuationRing.maximalIdeal: The maximal ideal of A (as an element of HeightOneSpectrum A).
• IsDiscreteValuationRing.equivValuationSubring: The ring isomorphism between a DVR and the unit ball in its field of fractions endowed with the adic valuation of the maximal ideal.

Main Results

• IsDiscreteValuationRing.isRankOneDiscrete: Given a DVR A and a field K satisfying IsFractionRing A K, the valuation induced on K is discrete.

def IsDiscreteValuationRing.maximalIdeal (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] : IsDedekindDomain.HeightOneSpectrum A

The maximal ideal of a discrete valuation ring.

Equations

• IsDiscreteValuationRing.maximalIdeal A = { asIdeal := IsLocalRing.maximalIdeal A, isPrime := ⋯, ne_bot := ⋯ }

instance IsDiscreteValuationRing.isRankOneDiscrete (A : Type u_1) (K : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] : (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).IsRankOneDiscrete

theorem IsDiscreteValuationRing.exists_lift_of_le_one {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (H : (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)) x ≤ 1) : ∃ (a : A), (algebraMap A K) a = x

theorem IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] : MonoidHom.mker (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)) = Submonoid.map (algebraMap A K) (IsUnit.submonoid A)

theorem IsDiscreteValuationRing.associated_of_valuation_eq {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] (x y : K) (h : (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)) x = (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)) y) : ∃ (u : Aˣ), u • x = y

theorem IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] : Subring.map (algebraMap A K) ⊤ = (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).valuationSubring.toSubring

noncomputable def IsDiscreteValuationRing.equivValuationSubring {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] : A ≃+* ↥(IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).valuationSubring

The ring isomorphism between a DVR A and the valuation subring of a field of fractions of A endowed with the adic valuation of the maximal ideal.

Equations

• IsDiscreteValuationRing.equivValuationSubring = (Subring.topEquiv.symm.trans (⊤.equivMapOfInjective (algebraMap A K) ⋯)).trans (RingEquiv.subringCongr ⋯)

theorem IsDiscreteValuationRing.intValuation_maximalIdeal {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (x : A) : (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun (x : ℕ) => ↑(Multiplicative.ofAdd ↑x)) ((addVal A) x))⁻¹