mathlib3 documentation

ring_theory.discrete_valuation_ring.basic

Discrete valuation rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : is_principal_ideal_ring R
to_local_ring : local_ring R
not_a_field' : local_ring.maximal_ideal R ≠ ⊥

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

Instances of this typeclass

padic_int.discrete_valuation_ring

theorem discrete_valuation_ring.not_a_field (R : Type u) [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

local_ring.maximal_ideal R ≠ ⊥

theorem discrete_valuation_ring.not_is_field (R : Type u) [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

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 : local_ring.maximal_ideal R = ideal.span {ϖ}) :

theorem discrete_valuation_ring.irreducible_iff_uniformizer {R : Type u} [comm_ring R] [is_domain R] [discrete_valuation_ring R] (ϖ : R) :

irreducible ϖ ↔ local_ring.maximal_ideal R = 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] [discrete_valuation_ring R] {ϖ : R} (h : irreducible ϖ) :

local_ring.maximal_ideal R = ideal.span {ϖ}

theorem discrete_valuation_ring.exists_irreducible (R : Type u) [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

∃ (ϖ : R), irreducible ϖ

Uniformisers exist in a DVR

theorem discrete_valuation_ring.exists_prime (R : Type u) [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

∃ (ϖ : R), prime ϖ

Uniformisers exist in a DVR

theorem discrete_valuation_ring.iff_pid_with_one_nonzero_prime (R : Type u) [comm_ring R] [is_domain R] :

discrete_valuation_ring R ↔ is_principal_ideal_ring R ∧ ∃! (P : ideal R), P ≠ ⊥ ∧ P.is_prime

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

theorem discrete_valuation_ring.associated_of_irreducible (R : Type u) [comm_ring R] [is_domain R] [discrete_valuation_ring R] {a b : R} (ha : irreducible a) (hb : irreducible b) :

def discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization (R : Type u_1) [comm_ring R] :

Prop

Alternative characterisation of discrete valuation rings.

Equations

discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R = ∃ (p : R), irreducible p ∧ ∀ {x : R}, x ≠ 0 → (∃ (n : ℕ), associated (p ^ n) x)

theorem discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.unique_irreducible {R : Type u_1} [comm_ring R] (hR : discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R) ⦃p q : R⦄ (hp : irreducible p) (hq : irreducible q) :

theorem discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.to_unique_factorization_monoid {R : Type u_1} [comm_ring R] (hR : discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R) [is_domain R] :

unique_factorization_monoid R

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.has_unit_mul_pow_irreducible_factorization.of_ufd_of_unique_irreducible {R : Type u_1} [comm_ring R] [is_domain R] [unique_factorization_monoid R] (h₁ : ∃ (p : R), irreducible p) (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :

discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R

theorem discrete_valuation_ring.aux_pid_of_ufd_of_unique_irreducible (R : Type u) [comm_ring R] [is_domain R] [unique_factorization_monoid R] (h₁ : ∃ (p : R), irreducible p) (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :

is_principal_ideal_ring R

theorem discrete_valuation_ring.of_ufd_of_unique_irreducible {R : Type u} [comm_ring R] [is_domain R] [unique_factorization_monoid R] (h₁ : ∃ (p : R), irreducible p) (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :

discrete_valuation_ring R

A unique factorization domain with at least one irreducible element in which all irreducible elements are associated is a discrete valuation ring.

theorem discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization {R : Type u} [comm_ring R] [is_domain R] (hR : discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization R) :

discrete_valuation_ring R

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] [discrete_valuation_ring R] {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : irreducible ϖ) :

∃ (n : ℕ), associated x (ϖ ^ n)

theorem discrete_valuation_ring.eq_unit_mul_pow_irreducible {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring 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] [discrete_valuation_ring 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] [discrete_valuation_ring 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] [discrete_valuation_ring 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] [discrete_valuation_ring R] :

add_valuation R part_enat

The part_enat-valued additive valuation on a DVR

Equations

discrete_valuation_ring.add_val R = multiplicity.add_valuation _

theorem discrete_valuation_ring.add_val_def {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] (r : R) (u : Rˣ) {ϖ : R} (hϖ : irreducible ϖ) (n : ℕ) (hr : r = ↑u * ϖ ^ n) :

⇑(discrete_valuation_ring.add_val R) r = ↑n

theorem discrete_valuation_ring.add_val_def' {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] (u : Rˣ) {ϖ : R} (hϖ : irreducible ϖ) (n : ℕ) :

⇑(discrete_valuation_ring.add_val R) (↑u * ϖ ^ n) = ↑n

@[simp]

theorem discrete_valuation_ring.add_val_zero {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

⇑(discrete_valuation_ring.add_val R) 0 = ⊤

@[simp]

theorem discrete_valuation_ring.add_val_one {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

⇑(discrete_valuation_ring.add_val R) 1 = 0

@[simp]

theorem discrete_valuation_ring.add_val_uniformizer {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {ϖ : R} (hϖ : irreducible ϖ) :

⇑(discrete_valuation_ring.add_val R) ϖ = 1

@[simp]

theorem discrete_valuation_ring.add_val_mul {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {a b : R} :

⇑(discrete_valuation_ring.add_val R) (a * b) = ⇑(discrete_valuation_ring.add_val R) a + ⇑(discrete_valuation_ring.add_val R) b

theorem discrete_valuation_ring.add_val_pow {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] (a : R) (n : ℕ) :

⇑(discrete_valuation_ring.add_val R) (a ^ n) = n • ⇑(discrete_valuation_ring.add_val R) a

theorem irreducible.add_val_pow {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {ϖ : R} (h : irreducible ϖ) (n : ℕ) :

⇑(discrete_valuation_ring.add_val R) (ϖ ^ n) = ↑n

theorem discrete_valuation_ring.add_val_eq_top_iff {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {a : R} :

⇑(discrete_valuation_ring.add_val R) a = ⊤ ↔ a = 0

theorem discrete_valuation_ring.add_val_le_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {a b : R} :

⇑(discrete_valuation_ring.add_val R) a ≤ ⇑(discrete_valuation_ring.add_val R) b ↔ a ∣ b

theorem discrete_valuation_ring.add_val_add {R : Type u_1} [comm_ring R] [is_domain R] [discrete_valuation_ring R] {a b : R} :

linear_order.min (⇑(discrete_valuation_ring.add_val R) a) (⇑(discrete_valuation_ring.add_val R) b) ≤ ⇑(discrete_valuation_ring.add_val R) (a + b)

@[protected, instance]

def discrete_valuation_ring.is_Hausdorff (R : Type u_1) [comm_ring R] [is_domain R] [discrete_valuation_ring R] :

is_Hausdorff (local_ring.maximal_ideal R) R