Discrete valuation rings
This file defines discrete valuation rings (DVRs) and develops a basic interface for them.
Important definitions
There are various definitions of a DVR in the literature; we define a DVR to be a local PID which is not a field (the first definition in Wikipedia) and prove that this is equivalent to being a PID with a unique non-zero prime ideal (the definition in Serre's book "Local Fields").
Let R be an integral domain, assumed to be a principal ideal ring and a local ring.
discrete_valuation_ring R
: a predicate expressing that R is a DVR
Definitions
add_val R : R → ℕ
: the additive valuation on a DVR (sending 0 to 0 rather than the mathematically correct +∞). TODO -- the multiplicative valuation, taking values in something likewith_zero (multiplicative ℤ)
?
Implementation notes
It's a theorem that an element of a DVR is a uniformizer if and only if it's irreducible.
We do not hence define uniformizer
at all, because we can use irreducible
instead.
Tags
discrete valuation ring
- to_is_principal_ideal_ring : is_principal_ideal_ring R
- to_local_ring : local_ring R
- not_a_field' : local_ring.maximal_ideal R ≠ ⊥
An integral domain is a discrete valuation ring (DVR) if it's a local PID which is not a field.
Instances
An element of a DVR is irreducible iff it is a uniformizer, that is, generates the maximal ideal of R
Uniformisers exist in a DVR
an integral domain is a DVR iff it's a PID with a unique non-zero prime ideal
Alternative characterisation of discrete valuation rings.
Equations
- discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R = ∃ (p : R), irreducible p ∧ ∀ {x : R}, x ≠ 0 → (∃ (n : ℕ), associated (p ^ n) x)
An integral domain in which there is an irreducible element p
such that every nonzero element is associated to a power of p
is a unique factorization domain.
See discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization
.
A unique factorization domain with at least one irreducible element in which all irreducible elements are associated is a discrete valuation ring.
An integral domain in which there is an irreducible element p
such that every nonzero element is associated to a power of p
is a discrete valuation ring.
The additive valuation on a DVR
The ℕ
-valued additive valuation on a DVR (returns junk at 0
rather than +∞
)
Equations
- discrete_valuation_ring.add_val R = λ (r : R), dite (r = 0) (λ (hr : r = 0), 0) (λ (hr : ¬r = 0), classical.some _)