mathlib3 documentation

ring_theory.valuation.valuation_ring

Valuation Rings #

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

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

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]
Equations
@[protected, instance]
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) :

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

Equations
@[protected, instance]
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] [valuation_ring R] ⦃p q : R⦄ (hp : irreducible p) (hq : irreducible q) :
@[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]

A field is a valuation ring.

@[protected, instance]

A DVR is a valuation ring.