# mathlibdocumentation

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 provide the equivalence of the following notions for a domain R in valuation_ring.tfae.

1. R is a valuation ring.
2. For each x : fraction_ring K, either x or x⁻¹ is in R.
3. "divides" is a total relation on the elements of R.
4. "contains" is a total relation on the ideals of R.
5. R is a local bezout domain.
@[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
def valuation_ring.value_group (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Type v

The value group of the valuation ring A.

Equations
Instances for valuation_ring.value_group
@[protected, instance]
def valuation_ring.value_group.inhabited (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_le (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
• = {le := λ (x y : , (λ (a b : K), ∃ (c : A), c b = a) _}
@[protected, instance]
def valuation_ring.value_group.has_zero (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_one (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_mul (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
@[protected, instance]
def valuation_ring.value_group.has_inv (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] :
Equations
• = {inv := λ (x : , (λ (a : K), _}
@[protected]
theorem valuation_ring.le_total (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] [is_domain A] [ K] (a b : K) :
a b b a
@[protected, instance]
noncomputable def valuation_ring.value_group.linear_ordered_comm_group_with_zero (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] [is_domain A] [ K] :
Equations
def valuation_ring.valuation (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] [is_domain A] [ K] :

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] [ K] [is_domain A] [ K] (x : K) :
x ∃ (a : A), K) a = x
noncomputable def valuation_ring.equiv_integer (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] [is_domain 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] [ K] [is_domain A] [ K] (a : A) :
a) = K) a
theorem valuation_ring.range_algebra_map_eq (A : Type u) [comm_ring A] (K : Type v) [field K] [ K] [is_domain A] [ K] :
= K).range
@[protected, instance]
def valuation_ring.local_ring (A : Type u) [comm_ring A] [is_domain A]  :
@[protected, instance]
Equations
theorem valuation_ring.iff_dvd_total {R : Type u_1} [comm_ring R] [is_domain R] :
theorem valuation_ring.iff_ideal_total {R : Type u_1} [comm_ring R] [is_domain R] :
theorem valuation_ring.dvd_total {R : Type u_1} [comm_ring R] [is_domain R] [h : valuation_ring R] (x y : R) :
x y y x
theorem valuation_ring.unique_irreducible {R : Type u_1} [comm_ring R] [is_domain R] ⦃p q : R⦄ (hp : irreducible p) (hq : irreducible q) :
q
theorem valuation_ring.iff_is_integer_or_is_integer (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] :
∀ (x : K),
theorem valuation_ring.is_integer_or_is_integer (R : Type u_1) [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] [h : valuation_ring R] (x : K) :
@[protected, instance]
def valuation_ring.is_bezout {R : Type u_1} [comm_ring R] [is_domain R]  :
@[protected]
theorem valuation_ring.tfae (R : Type u) [comm_ring R] [is_domain R] :
, ∀ (x : , , , , .tfae
theorem function.surjective.valuation_ring {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] (f : R →+* S) (hf : function.surjective f) :
theorem valuation_ring.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [comm_ring 𝒪] [is_domain 𝒪] [field K] [ K] (v : Γ) (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.