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.

We also show that, given a valuation v on a field K, the ring of valuation integers is a valuation ring and K is the fraction field of this ring.

Implementation details

The Mathlib definition of a valuation ring requires IsDomain A even though the condition does not mention zero divisors. Thus, there is a technical PreValuationRing A that is defined in further generality that can be used in places where the ring cannot be a domain. The ValuationRing class is kept to be in sync with the literature.

class PreValuationRing (A : Type u) [Mul A] : Prop

A magma is called a PreValuationRing 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

theorem PreValuationRing.cond' {A : Type u} : ∀ {inst : Mul A} [self : PreValuationRing A] (a b : A), ∃ (c : A), a * c = b ∨ b * c = a

theorem PreValuationRing.cond {A : Type u} [Mul A] [PreValuationRing A] (a : A) (b : A) : ∃ (c : A), a * c = b ∨ b * c = a

class ValuationRing (A : Type u) [CommRing A] [IsDomain A] extends PreValuationRing : Prop

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

theorem ValuationRing.cond {A : Type u} [CommRing A] [IsDomain A] [ValuationRing A] (a : A) (b : A) : ∃ (c : A), a * c = b ∨ b * c = a

def ValuationRing.ValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : Type v

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

Equations

• ValuationRing.ValueGroup A K = Quotient (MulAction.orbitRel Aˣ K)

instance ValuationRing.instInhabitedValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : Inhabited (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instInhabitedValueGroup A K = { default := Quotient.mk'' 0 }

instance ValuationRing.instLEValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : LE (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instLEValueGroup A K = { le := fun (x y : ValuationRing.ValueGroup A K) => Quotient.liftOn₂' x y (fun (a b : K) => ∃ (c : A), c • b = a) ⋯ }

instance ValuationRing.instZeroValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : Zero (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instZeroValueGroup A K = { zero := Quotient.mk'' 0 }

instance ValuationRing.instOneValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : One (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instOneValueGroup A K = { one := Quotient.mk'' 1 }

instance ValuationRing.instMulValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : Mul (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instMulValueGroup A K = { mul := fun (x y : ValuationRing.ValueGroup A K) => Quotient.liftOn₂' x y (fun (a b : K) => Quotient.mk'' (a * b)) ⋯ }

instance ValuationRing.instInvValueGroup (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] : Inv (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.instInvValueGroup A K = { inv := fun (x : ValuationRing.ValueGroup A K) => Quotient.liftOn' x (fun (a : K) => Quotient.mk'' a⁻¹) ⋯ }

theorem ValuationRing.le_total (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] (a : ValuationRing.ValueGroup A K) (b : ValuationRing.ValueGroup A K) : a ≤ b ∨ b ≤ a

noncomputable instance ValuationRing.linearOrder (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] : LinearOrder (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.linearOrder A K = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

noncomputable instance ValuationRing.linearOrderedCommGroupWithZero (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] : LinearOrderedCommGroupWithZero (ValuationRing.ValueGroup A K)

Equations

• ValuationRing.linearOrderedCommGroupWithZero A K = LinearOrderedCommGroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

def ValuationRing.valuation (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] : Valuation K (ValuationRing.ValueGroup A K)

Any valuation ring induces a valuation on its fraction field.

Equations

• ValuationRing.valuation A K = { toFun := Quotient.mk'', map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

theorem ValuationRing.mem_integer_iff (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] (x : K) : x ∈ (ValuationRing.valuation A K).integer ↔ ∃ (a : A), (algebraMap A K) a = x

noncomputable def ValuationRing.equivInteger (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] : A ≃+* ↥(ValuationRing.valuation A K).integer

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

Equations

• ValuationRing.equivInteger A K = RingEquiv.ofBijective (let_fun this := { toFun := fun (a : A) => ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }; this) ⋯

@[simp]

theorem ValuationRing.coe_equivInteger_apply (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] (a : A) : ↑((ValuationRing.equivInteger A K) a) = (algebraMap A K) a

theorem ValuationRing.range_algebraMap_eq (A : Type u) [CommRing A] (K : Type v) [Field K] [Algebra A K] [IsDomain A] [ValuationRing A] [IsFractionRing A K] : (ValuationRing.valuation A K).integer = (algebraMap A K).range

@[instance 100]

instance ValuationRing.localRing (A : Type u) [CommRing A] [Nontrivial A] [PreValuationRing A] : LocalRing A

Equations

• ⋯ = ⋯

instance ValuationRing.instLinearOrderIdealOfDecidableRelLe (A : Type u) [CommRing A] [PreValuationRing A] [DecidableRel fun (x1 x2 : Ideal A) => x1 ≤ x2] : LinearOrder (Ideal A)

Equations

• ValuationRing.instLinearOrderIdealOfDecidableRelLe A = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

theorem PreValuationRing.iff_dvd_total {R : Type u_1} [Monoid R] : PreValuationRing R ↔ IsTotal R fun (x1 x2 : R) => x1 ∣ x2

theorem PreValuationRing.iff_ideal_total {R : Type u_1} [CommRing R] : PreValuationRing R ↔ IsTotal (Ideal R) fun (x1 x2 : Ideal R) => x1 ≤ x2

theorem ValuationRing.dvd_total {R : Type u_1} [Monoid R] [h : PreValuationRing R] (x : R) (y : R) : x ∣ y ∨ y ∣ x

theorem ValuationRing.iff_dvd_total {R : Type u_1} [CommRing R] [IsDomain R] : ValuationRing R ↔ IsTotal R fun (x1 x2 : R) => x1 ∣ x2

theorem ValuationRing.iff_ideal_total {R : Type u_1} [CommRing R] [IsDomain R] : ValuationRing R ↔ IsTotal (Ideal R) fun (x1 x2 : Ideal R) => x1 ≤ x2

theorem ValuationRing.unique_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] ⦃p : R⦄ ⦃q : R⦄ (hp : Irreducible p) (hq : Irreducible q) : Associated p q

theorem ValuationRing.iff_isInteger_or_isInteger (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

theorem ValuationRing.isInteger_or_isInteger (R : Type u_1) [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [h : ValuationRing R] (x : K) : IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

@[instance 100]

instance ValuationRing.instIsBezout {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] : IsBezout R

Equations

• ⋯ = ⋯

@[instance 100]

instance ValuationRing.instOfLocalRingOfIsBezout {R : Type u_1} [CommRing R] [IsDomain R] [LocalRing R] [IsBezout R] : ValuationRing R

Equations

• ⋯ = ⋯

theorem ValuationRing.iff_local_bezout_domain {R : Type u_1} [CommRing R] [IsDomain R] : ValuationRing R ↔ LocalRing R ∧ IsBezout R

theorem ValuationRing.TFAE (R : Type u) [CommRing R] [IsDomain R] : [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹, IsTotal R fun (x1 x2 : R) => x1 ∣ x2, IsTotal (Ideal R) fun (x1 x2 : Ideal R) => x1 ≤ x2, LocalRing R ∧ IsBezout R].TFAE

theorem Function.Surjective.preValuationRing {R : Type u_1} {S : Type u_2} [Mul R] [PreValuationRing R] [Mul S] (f : R →ₙ* S) (hf : Function.Surjective ⇑f) : PreValuationRing S

theorem Function.Surjective.valuationRing {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [ValuationRing R] [CommRing S] [IsDomain S] (f : R →+* S) (hf : Function.Surjective ⇑f) : ValuationRing S

theorem ValuationRing.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [CommRing 𝒪] [IsDomain 𝒪] [Field K] [Algebra 𝒪 K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (hh : v.Integers 𝒪) : ValuationRing 𝒪

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

instance ValuationRing.instValuationRingInteger {K : Type v} {Γ : Type w} [Field K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) : ValuationRing ↥v.integer

Equations

• ⋯ = ⋯

theorem ValuationRing.isFractionRing_iff {𝒪 : Type u} {K : Type v} [CommRing 𝒪] [IsDomain 𝒪] [Field K] [Algebra 𝒪 K] [ValuationRing 𝒪] : IsFractionRing 𝒪 K ↔ (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)

instance ValuationRing.instIsFractionRingInteger {K : Type v} {Γ : Type w} [Field K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) : IsFractionRing (↥v.integer) K

Equations

• ⋯ = ⋯

@[instance 100]

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

A field is a valuation ring.

Equations

• ⋯ = ⋯