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.
Main definitions #
maximal_spectrumdefines the set of nonzero prime ideals ofR. WhenRis a Dedekind domain of Krull dimension 1, this is the set of maximal ideals ofR.maximal_spectrum.int_valuation vis thev-adic valuation onR.maximal_spectrum.valuation vis thev-adic valuation onK.
Main results #
int_valuation_le_one: Thev-adic valuation onRis bounded above by 1.int_valuation_lt_one_iff_dvd: Thev-adic valuation ofr ∈ Ris less than 1 if and only ifvdivides the ideal(r).int_valuation_le_pow_iff_dvd: Thev-adic valuation ofr ∈ Ris less than or equal tomultiplicative.of_add (-n)if and only ifvⁿdivides the ideal(r).int_valuation_exists_uniformizer: There existsπ ∈ Rwithv-adic valuationmultiplicative.of_add (-1).valuation_well_defined: The valuation ofk ∈ Kis independent on how we expresskas a fraction.valuation_of_mk': Thev-adic valuation ofr/s ∈ Kis the valuation ofrdivided by the valuation ofs.valuation_of_algebra_map: Thev-adic valuation onKextends thev-adic valuation onR.valuation_exists_uniformizer: There existsπ ∈ Kwithv-adic valuationmultiplicative.of_add (-1).
Implementation notes #
We are only interested in Dedekind domains with Krull dimension 1. Dedekind domains of Krull
dimension 0 are fields, and for them maximal_spectrum is the empty set, which does not agree with
the set of maximal ideals (which is {(0)}).
Most of the code in this file has already been incorporated to mathlib and can be found in the files
ring_theory/dedekind_domain/ideal.lean and ring_theory/dedekind_domain/adic_valuation.lean. Note
that maximal_spectrum is called height_one_spectrum there, and that some of the names of
definitions and lemmas have been modified. We keep this version of the code here so that this branch
contains all of the code referred to in the article "Formalizing the Rings of Adèles of a Global
Field".
References #
- [G. J. Janusz, Algebraic Number Fields][janusz1996]
- J.W.S. Cassels, A. Frölich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
Tags #
dedekind domain, dedekind ring, adic valuation
Maximal spectrum of a Dedekind domain #
If R is a Dedekind domain of Krull dimension 1, the maximal ideals of R are exactly its nonzero
prime ideals.
We define maximal_spectrum and provide lemmas to recover the facts that maximal ideals are prime
and irreducible.
The maximal spectrum of a Dedekind domain R of Krull dimension 1 is its set of nonzero prime
ideals. Note that this is not the maximal spectrum if R has Krull dimension 0.
Auxiliary lemmas #
We provide auxiliary lemmas about multiplicative.of_add, is_localization, associates and
ideal. They will be moved to the appropriate files when the code is integrated in mathlib.
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. int_valuation_def is the corresponding
multiplicative valuation.
Equations
- v.int_valuation_def r = ite (r = 0) 0 ↑(⇑multiplicative.of_add (-↑((associates.mk v.as_ideal).count (associates.mk (ideal.span {r})).factors)))
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.of_add (-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.
Equations
- v.int_valuation = {to_monoid_with_zero_hom := {to_fun := v.int_valuation_def, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}
There exists π ∈ R with v-adic valuation multiplicative.of_add (-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_def x = let s : ↥R⁰ := classical.some _ in v.int_valuation_def (classical.some _) / v.int_valuation_def ↑s
The valuation of k ∈ K is independent on how we express k as a fraction.
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).
The v-adic valuation of 0 : K equals 0.
The v-adic valuation of 1 : K equals 1.
The v-adic valuation of a product is 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 K.
Equations
- v.valuation = {to_monoid_with_zero_hom := {to_fun := v.valuation_def, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}
There exists π ∈ K with v-adic valuation multiplicative.of_add (-1).
Uniformizers are nonzero.