# Documentation

Mathlib.RingTheory.Valuation.ValuationRing

# 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: [CommRing A] [IsDomain A] [ValuationRing A] [Field K] [Algebra A K] [IsFractionRing 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 algebraMap A K agrees with (Valuation A K).integer.

We also provide the equivalence of the following notions for a domain R in ValuationRing.tFAE.

1. R is a valuation ring.
2. For each x : FractionRing 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 ValuationRing (A : Type u) [] [] :
• cond' : ∀ (a b : A), c, a * c = b b * c = a

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

Instances
theorem ValuationRing.cond {A : Type u} [] [] [] (a : A) (b : A) :
c, a * c = b b * c = a
def ValuationRing.ValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :

The value group of the valuation ring A. Note: this is actually a group with zero.

Instances For
instance ValuationRing.instInhabitedValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
instance ValuationRing.instLEValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
instance ValuationRing.instZeroValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
instance ValuationRing.instOneValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
instance ValuationRing.instMulValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
instance ValuationRing.instInvValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
theorem ValuationRing.le_total (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] (a : ) (b : ) :
a b b a
noncomputable instance ValuationRing.instLinearOrderValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
noncomputable instance ValuationRing.linearOrderedCommGroupWithZero (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
def ValuationRing.valuation (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :

Any valuation ring induces a valuation on its fraction field.

Instances For
theorem ValuationRing.mem_integer_iff (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] (x : K) :
a, ↑() a = x
noncomputable def ValuationRing.equivInteger (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
A ≃+* { x // }

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

Instances For
@[simp]
theorem ValuationRing.coe_equivInteger_apply (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] (a : A) :
↑(↑() a) = ↑() a
theorem ValuationRing.range_algebraMap_eq (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
instance ValuationRing.localRing (A : Type u) [] [] [] :
theorem ValuationRing.iff_dvd_total {R : Type u_1} [] [] :
IsTotal R fun x x_1 => x x_1
theorem ValuationRing.iff_ideal_total {R : Type u_1} [] [] :
IsTotal () fun x x_1 => x x_1
theorem ValuationRing.dvd_total {R : Type u_1} [] [] [h : ] (x : R) (y : R) :
x y y x
theorem ValuationRing.unique_irreducible {R : Type u_1} [] [] [] ⦃p : R ⦃q : R (hp : ) (hq : ) :
theorem ValuationRing.iff_isInteger_or_isInteger (R : Type u_1) [] [] (K : Type u_2) [] [Algebra R K] [] :
∀ (x : K),
theorem ValuationRing.isInteger_or_isInteger (R : Type u_1) [] [] {K : Type u_2} [] [Algebra R K] [] [h : ] (x : K) :
instance ValuationRing.instIsBezout {R : Type u_1} [] [] [] :
theorem ValuationRing.tFAE (R : Type u) [] [] :
List.TFAE [, ∀ (x : ), , IsTotal R fun x x_1 => x x_1, IsTotal () fun x x_1 => x x_1, ]
theorem Function.Surjective.valuationRing {R : Type u_1} {S : Type u_2} [] [] [] [] [] (f : R →+* S) (hf : ) :
theorem ValuationRing.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [] [] [] [Algebra 𝒪 K] (v : ) (hh : ) :

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

instance ValuationRing.of_field (K : Type u) [] :

A field is a valuation ring.

A DVR is a valuation ring.