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.
IsDiscreteValuationRing R
: a predicate expressing that R is a DVR.
Definitions #
addVal R : AddValuation R PartENat
: the additive valuation on a DVR.toEuclideanDomain R : EuclideanDomain R
: a non-canonical structure of Euclidean domain on a DVR, wherex % y = 0
ify ∣ x
andx % y = x
otherwise. The GCD algorithm terminates in two steps.
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.
- exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
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.
Alternative characterisation of discrete valuation rings.
Equations
- IsDiscreteValuationRing.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 IsDiscreteValuationRing.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
An alternative definition of the additive valuation, taking units into account
A noncomputable quotient to define the Euclidean domain structure. The GCD algorithm only takes
two steps to terminate. Given GCD(x,y)
, if x ∣ y
then y%x = 0
so we're done in one step;
otherwise y%x = y
and then GCD(x,y) = GCD(y,x)
which brings us back to the first case.
Equations
- IsDiscreteValuationRing.quotient x y = if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0
Instances For
A noncomputable remainder to define the Euclidean domain structure. The GCD algorithm only takes
two steps to terminate. Given GCD(x,y)
, if x ∣ y
then y%x = 0
so we're done in one step;
otherwise y%x = y
and then GCD(x,y) = GCD(y,x)
which brings us back to the first case.
Instances For
A modification of the valuation, sending 0
to ⊥
instead of ⊤
.
Equations
Instances For
A noncomputable Euclidean domain structure on a discrete valuation ring, where the GCD algorithm
only takes two steps to terminate. Given GCD(x,y)
, if x ∣ y
then y%x = 0
so we're done in one
step; otherwise y%x = y
and then GCD(x,y) = GCD(y,x)
which brings us back to the first case.
See EuclideanDomain.to_principal_ideal_domain
for EuclideanDomain ⇒ PID.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A DVR is a valuation ring.