# 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

class DiscreteValuationRing (R : Type u) [] [] extends , :

An integral domain is a discrete valuation ring (DVR) if it's a local PID which is not a field.

• principal : ∀ (S : ),
• exists_pair_ne : ∃ (x : R) (y : R), x y
• isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1
• not_a_field' :
Instances
theorem DiscreteValuationRing.not_a_field' {R : Type u} [] [] [self : ] :

A discrete valuation ring R is not a field.

theorem DiscreteValuationRing.irreducible_of_span_eq_maximalIdeal {R : Type u_1} [] [] [] (ϖ : R) (hϖ : ϖ 0) (h : ) :

An element of a DVR is irreducible iff it is a uniformizer, that is, generates the maximal ideal of R.

theorem Irreducible.maximalIdeal_eq {R : Type u} [] [] {ϖ : R} (h : ) :
theorem DiscreteValuationRing.exists_irreducible (R : Type u) [] [] :
∃ (ϖ : R),

Uniformizers exist in a DVR.

theorem DiscreteValuationRing.exists_prime (R : Type u) [] [] :
∃ (ϖ : R),

Uniformizers exist in a DVR.

theorem DiscreteValuationRing.iff_pid_with_one_nonzero_prime (R : Type u) [] [] :
∃! P : , P P.IsPrime

An integral domain is a DVR iff it's a PID with a unique non-zero prime ideal.

theorem DiscreteValuationRing.associated_of_irreducible (R : Type u) [] [] {a : R} {b : R} (ha : ) (hb : ) :

Alternative characterisation of discrete valuation rings.

Equations
Instances For
theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible {R : Type u_1} [] ⦃p : R ⦃q : R (hp : ) (hq : ) :

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.

theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible {R : Type u_1} [] [] (h₁ : ∃ (p : R), ) (h₂ : ∀ ⦃p q : R⦄, ) :
theorem DiscreteValuationRing.aux_pid_of_ufd_of_unique_irreducible (R : Type u) [] [] (h₁ : ∃ (p : R), ) (h₂ : ∀ ⦃p q : R⦄, ) :
theorem DiscreteValuationRing.of_ufd_of_unique_irreducible {R : Type u} [] [] (h₁ : ∃ (p : R), ) (h₂ : ∀ ⦃p q : R⦄, ) :

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.

theorem DiscreteValuationRing.associated_pow_irreducible {R : Type u_1} [] [] {x : R} (hx : x 0) {ϖ : R} (hirr : ) :
∃ (n : ), Associated x (ϖ ^ n)
theorem DiscreteValuationRing.eq_unit_mul_pow_irreducible {R : Type u_1} [] [] {x : R} (hx : x 0) {ϖ : R} (hirr : ) :
∃ (n : ) (u : Rˣ), x = u * ϖ ^ n
theorem DiscreteValuationRing.ideal_eq_span_pow_irreducible {R : Type u_1} [] [] {s : } (hs : s ) {ϖ : R} (hirr : ) :
∃ (n : ), s = Ideal.span {ϖ ^ n}
theorem DiscreteValuationRing.unit_mul_pow_congr_pow {R : Type u_1} [] [] {p : R} {q : R} (hp : ) (hq : ) (u : Rˣ) (v : Rˣ) (m : ) (n : ) (h : u * p ^ m = v * q ^ n) :
m = n
theorem DiscreteValuationRing.unit_mul_pow_congr_unit {R : Type u_1} [] [] {ϖ : R} (hirr : ) (u : Rˣ) (v : Rˣ) (m : ) (n : ) (h : u * ϖ ^ m = v * ϖ ^ n) :
u = v

## The additive valuation on a DVR #

noncomputable def DiscreteValuationRing.addVal (R : Type u) [] [] :

The PartENat-valued additive valuation on a DVR.

Equations
Instances For
theorem DiscreteValuationRing.addVal_def {R : Type u_1} [] [] (r : R) (u : Rˣ) {ϖ : R} (hϖ : ) (n : ) (hr : r = u * ϖ ^ n) :
= n
theorem DiscreteValuationRing.addVal_def' {R : Type u_1} [] [] (u : Rˣ) {ϖ : R} (hϖ : ) (n : ) :
(u * ϖ ^ n) = n
@[simp]
theorem DiscreteValuationRing.addVal_uniformizer {R : Type u_1} [] [] {ϖ : R} (hϖ : ) :
theorem DiscreteValuationRing.addVal_mul {R : Type u_1} [] [] {a : R} {b : R} :
(a * b) =
theorem DiscreteValuationRing.addVal_pow {R : Type u_1} [] [] (a : R) (n : ) :
(a ^ n) =
theorem Irreducible.addVal_pow {R : Type u_1} [] [] {ϖ : R} (h : ) (n : ) :
(ϖ ^ n) = n
theorem DiscreteValuationRing.addVal_eq_top_iff {R : Type u_1} [] [] {a : R} :
a = 0
theorem DiscreteValuationRing.addVal_le_iff_dvd {R : Type u_1} [] [] {a : R} {b : R} :
a b
theorem DiscreteValuationRing.addVal_add {R : Type u_1} [] [] {a : R} {b : R} :
min () () (a + b)
Equations
• =