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
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 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)
Implementation detail: an integral domain in which there is a unit 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.
Equations
- hR.ufd = let p : R := classical.some hR, spec : irreducible (classical.some hR) ∧ ∀ {x : R}, x ≠ 0 → (∃ (n : ℕ), associated (classical.some hR ^ n) x) := _ in {factors := λ (x : R), dite (x = 0) (λ (h : x = 0), 0) (λ (h : ¬x = 0), multiset.repeat p (classical.some _)), factors_prod := _, prime_factors := _}
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 a unit p
such that every nonzero element is associated to a power of p
is a discrete valuation ring.