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]
- 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
theorem
discrete_valuation_ring.not_a_field
(R : Type u)
[comm_ring R]
[is_domain R]
[discrete_valuation_ring 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 ϖ) :
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] :
Uniformisers exist in a DVR
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) :
associated a 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) :
associated p 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] :
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) :
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) :
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) :
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) :
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.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 ϖ) :
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
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] :
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]
[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 : ℕ) :
@[simp]
theorem
discrete_valuation_ring.add_val_zero
{R : Type u_1}
[comm_ring R]
[is_domain R]
[discrete_valuation_ring R] :
@[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} :
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] :