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.

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.

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

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

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

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

      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' := }
      Instances For
        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
        Instances For
          @[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) :
          @[instance 100]
          Equations
          • =
          Equations
          theorem ValuationRing.iff_dvd_total {R : Type u_1} [CommRing R] [IsDomain R] :
          ValuationRing R IsTotal R fun (x x_1 : R) => x x_1
          theorem ValuationRing.iff_ideal_total {R : Type u_1} [CommRing R] [IsDomain R] :
          ValuationRing R IsTotal (Ideal R) fun (x x_1 : Ideal R) => x x_1
          theorem ValuationRing.dvd_total {R : Type u_1} [CommRing R] [IsDomain R] [h : ValuationRing R] (x : R) (y : R) :
          x y y x
          theorem ValuationRing.unique_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] ⦃p : R ⦃q : R (hp : Irreducible p) (hq : Irreducible q) :
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          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 (x x_1 : R) => x x_1, IsTotal (Ideal R) fun (x x_1 : Ideal R) => x x_1, LocalRing R IsBezout R].TFAE
          theorem ValuationRing.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [CommRing 𝒪] [IsDomain 𝒪] [Field K] [Algebra 𝒪 K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (hh : v.Integers 𝒪) :

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

          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]

          A field is a valuation ring.

          Equations
          • =
          @[instance 100]

          A DVR is a valuation ring.

          Equations
          • =