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.

• IsDiscreteValuationRing R : a predicate expressing that R is a DVR.

Definitions

• addVal R : AddValuation R PartENat : the additive valuation on a DVR.
• toEuclideanDomain R : EuclideanDomain R : a non-canonical structure of Euclidean domain on a DVR, where x % y = 0 if y ∣ x and x % y = x otherwise. The GCD algorithm terminates in two steps.

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 IsDiscreteValuationRing (R : Type u) [CommRing R] [IsDomain R] extends IsPrincipalIdealRing R, IsLocalRing R : Prop

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

• principal (S : Ideal R) : Submodule.IsPrincipal S
• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one {a b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b
• not_a_field' : IsLocalRing.maximalIdeal R ≠ ⊥

theorem IsDiscreteValuationRing.not_a_field (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsLocalRing.maximalIdeal R ≠ ⊥

theorem IsDiscreteValuationRing.not_isField (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ¬IsField R

A discrete valuation ring R is not a field.

theorem IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] [IsDomain R] (ϖ : R) (hϖ : ϖ ≠ 0) (h : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) : Irreducible ϖ

theorem IsDiscreteValuationRing.irreducible_iff_uniformizer {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (ϖ : R) : Irreducible ϖ ↔ IsLocalRing.maximalIdeal 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.maximalIdeal_eq {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (h : Irreducible ϖ) : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}

theorem IsDiscreteValuationRing.exists_irreducible (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ∃ (ϖ : R), Irreducible ϖ

Uniformizers exist in a DVR.

theorem IsDiscreteValuationRing.exists_prime (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ∃ (ϖ : R), Prime ϖ

Uniformizers exist in a DVR.

theorem IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (R : Type u) [CommRing R] [IsDomain R] : IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

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

theorem IsDiscreteValuationRing.associated_of_irreducible (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {a b : R} (ha : Irreducible a) (hb : Irreducible b) : Associated a b

def IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (R : Type u_1) [CommRing R] : Prop

Alternative characterisation of discrete valuation rings.

Equations

• IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R = ∃ (p : R), Irreducible p ∧ ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x

theorem IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible {R : Type u_1} [CommRing R] (hR : HasUnitMulPowIrreducibleFactorization R) ⦃p q : R⦄ (hp : Irreducible p) (hq : Irreducible q) : Associated p q

theorem IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid {R : Type u_1} [CommRing R] [IsDomain R] (hR : HasUnitMulPowIrreducibleFactorization R) : UniqueFactorizationMonoid 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 IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization.

theorem IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (h₁ : ∃ (p : R), Irreducible p) (h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) : HasUnitMulPowIrreducibleFactorization R

theorem IsDiscreteValuationRing.aux_pid_of_ufd_of_unique_irreducible (R : Type u) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (h₁ : ∃ (p : R), Irreducible p) (h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) : IsPrincipalIdealRing R

theorem IsDiscreteValuationRing.of_ufd_of_unique_irreducible {R : Type u} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (h₁ : ∃ (p : R), Irreducible p) (h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) : IsDiscreteValuationRing R

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

theorem IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization {R : Type u} [CommRing R] [IsDomain R] (hR : HasUnitMulPowIrreducibleFactorization R) : IsDiscreteValuationRing 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 IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing {A : Type u_2} {B : Type u_3} {E : Type u_4} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing A] [EquivLike E A B] [RingEquivClass E A B] (e : E) : IsDiscreteValuationRing B

theorem IsDiscreteValuationRing.associated_pow_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : Irreducible ϖ) : ∃ (n : ℕ), Associated x (ϖ ^ n)

theorem IsDiscreteValuationRing.eq_unit_mul_pow_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : Irreducible ϖ) : ∃ (n : ℕ) (u : Rˣ), x = ↑u * ϖ ^ n

theorem IsDiscreteValuationRing.ideal_eq_span_pow_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {s : Ideal R} (hs : s ≠ ⊥) {ϖ : R} (hirr : Irreducible ϖ) : ∃ (n : ℕ), s = Ideal.span {ϖ ^ n}

theorem IsDiscreteValuationRing.unit_mul_pow_congr_pow {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing 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 IsDiscreteValuationRing.unit_mul_pow_congr_unit {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (hirr : Irreducible ϖ) (u v : Rˣ) (m n : ℕ) (h : ↑u * ϖ ^ m = ↑v * ϖ ^ n) : u = v

The additive valuation on a DVR

noncomputable def IsDiscreteValuationRing.addVal (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : AddValuation R ℕ∞

The ℕ∞-valued additive valuation on a DVR.

Equations

• IsDiscreteValuationRing.addVal R = multiplicity_addValuation ⋯

theorem IsDiscreteValuationRing.addVal_def {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (r : R) (u : Rˣ) {ϖ : R} (hϖ : Irreducible ϖ) (n : ℕ) (hr : r = ↑u * ϖ ^ n) : (addVal R) r = ↑n

theorem IsDiscreteValuationRing.addVal_def' {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (u : Rˣ) {ϖ : R} (hϖ : Irreducible ϖ) (n : ℕ) : (addVal R) (↑u * ϖ ^ n) = ↑n

An alternative definition of the additive valuation, taking units into account

theorem IsDiscreteValuationRing.addVal_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : (addVal R) 0 = ⊤

theorem IsDiscreteValuationRing.addVal_one {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : (addVal R) 1 = 0

@[simp]

theorem IsDiscreteValuationRing.addVal_uniformizer {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (hϖ : Irreducible ϖ) : (addVal R) ϖ = 1

theorem IsDiscreteValuationRing.addVal_mul {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {a b : R} : (addVal R) (a * b) = (addVal R) a + (addVal R) b

theorem IsDiscreteValuationRing.addVal_pow {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (a : R) (n : ℕ) : (addVal R) (a ^ n) = n • (addVal R) a

theorem Irreducible.addVal_pow {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (h : Irreducible ϖ) (n : ℕ) : (IsDiscreteValuationRing.addVal R) (ϖ ^ n) = ↑n

theorem IsDiscreteValuationRing.addVal_eq_top_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {a : R} : (addVal R) a = ⊤ ↔ a = 0

theorem IsDiscreteValuationRing.addVal_le_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {a b : R} : (addVal R) a ≤ (addVal R) b ↔ a ∣ b

theorem IsDiscreteValuationRing.addVal_add {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {a b : R} : min ((addVal R) a) ((addVal R) b) ≤ (addVal R) (a + b)

@[simp]

theorem IsDiscreteValuationRing.addVal_eq_zero_of_unit {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (u : Rˣ) : (addVal R) ↑u = 0

theorem IsDiscreteValuationRing.addVal_eq_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {x : R} : (addVal R) x = 0 ↔ IsUnit x

instance IsDiscreteValuationRing.instIsHausdorffMaximalIdeal (R : Type u_2) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsHausdorff (IsLocalRing.maximalIdeal R) R

def IsDiscreteValuationRing.quotient {R : Type u_2} [CommRing R] (x y : R) : R

A noncomputable quotient to define the Euclidean domain structure. The GCD algorithm only takes two steps to terminate. Given GCD(x,y), if x ∣ y then y%x = 0 so we're done in one step; otherwise y%x = y and then GCD(x,y) = GCD(y,x) which brings us back to the first case.

Equations

• IsDiscreteValuationRing.quotient x y = if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0

def IsDiscreteValuationRing.remainder {R : Type u_2} [CommRing R] (x y : R) : R

A noncomputable remainder to define the Euclidean domain structure. The GCD algorithm only takes two steps to terminate. Given GCD(x,y), if x ∣ y then y%x = 0 so we're done in one step; otherwise y%x = y and then GCD(x,y) = GCD(y,x) which brings us back to the first case.

Equations

• IsDiscreteValuationRing.remainder x y = if y ∣ x then 0 else x

def IsDiscreteValuationRing.toWithBotNat {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x : R) : WithBot ℕ

A modification of the valuation, sending 0 to ⊥ instead of ⊤.

Equations

• IsDiscreteValuationRing.toWithBotNat x = (IsDiscreteValuationRing.addVal R) x

@[simp]

theorem IsDiscreteValuationRing.toWithBotNat_zero {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : toWithBotNat 0 = ⊥

@[simp]

theorem IsDiscreteValuationRing.toWithBotNat_eq_bot_iff {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x : R) : toWithBotNat x = ⊥ ↔ x = 0

@[simp]

theorem IsDiscreteValuationRing.bot_lt_toWithBotNat_iff {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x : R) : ⊥ < toWithBotNat x ↔ x ≠ 0

theorem IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : toWithBotNat x ≤ toWithBotNat y ↔ x ∣ y

theorem IsDiscreteValuationRing.dvd_of_toWithBotNat_le_toWithBotNat {R : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (x y : R) (hx : x ≠ 0) (hle : toWithBotNat x ≤ toWithBotNat y) : x ∣ y

def IsDiscreteValuationRing.toEuclideanDomain (R : Type u_2) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : EuclideanDomain R

A noncomputable Euclidean domain structure on a discrete valuation ring, where the GCD algorithm only takes two steps to terminate. Given GCD(x,y), if x ∣ y then y%x = 0 so we're done in one step; otherwise y%x = y and then GCD(x,y) = GCD(y,x) which brings us back to the first case. See EuclideanDomain.to_principal_ideal_domain for EuclideanDomain ⇒ PID.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance of_isDiscreteValuationRing (A : Type u) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] : ValuationRing A

A DVR is a valuation ring.

theorem Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O) [IsDiscreteValuationRing O] {ϖ : O} (_h : Irreducible ϖ) : ↑(IsLocalRing.maximalIdeal O) = {y : O | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}

theorem Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O) [IsDiscreteValuationRing O] {ϖ : O} (_h : Irreducible ϖ) (n : ℕ) : ↑(IsLocalRing.maximalIdeal O ^ n) = {y : O | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

theorem Irreducible.maximalIdeal_eq_setOf_le_v_coe {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer} (h : Irreducible ϖ) : ↑(IsLocalRing.maximalIdeal ↥v.integer) = {y : ↥v.integer | v ↑y ≤ v ↑ϖ}

theorem Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer} (h : Irreducible ϖ) (n : ℕ) : ↑(IsLocalRing.maximalIdeal ↥v.integer ^ n) = {y : ↥v.integer | v ↑y ≤ v ↑ϖ ^ n}