# 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) [] [] :

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

• cond' : ∀ (a b : A), ∃ (c : A), a * c = b b * c = a
Instances
theorem ValuationRing.cond' {A : Type u} [] [] [self : ] (a : A) (b : A) :
∃ (c : A), a * c = b b * c = a
theorem ValuationRing.cond {A : Type u} [] [] [] (a : A) (b : A) :
∃ (c : A), 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.

Equations
Instances For
instance ValuationRing.instInhabitedValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
• = { default := }
instance ValuationRing.instLEValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
instance ValuationRing.instZeroValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
• = { zero := }
instance ValuationRing.instOneValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
• = { one := }
instance ValuationRing.instMulValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
instance ValuationRing.instInvValueGroup (A : Type u) [] (K : Type v) [] [Algebra A K] :
Equations
theorem ValuationRing.le_total (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] (a : ) (b : ) :
a b b a
noncomputable instance ValuationRing.linearOrder (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
Equations
• = LinearOrder.mk inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE
noncomputable instance ValuationRing.linearOrderedCommGroupWithZero (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
Equations
def ValuationRing.valuation (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :

Any valuation ring induces a valuation on its fraction field.

Equations
• = { toFun := Quotient.mk'', map_zero' := , map_one' := , map_mul' := , map_add_le_max' := }
Instances For
theorem ValuationRing.mem_integer_iff (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] (x : K) :
x ().integer ∃ (a : A), () a = x
noncomputable def ValuationRing.equivInteger (A : Type u) [] (K : Type v) [] [Algebra A K] [] [] [] :
A ≃+* ().integer

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

Equations
• = RingEquiv.ofBijective (let_fun this := { toFun := fun (a : A) => () a, , map_mul' := , map_zero' := , map_add' := }; this)
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] [] [] [] :
().integer = ().range
@[instance 100]
instance ValuationRing.localRing (A : Type u) [] [] [] :
Equations
• =
instance ValuationRing.instLinearOrderIdealOfDecidableRelLe (A : Type u) [] [] [] [DecidableRel fun (x x_1 : ) => x x_1] :
Equations
• = let __src := inferInstance; LinearOrder.mk inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE
theorem ValuationRing.iff_dvd_total {R : Type u_1} [] [] :
IsTotal R fun (x x_1 : R) => 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 100]
instance ValuationRing.instIsBezout {R : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance ValuationRing.instOfLocalRingOfIsBezout {R : Type u_1} [] [] [] [] :
Equations
• =
theorem ValuationRing.tFAE (R : Type u) [] [] :
[, ∀ (x : ), , IsTotal R fun (x x_1 : R) => x x_1, IsTotal () fun (x x_1 : ) => x x_1, ].TFAE
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 : v.Integers 𝒪) :

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

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

A field is a valuation ring.

Equations
• =
@[instance 100]

A DVR is a valuation ring.

Equations
• =