Documentation

TauCeti.RingTheory.DedekindDomain.LocalizationAtPrime

The localisation of a Dedekind domain at a height-one prime, inside its fraction field #

Let O be a Dedekind domain with fraction field K and let v be a height-one prime of O. Mathlib's IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain says that the localisation Oᵥ := Localization.AtPrime v.asIdeal is a discrete valuation ring, as a theorem with the nonzero-prime hypothesis explicit. This file records it as an instance for height-one primes, which carry that hypothesis as v.ne_bot. Together with the Algebra Oᵥ K, IsScalarTower O Oᵥ K and IsFractionRing Oᵥ K instances of TauCeti/RingTheory/Localization/AtPrime.lean, every result Mathlib states over a discrete valuation ring R with fraction field K — in particular its theory of integral and minimal Weierstrass equations — now applies to Oᵥ ⊆ K by instance search, for arbitrary O and K.

The remaining results are the two bridges between v and Oᵥ. Downwards: an element of K that comes from Oᵥ has v-adic valuation at most one; hence, by Mathlib's IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one, an element that comes from every Oᵥ comes from O. The latter is O = ⋂ᵥ Oᵥ inside K, and is what lets a property that holds over every localisation descend to O. The ring-of-integers identification is stated for any IsLocalization.AtPrime model of Oᵥ mapping to K over O, not only for Localization.AtPrime v.asIdeal itself.

Sideways: Oᵥ is exactly the ring of integers of the v-adic valuation, and the discrete valuation Oᵥ carries as a discrete valuation ring — Mathlib's IsDiscreteValuationRing.maximalIdeal Oᵥ, the phrasing of every statement it makes over a discrete valuation ring — is the v-adic valuation itself. Without that identification a result proved at Oᵥ cannot be compared with the v-adic factorisation of an element of O.

Main declarations #

source
instance IsDedekindDomain.HeightOneSpectrum.isDiscreteValuationRing_localizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] (v : HeightOneSpectrum O) :
IsDiscreteValuationRing (Localization.AtPrime v.asIdeal)

The localisation of a Dedekind domain at a height-one prime is a discrete valuation ring. With the Algebra, IsScalarTower and IsFractionRing instances of TauCeti/RingTheory/Localization/AtPrime.lean, this is what lets Mathlib's theory over a discrete valuation ring and its fraction field apply at each height-one prime of O.

source
theorem IsDedekindDomain.HeightOneSpectrum.integers_valuation_of_isLocalizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : HeightOneSpectrum O) (S : Type u_3) [CommRing S] [Algebra O S] [IsLocalization.AtPrime S v.asIdeal] [Algebra S K] [IsScalarTower O S K] :
(valuation K v).Integers S

Any model of the localisation at v mapping to K over O is the ring of integers of the v-adic valuation. This gives the valuation bound on its elements as map_le_one, and makes the unit and divisibility API of Valuation.Integers available.

source
theorem IsDedekindDomain.HeightOneSpectrum.isInteger_of_forall_isInteger_localizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (x : K) (h : ∀ (v : HeightOneSpectrum O), IsLocalization.IsInteger (Localization.AtPrime v.asIdeal) x) :
IsLocalization.IsInteger O x

O is the intersection of its localisations at height-one primes, inside K: an element of K that comes from Localization.AtPrime v.asIdeal for every v comes from O. This is the form in which a property holding over every localisation descends to O, as for the coefficients of a Weierstrass equation in WeierstrassCurve.isIntegral_of_forall_isIntegral_localizationAtPrime.

source
theorem IsDedekindDomain.HeightOneSpectrum.isUnit_of_forall_isUnit_localizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (x : K) (hx : x ≠ 0) (h : ∀ (v : HeightOneSpectrum O), ∃ (u : (Localization.AtPrime v.asIdeal)ˣ), (algebraMap (Localization.AtPrime v.asIdeal) K) ↑u = x) :
∃ (u : Oˣ), (algebraMap O K) ↑u = x

A nonzero element of the fraction field which is the image of a unit in every height-one localisation is the image of a unit of the Dedekind domain. The nonzero assumption also covers the case where the height-one spectrum is empty.

source
theorem IsDedekindDomain.HeightOneSpectrum.irreducible_algebraMap_localizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] (v : HeightOneSpectrum O) {ϖ : O} (hϖ : v.intValuation ϖ = WithZero.exp (-1)) :
Irreducible ((algebraMap O (Localization.AtPrime v.asIdeal)) ϖ)

A v-adic uniformiser of O is irreducible in the localisation at v. This is what identifies the discrete valuation of Oᵥ with the v-adic valuation in valuation_maximalIdeal_localizationAtPrime.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuation_maximalIdeal_localizationAtPrime {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : HeightOneSpectrum O) (x : K) :
(valuation K (IsDiscreteValuationRing.maximalIdeal (Localization.AtPrime v.asIdeal))) x = (valuation K v) x

The valuation of the discrete valuation ring Oᵥ is the v-adic valuation. Mathlib's theory of minimal Weierstrass equations, like every other statement it makes over a discrete valuation ring, is phrased through IsDiscreteValuationRing.maximalIdeal Oᵥ; this lemma reads such a statement as one about v, which is what lets the local data at the height-one primes of O be assembled into a single object over O.