mathlib3 documentation

ring_theory.dedekind_domain.adic_valuation

Adic valuations on Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.adic_completion,and its ring of integers, denoted v.adic_completion_integers.

Main definitions #

Main results #

Implementation notes #

We are only interested in Dedekind domains with Krull dimension 1.

References #

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. int_valuation_def is the corresponding multiplicative valuation.

Equations

Nonzero elements have nonzero adic valuation.

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 a product equals the product of the valuations.

The v-adic valuation of a sum is bounded above by the maximum of the valuations.

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

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).

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.adic_completion, and its ring of integers, denoted v.adic_completion_integers.

K as a valued field with the v-adic valuation.

Equations