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 thev
-adic valuation onR
.IsDedekindDomain.HeightOneSpectrum.valuation v
is thev
-adic valuation onK
.IsDedekindDomain.HeightOneSpectrum.adicCompletion v
is the completion ofK
with respect to itsv
-adic valuation.IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers v
is the ring of integers ofv.adicCompletion
.
Main results #
IsDedekindDomain.HeightOneSpectrum.intValuation_le_one
: Thev
-adic valuation onR
is bounded above by 1.IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd
: Thev
-adic valuation ofr ∈ R
is less than 1 if and only ifv
divides the ideal(r)
.IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd
: Thev
-adic valuation ofr ∈ R
is less than or equal toMultiplicative.ofAdd (-n)
if and only ifvⁿ
divides the ideal(r)
.IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer
: There existsπ ∈ R
withv
-adic valuationMultiplicative.ofAdd (-1)
.IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'
: Thev
-adic valuation ofr/s ∈ K
is the valuation ofr
divided by the valuation ofs
.IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
: Thev
-adic valuation onK
extends thev
-adic valuation onR
.IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer
: There existsπ ∈ K
withv
-adic valuationMultiplicative.ofAdd (-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ölich, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]
Tags #
dedekind domain, dedekind ring, adic valuation
Adic valuations on the Dedekind domain R #
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 ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))
Instances For
Nonzero elements have nonzero adic valuation.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero
.
Nonzero elements have nonzero adic valuation.
Nonzero divisors have nonzero valuation.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'
.
Nonzero divisors have nonzero valuation.
Nonzero divisors have valuation greater than zero.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le
.
Nonzero divisors have valuation greater than zero.
The v
-adic valuation on R
is bounded above by 1.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_one
.
The v
-adic valuation on R
is bounded above by 1.
The v
-adic valuation of r ∈ R
is less than 1 if and only if v
divides the ideal (r)
.
Alias of 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)
.
The v
-adic valuation of r ∈ R
is less than Multiplicative.ofAdd (-n)
if and only if
vⁿ
divides the ideal (r)
.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd
.
The v
-adic valuation of r ∈ R
is less than Multiplicative.ofAdd (-n)
if and only if
vⁿ
divides the ideal (r)
.
The v
-adic valuation of 0 : R
equals 0.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'
.
The v
-adic valuation of 0 : R
equals 0.
The v
-adic valuation of 1 : R
equals 1.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'
.
The v
-adic valuation of 1 : R
equals 1.
The v
-adic valuation of a product equals the product of the valuations.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'
.
The v
-adic valuation of a product equals the product of the valuations.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le
.
The v
-adic valuation of a sum is bounded above by the maximum of the valuations.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'
.
The v
-adic valuation of a sum is bounded above by the maximum of the valuations.
The v
-adic valuation on R
.
Equations
- v.intValuation = { toFun := v.intValuationDef, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }
Instances For
There exists π ∈ R
with v
-adic valuation Multiplicative.ofAdd (-1)
.
Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer
.
There exists π ∈ R
with v
-adic valuation Multiplicative.ofAdd (-1)
.
The I
-adic valuation of a generator of I
equals (-1 : ℤₘ₀)
Adic valuations on the field of fractions K
#
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
- v.valuation = v.intValuation.extendToLocalization ⋯ K
Instances For
The v
-adic valuation of r/s ∈ K
is the valuation of r
divided by the valuation of s
.
The v
-adic valuation on K
extends the v
-adic valuation on R
.
The v
-adic valuation on R
is bounded above by 1.
The v
-adic valuation of r ∈ R
is less than 1 if and only if v
divides the ideal (r)
.
There exists π ∈ K
with v
-adic valuation Multiplicative.ofAdd (-1)
.
Uniformizers are nonzero.
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
.
K
as a valued field with the v
-adic valuation.
Equations
- v.adicValued = Valued.mk' v.valuation
Instances For
The completion of K
with respect to its v
-adic valuation.
Instances For
Equations
- IsDedekindDomain.HeightOneSpectrum.instFieldAdicCompletion K v = UniformSpace.Completion.instField
Equations
- IsDedekindDomain.HeightOneSpectrum.instInhabitedAdicCompletion K v = { default := 0 }
Equations
- IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion K v = Valued.valuedCompletion
Equations
- ⋯ = ⋯
Equations
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe K v = inferInstance
The ring of integers of adicCompletion
.
Equations
- IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v = Valued.v.valuationSubring
Instances For
Equations
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯