# mathlibdocumentation

ring_theory.discrete_valuation_ring

# 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 : add_valuation R part_enat : 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]
structure discrete_valuation_ring (R : Type u) [comm_ring R] [is_domain R] :
Prop
• to_is_principal_ideal_ring :
• to_local_ring :
• not_a_field' :

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

Instances of this typeclass

A discrete valuation ring R is not a field.

theorem discrete_valuation_ring.irreducible_of_span_eq_maximal_ideal {R : Type u_1} [comm_ring R] [local_ring R] [is_domain R] (ϖ : R) (hϖ : ϖ 0) (h : = ideal.span {ϖ}) :

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

theorem irreducible.maximal_ideal_eq {R : Type u} [comm_ring R] [is_domain R] {ϖ : R} (h : irreducible ϖ) :

Uniformisers exist in a DVR

theorem discrete_valuation_ring.exists_prime (R : Type u) [comm_ring R] [is_domain R]  :
(ϖ : 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

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.

theorem discrete_valuation_ring.aux_pid_of_ufd_of_unique_irreducible (R : Type u) [comm_ring R] [is_domain R] (h₁ : (p : R), ) (h₂ : ⦃p q : R⦄, q) :
theorem discrete_valuation_ring.of_ufd_of_unique_irreducible {R : Type u} [comm_ring R] [is_domain R] (h₁ : (p : R), ) (h₂ : ⦃p q : R⦄, q) :

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 discrete_valuation_ring.associated_pow_irreducible {R : Type u_1} [comm_ring R] [is_domain R] {x : R} (hx : x 0) {ϖ : R} (hirr : irreducible ϖ) :
(n : ), ^ n)
theorem discrete_valuation_ring.eq_unit_mul_pow_irreducible {R : Type u_1} [comm_ring R] [is_domain R] {x : R} (hx : x 0) {ϖ : R} (hirr : irreducible ϖ) :
(n : ) (u : Rˣ), x = u * ϖ ^ n
theorem discrete_valuation_ring.ideal_eq_span_pow_irreducible {R : Type u_1} [comm_ring R] [is_domain R] {s : ideal R} (hs : s ) {ϖ : R} (hirr : irreducible ϖ) :
(n : ), s = ideal.span ^ n}
theorem discrete_valuation_ring.unit_mul_pow_congr_pow {R : Type u_1} [comm_ring R] [is_domain R] {p q : R} (hp : irreducible p) (hq : irreducible q) (u v : Rˣ) (m n : ) (h : u * p ^ m = v * q ^ n) :
m = n
theorem discrete_valuation_ring.unit_mul_pow_congr_unit {R : Type u_1} [comm_ring R] [is_domain R] {ϖ : R} (hirr : irreducible ϖ) (u v : Rˣ) (m n : ) (h : u * ϖ ^ m = v * ϖ ^ n) :
u = v

## The additive valuation on a DVR #

noncomputable def discrete_valuation_ring.add_val (R : Type u) [comm_ring R] [is_domain R]  :

The part_enat-valued additive valuation on a DVR

Equations
theorem discrete_valuation_ring.add_val_def {R : Type u_1} [comm_ring R] [is_domain R] (r : R) (u : Rˣ) {ϖ : R} (hϖ : irreducible ϖ) (n : ) (hr : r = u * ϖ ^ n) :
theorem discrete_valuation_ring.add_val_def' {R : Type u_1} [comm_ring R] [is_domain R] (u : Rˣ) {ϖ : R} (hϖ : irreducible ϖ) (n : ) :
(u * ϖ ^ n) = n
@[simp]
@[simp]
@[simp]
theorem discrete_valuation_ring.add_val_uniformizer {R : Type u_1} [comm_ring R] [is_domain R] {ϖ : R} (hϖ : irreducible ϖ) :
@[simp]
theorem discrete_valuation_ring.add_val_mul {R : Type u_1} [comm_ring R] [is_domain R] {a b : R} :
(a * b) =
theorem discrete_valuation_ring.add_val_pow {R : Type u_1} [comm_ring R] [is_domain R] (a : R) (n : ) :
(a ^ n) =
theorem irreducible.add_val_pow {R : Type u_1} [comm_ring R] [is_domain R] {ϖ : R} (h : irreducible ϖ) (n : ) :
^ n) = n
theorem discrete_valuation_ring.add_val_le_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] {a b : R} :
a b
theorem discrete_valuation_ring.add_val_add {R : Type u_1} [comm_ring R] [is_domain R] {a b : R} :
(a + b)
@[protected, instance]