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.
DiscreteValuationRing R
: a predicate expressing that R is a DVR.
Definitions #
addVal R : AddValuation R PartENat
: the additive valuation on a DVR.
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
An integral domain is a discrete valuation ring (DVR) if it's a local PID which is not a field.
- principal : ∀ (S : Ideal R), Submodule.IsPrincipal S
- exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
- not_a_field' : IsLocalRing.maximalIdeal R ≠ ⊥
Instances
A discrete valuation ring R
is not a field.
An element of a DVR is irreducible iff it is a uniformizer, that is, generates the
maximal ideal of R
.
Uniformizers exist in a DVR.
Uniformizers 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
- DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R = ∃ (p : R), Irreducible p ∧ ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
Instances For
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 DiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization
.
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.
Equations
Instances For
A DVR is a valuation ring.