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} [Mul A] [PreValuationRing A] (a b : A) : ∃ (c : A), a * c = b ∨ b * c = a

class ValuationRing (A : Type u) [CommRing A] [IsDomain A] extends PreValuationRing A : 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.

• cond' (a b : A) : ∃ (c : A), a * c = b ∨ b * c = a

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

An abbreviation for PreValuationRing.cond which should save some writing.

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.

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

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

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

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

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

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

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

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 b : 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 (ValueGroup A K)

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

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 (ValueGroup A K)

noncomputable 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 (ValueGroup A K)

Any valuation ring induces a valuation on its fraction field.

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 ∈ (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 ≃+* ↥(valuation A K).integer

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

@[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) : ↑((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] : (valuation A K).integer = (algebraMap A K).range

@[instance 100]

instance ValuationRing.isLocalRing (A : Type u) [CommRing A] [Nontrivial A] [PreValuationRing A] : IsLocalRing A

instance ValuationRing.le_total_ideal (A : Type u) [CommRing A] [PreValuationRing A] : Std.Total fun (x1 x2 : Ideal A) => x1 ≤ x2

instance ValuationRing.instLinearOrderIdealOfDecidableLE (A : Type u) [CommRing A] [PreValuationRing A] [DecidableLE (Ideal A)] : LinearOrder (Ideal A)

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

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

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

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

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

theorem ValuationRing.unique_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [PreValuationRing R] ⦃p 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

@[instance 100]

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

theorem ValuationRing.iff_local_bezout_domain {R : Type u_1} [CommRing R] [IsDomain R] : ValuationRing R ↔ IsLocalRing 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⁻¹, Std.Total fun (x1 x2 : R) => x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) => x1 ≤ x2, IsLocalRing 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 : Surjective ⇑f) : PreValuationRing S

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

theorem isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective {𝒪 : Type u} {K : Type v} [CommRing 𝒪] [Field K] [Algebra 𝒪 K] (h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) (hinj : Function.Injective ⇑(algebraMap 𝒪 K)) : IsFractionRing 𝒪 K

theorem Valuation.Integers.isFractionRing {𝒪 : Type u} {K : Type v} {Γ : Type w} [CommRing 𝒪] [Field K] [Algebra 𝒪 K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation K Γ} (hv : v.Integers 𝒪) : IsFractionRing 𝒪 K

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

theorem ValuationRing.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [CommRing 𝒪] [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

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

@[instance 100]

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

A field is a valuation ring.