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.int_valuation_le_one
: Thev
-adic valuation onR
is bounded above by 1.IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd
: Thev
-adic valuation ofr ∈ R
is less than 1 if and only ifv
divides the ideal(r)
.IsDedekindDomain.HeightOneSpectrum.int_valuation_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.int_valuation_exists_uniformizer
: There existsπ ∈ R
withv
-adic valuationMultiplicative.ofAdd (-1)
.is_dedekind_domain.height_one_spectrum.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.
Instances For
Nonzero elements have nonzero adic valuation.
Nonzero divisors have nonzero valuation.
Nonzero divisors have valuation greater than zero.
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)
.
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.
The v
-adic valuation of 1 : R
equals 1.
The v
-adic valuation of a product equals the product of the valuations.
The v
-adic valuation of a sum is bounded above by the maximum of the valuations.
The v
-adic valuation on R
.
Instances For
There exists π ∈ R
with v
-adic valuation Multiplicative.ofAdd (-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
.
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.
Instances For
The completion of K
with respect to its v
-adic valuation.
Instances For
The ring of integers of adicCompletion
.