mathlib documentation

ring_theory.valuation.valuation_ring

Valuation Rings #

A valuation ring is a domain such that for every pair of elements a b, either a divides b or vice-versa.

Any valuation ring induces a natural valuation on its fraction field, as we show in this file. Namely, given the following instances: [comm_ring A] [is_domain A] [valuation_ring A] [field K] [algebra A K] [is_fraction_ring A K], there is a natural valuation valuation A K on K with values in value_group A K where the image of A under algebra_map A K agrees with (valuation A K).integer.

We also show that valuation rings are local and that their lattice of ideals is totally ordered.

@[class]
structure valuation_ring (A : Type u) [comm_ring A] [is_domain A] :
Prop
  • cond : ∀ (a b : A), ∃ (c : A), a * c = b b * c = a

An integral domain is called a valuation ring provided that for any pair of elements a b : A, either a divides b or vice versa.

Instances of this typeclass
@[protected, instance]
Equations
@[protected, instance]
def valuation_ring.value_group.has_le (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_zero (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_one (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_mul (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_inv (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :
Equations
@[protected]
theorem valuation_ring.le_total (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (a b : valuation_ring.value_group A K) :
a b b a
@[protected, instance]
Equations

Any valuation ring induces a valuation on its fraction field.

Equations
theorem valuation_ring.mem_integer_iff (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (x : K) :
x (valuation_ring.valuation A K).integer ∃ (a : A), (algebra_map A K) a = x
noncomputable def valuation_ring.equiv_integer (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] :

The valuation ring A is isomorphic to the ring of integers of its associated valuation.

Equations
@[simp]
theorem valuation_ring.coe_equiv_integer_apply (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (a : A) :
@[protected, instance]
theorem valuation_ring.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [comm_ring 𝒪] [is_domain 𝒪] [field K] [algebra 𝒪 K] [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (hh : v.integers 𝒪) :

If 𝒪 satisfies v.integers 𝒪 where v is a valuation on a field, then 𝒪 is a valuation ring.

@[protected, instance]
def valuation_ring.of_field (K : Type u) [field K] :

A field is a valuation ring.

@[protected, instance]

A DVR is a valuation ring.