mathlib documentation

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.

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

@[class]
structure discrete_valuation_ring (R : Type u) [integral_domain R] :
Prop

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

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.

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.

theorem discrete_valuation_ring.associated_pow_irreducible {R : Type u_1} [integral_domain R] [discrete_valuation_ring R] {x : R} (hx : x 0) {ϖ : R} :
irreducible ϖ(∃ (n : ), associated x ^ n))

theorem discrete_valuation_ring.ideal_eq_span_pow_irreducible {R : Type u_1} [integral_domain R] [discrete_valuation_ring R] {s : ideal R} (hs : s ) {ϖ : R} :
irreducible ϖ(∃ (n : ), s = ideal.span ^ n})

theorem discrete_valuation_ring.unit_mul_pow_congr_pow {R : Type u_1} [integral_domain R] [discrete_valuation_ring R] {p q : R} (hp : irreducible p) (hq : irreducible q) (u v : units R) (m n : ) :
(u) * p ^ m = (v) * q ^ nm = n

theorem discrete_valuation_ring.unit_mul_pow_congr_unit {R : Type u_1} [integral_domain R] [discrete_valuation_ring R] {ϖ : R} (hirr : irreducible ϖ) (u v : units R) (m n : ) :
(u) * ϖ ^ m = (v) * ϖ ^ nu = v