Documentation

Mathlib.RingTheory.Valuation.Basic

The basics of valuation theory. #

The basic theory of valuations (non-archimedean norms) on a commutative ring, following T. Wedhorn's unpublished notes “Adic Spaces” ([wedhorn_adic]).

The definition of a valuation we use here is Definition 1.22 of [wedhorn_adic]. A valuation on a ring R is a monoid homomorphism v to a linearly ordered commutative monoid with zero, that in addition satisfies the following two axioms:

Valuation R Γ₀is the type of valuations R → Γ₀, with a coercion to the underlying function. If v is a valuation from R to Γ₀ then the induced group homomorphism units(R) → Γ₀ is called unit_map v.

The equivalence "relation" IsEquiv v₁ v₂ : Prop defined in 1.27 of [wedhorn_adic] is not strictly speaking a relation, because v₁ : Valuation R Γ₁ and v₂ : Valuation R Γ₂ might not have the same type. This corresponds in ZFC to the set-theoretic difficulty that the class of all valuations (as Γ₀ varies) on a ring R is not a set. The "relation" is however reflexive, symmetric and transitive in the obvious sense. Note that we use 1.27(iii) of [wedhorn_adic] as the definition of equivalence.

Main definitions #

Implementation Details #

AddValuation R Γ₀ is implemented as Valuation R (Multiplicative Γ₀)ᵒᵈ.

Notation #

In the DiscreteValuation locale:

TODO #

If ever someone extends Valuation, we should fully comply to the FunLike by migrating the boilerplate lemmas to ValuationClass.

structure Valuation (R : Type u_3) (Γ₀ : Type u_4) [LinearOrderedCommMonoidWithZero Γ₀] [Ring R] extends MonoidWithZeroHom :
Type (max u_3 u_4)

The type of Γ₀-valued valuations on R.

When you extend this structure, make sure to extend ValuationClass.

Instances For
    class ValuationClass (F : Type u_7) (R : outParam (Type u_5)) (Γ₀ : outParam (Type u_6)) [LinearOrderedCommMonoidWithZero Γ₀] [Ring R] extends MonoidWithZeroHomClass :
    Type (max (max u_5 u_6) u_7)
    • coe : FRΓ₀
    • coe_injective' : Function.Injective FunLike.coe
    • map_mul : ∀ (f : F) (x y : R), f (x * y) = f x * f y
    • map_one : ∀ (f : F), f 1 = 1
    • map_zero : ∀ (f : F), f 0 = 0
    • map_add_le_max : ∀ (f : F) (x y : R), f (x + y) max (f x) (f y)

      The valuation of a a sum is less that the sum of the valuations

    ValuationClass F α β states that F is a type of valuations.

    You should also extend this typeclass when you extend Valuation.

    Instances
      instance instCoeTCValuation (F : Type u_2) (R : Type u_3) (Γ₀ : Type u_4) [LinearOrderedCommMonoidWithZero Γ₀] [Ring R] [ValuationClass F R Γ₀] :
      CoeTC F (Valuation R Γ₀)
      Equations
      • One or more equations did not get rendered due to their size.
      instance Valuation.instValuationClassValuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
      ValuationClass (Valuation R Γ₀) R Γ₀
      Equations
      • One or more equations did not get rendered due to their size.
      theorem Valuation.toFun_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
      v.toFun = v
      @[simp]
      theorem Valuation.toMonoidWithZeroHom_coe_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
      v.toMonoidWithZeroHom = v
      theorem Valuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
      v₁ = v₂
      @[simp]
      theorem Valuation.coe_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
      v = v
      theorem Valuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
      v 0 = 0
      theorem Valuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
      v 1 = 1
      theorem Valuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (y : R) :
      v (x * y) = v x * v y
      theorem Valuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (y : R) :
      v (x + y) max (v x) (v y)
      @[simp]
      theorem Valuation.map_add' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (y : R) :
      v (x + y) v x v (x + y) v y
      theorem Valuation.map_add_le {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} {g : (fun x => Γ₀) x} (hx : v x g) (hy : v y g) :
      v (x + y) g
      theorem Valuation.map_add_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} {g : (fun x => Γ₀) x} (hx : v x < g) (hy : v y < g) :
      v (x + y) < g
      theorem Valuation.map_sum_le {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {ι : Type u_7} {s : Finset ι} {f : ιR} {g : Γ₀} (hf : ∀ (i : ι), i sv (f i) g) :
      v (Finset.sum s fun i => f i) g
      theorem Valuation.map_sum_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {ι : Type u_7} {s : Finset ι} {f : ιR} {g : Γ₀} (hg : g 0) (hf : ∀ (i : ι), i sv (f i) < g) :
      v (Finset.sum s fun i => f i) < g
      theorem Valuation.map_sum_lt' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {ι : Type u_7} {s : Finset ι} {f : ιR} {g : Γ₀} (hg : 0 < g) (hf : ∀ (i : ι), i sv (f i) < g) :
      v (Finset.sum s fun i => f i) < g
      theorem Valuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (n : ) :
      v (x ^ n) = v x ^ n
      theorem Valuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀} :
      v₁ = v₂ ∀ (r : R), v₁ r = v₂ r

      Deprecated. Use FunLike.ext_iff.

      def Valuation.toPreorder {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :

      A valuation gives a preorder on the underlying ring.

      Equations
      Instances For
        theorem Valuation.zero_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K} :
        v x = 0 x = 0

        If v is a valuation on a division ring then v(x) = 0 iff x = 0.

        theorem Valuation.ne_zero_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K} :
        v x 0 x 0
        theorem Valuation.unit_map_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (u : Rˣ) :
        ↑(↑(Units.map v) u) = v u
        def Valuation.comap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {S : Type u_7} [Ring S] (f : S →+* R) (v : Valuation R Γ₀) :
        Valuation S Γ₀

        A ring homomorphism S → R induces a map Valuation R Γ₀ → Valuation S Γ₀.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Valuation.comap_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {S : Type u_7} [Ring S] (f : S →+* R) (v : Valuation R Γ₀) (s : S) :
          ↑(Valuation.comap f v) s = v (f s)
          @[simp]
          theorem Valuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
          theorem Valuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {S₁ : Type u_7} {S₂ : Type u_8} [Ring S₁] [Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
          def Valuation.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (v : Valuation R Γ₀) :
          Valuation R Γ'₀

          A -preserving group homomorphism Γ₀ → Γ'₀ induces a map Valuation R Γ₀ → Valuation R Γ'₀.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Valuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] (v₁ : Valuation R Γ₀) (v₂ : Valuation R Γ'₀) :

            Two valuations on R are defined to be equivalent if they induce the same preorder on R.

            Equations
            Instances For
              @[simp]
              theorem Valuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (x : R) :
              v (-x) = v x
              theorem Valuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (y : R) :
              v (x - y) = v (y - x)
              theorem Valuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (x : R) (y : R) :
              v (x - y) max (v x) (v y)
              theorem Valuation.map_sub_le {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} {g : (fun x => Γ₀) x} (hx : v x g) (hy : v y g) :
              v (x - y) g
              theorem Valuation.map_add_of_distinct_val {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} (h : v x v y) :
              v (x + y) = max (v x) (v y)
              theorem Valuation.map_add_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} (h : v x < v y) :
              v (x + y) = v y
              theorem Valuation.map_add_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} (h : v y < v x) :
              v (x + y) = v x
              theorem Valuation.map_eq_of_sub_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} {y : R} (h : v (y - x) < v x) :
              v y = v x
              theorem Valuation.map_one_add_of_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} (h : v x < 1) :
              v (1 + x) = 1
              theorem Valuation.map_one_sub_of_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {x : R} (h : v x < 1) :
              v (1 - x) = 1
              theorem Valuation.one_lt_val_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x : K} (h : x 0) :
              1 < v x v x⁻¹ < 1
              def Valuation.ltAddSubgroup {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

              The subgroup of elements whose valuation is less than a certain unit.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Valuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} :
                theorem Valuation.IsEquiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : Valuation.IsEquiv v₁ v₂) :
                theorem Valuation.IsEquiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ''₀] [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {v₃ : Valuation R Γ''₀} (h₁₂ : Valuation.IsEquiv v₁ v₂) (h₂₃ : Valuation.IsEquiv v₂ v₃) :
                theorem Valuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} {v' : Valuation R Γ₀} (h : v = v') :
                theorem Valuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} {v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (inf : Function.Injective f) (h : Valuation.IsEquiv v v') :
                theorem Valuation.IsEquiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {S : Type u_7} [Ring S] (f : S →+* R) (h : Valuation.IsEquiv v₁ v₂) :

                comap preserves equivalence.

                theorem Valuation.IsEquiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : Valuation.IsEquiv v₁ v₂) {r : R} {s : R} :
                v₁ r = v₁ s v₂ r = v₂ s
                theorem Valuation.IsEquiv.ne_zero {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : Valuation.IsEquiv v₁ v₂) {r : R} :
                v₁ r 0 v₂ r 0
                theorem Valuation.isEquiv_of_map_strictMono {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] [Ring R] {v : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : StrictMono f) :
                theorem Valuation.isEquiv_of_val_le_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) (h : ∀ {x : K}, v x 1 v' x 1) :
                theorem Valuation.isEquiv_iff_val_le_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
                Valuation.IsEquiv v v' ∀ {x : K}, v x 1 v' x 1
                theorem Valuation.isEquiv_iff_val_eq_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
                Valuation.IsEquiv v v' ∀ {x : K}, v x = 1 v' x = 1
                theorem Valuation.isEquiv_iff_val_lt_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
                Valuation.IsEquiv v v' ∀ {x : K}, v x < 1 v' x < 1
                theorem Valuation.isEquiv_iff_val_sub_one_lt_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
                Valuation.IsEquiv v v' ∀ {x : K}, v (x - 1) < 1 v' (x - 1) < 1
                theorem Valuation.isEquiv_tfae {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
                List.TFAE [Valuation.IsEquiv v v', ∀ {x : K}, v x 1 v' x 1, ∀ {x : K}, v x = 1 v' x = 1, ∀ {x : K}, v x < 1 v' x < 1, ∀ {x : K}, v (x - 1) < 1 v' (x - 1) < 1]
                def Valuation.supp {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :

                The support of a valuation v : R → Γ₀ is the ideal of R where v vanishes.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Valuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) :
                  x Valuation.supp v v x = 0
                  theorem Valuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (a : R) {s : R} (h : s Valuation.supp v) :
                  v (a + s) = v a
                  theorem Valuation.comap_supp {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {S : Type u_7} [CommRing S] (f : S →+* R) :
                  def AddValuation (R : Type u_3) [Ring R] (Γ₀ : Type u_4) [LinearOrderedAddCommMonoidWithTop Γ₀] :
                  Type (max u_3 u_4)

                  The type of Γ₀-valued additive valuations on R.

                  Equations
                  Instances For
                    instance AddValuation.instFunLikeAddValuation (R : Type u_6) (Γ₀ : Type u_7) [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
                    FunLike (AddValuation R Γ₀) R fun x => Γ₀

                    A valuation is coerced to the underlying function R → Γ₀.

                    Equations
                    def AddValuation.of {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (f : RΓ₀) (h0 : f 0 = ) (h1 : f 1 = 0) (hadd : ∀ (x y : R), min (f x) (f y) f (x + y)) (hmul : ∀ (x y : R), f (x * y) = f x + f y) :
                    AddValuation R Γ₀

                    An alternate constructor of AddValuation, that doesn't reference Multiplicative Γ₀ᵒᵈ

                    Equations
                    • AddValuation.of f h0 h1 hadd hmul = { toMonoidWithZeroHom := { toZeroHom := { toFun := f, map_zero' := h0 }, map_one' := h1, map_mul' := hmul }, map_add_le_max' := hadd }
                    Instances For
                      @[simp]
                      theorem AddValuation.of_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (f : RΓ₀) {h0 : f 0 = } {h1 : f 1 = 0} {hadd : ∀ (x y : R), min (f x) (f y) f (x + y)} {hmul : ∀ (x y : R), f (x * y) = f x + f y} {r : R} :
                      ↑(AddValuation.of f h0 h1 hadd hmul) r = f r
                      def AddValuation.valuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :

                      The Valuation associated to an AddValuation (useful if the latter is constructed using AddValuation.of).

                      Equations
                      Instances For
                        @[simp]
                        theorem AddValuation.valuation_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (r : R) :
                        ↑(AddValuation.valuation v) r = Multiplicative.ofAdd (OrderDual.toDual (v r))
                        @[simp]
                        theorem AddValuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
                        v 0 =
                        @[simp]
                        theorem AddValuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
                        v 1 = 0
                        def AddValuation.asFun {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
                        RΓ₀

                        A helper function for Lean to inferring types correctly

                        Equations
                        Instances For
                          @[simp]
                          theorem AddValuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x : R) (y : R) :
                          v (x * y) = v x + v y
                          theorem AddValuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x : R) (y : R) :
                          min (v x) (v y) v (x + y)
                          @[simp]
                          theorem AddValuation.map_add' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x : R) (y : R) :
                          v x v (x + y) v y v (x + y)
                          theorem AddValuation.map_le_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x : R} {y : R} {g : Γ₀} (hx : g v x) (hy : g v y) :
                          g v (x + y)
                          theorem AddValuation.map_lt_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x : R} {y : R} {g : Γ₀} (hx : g < v x) (hy : g < v y) :
                          g < v (x + y)
                          theorem AddValuation.map_le_sum {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {ι : Type u_6} {s : Finset ι} {f : ιR} {g : Γ₀} (hf : ∀ (i : ι), i sg v (f i)) :
                          g v (Finset.sum s fun i => f i)
                          theorem AddValuation.map_lt_sum {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {ι : Type u_6} {s : Finset ι} {f : ιR} {g : Γ₀} (hg : g ) (hf : ∀ (i : ι), i sg < v (f i)) :
                          g < v (Finset.sum s fun i => f i)
                          theorem AddValuation.map_lt_sum' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {ι : Type u_6} {s : Finset ι} {f : ιR} {g : Γ₀} (hg : g < ) (hf : ∀ (i : ι), i sg < v (f i)) :
                          g < v (Finset.sum s fun i => f i)
                          @[simp]
                          theorem AddValuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x : R) (n : ) :
                          v (x ^ n) = n v x
                          theorem AddValuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
                          v₁ = v₂
                          theorem AddValuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ₀} :
                          v₁ = v₂ ∀ (r : R), v₁ r = v₂ r
                          def AddValuation.toPreorder {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :

                          A valuation gives a preorder on the underlying ring.

                          Equations
                          Instances For
                            @[simp]
                            theorem AddValuation.top_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Nontrivial Γ₀] (v : AddValuation K Γ₀) {x : K} :
                            v x = x = 0

                            If v is an additive valuation on a division ring then v(x) = ⊤ iff x = 0.

                            theorem AddValuation.ne_top_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Nontrivial Γ₀] (v : AddValuation K Γ₀) {x : K} :
                            v x x 0
                            def AddValuation.comap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {S : Type u_6} [Ring S] (f : S →+* R) (v : AddValuation R Γ₀) :
                            AddValuation S Γ₀

                            A ring homomorphism S → R induces a map AddValuation R Γ₀ → AddValuation S Γ₀.

                            Equations
                            Instances For
                              @[simp]
                              theorem AddValuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
                              theorem AddValuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {S₁ : Type u_6} {S₂ : Type u_7} [Ring S₁] [Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
                              def AddValuation.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : Monotone f) (v : AddValuation R Γ₀) :
                              AddValuation R Γ'₀

                              A -preserving, -preserving group homomorphism Γ₀ → Γ'₀ induces a map AddValuation R Γ₀ → AddValuation R Γ'₀.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def AddValuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] (v₁ : AddValuation R Γ₀) (v₂ : AddValuation R Γ'₀) :

                                Two additive valuations on R are defined to be equivalent if they induce the same preorder on R.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AddValuation.map_inv {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] (v : AddValuation K Γ₀) {x : K} :
                                  v x⁻¹ = -v x
                                  @[simp]
                                  theorem AddValuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) (x : R) :
                                  v (-x) = v x
                                  theorem AddValuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) (x : R) (y : R) :
                                  v (x - y) = v (y - x)
                                  theorem AddValuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) (x : R) (y : R) :
                                  min (v x) (v y) v (x - y)
                                  theorem AddValuation.map_le_sub {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} {g : Γ₀} (hx : g v x) (hy : g v y) :
                                  g v (x - y)
                                  theorem AddValuation.map_add_of_distinct_val {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (h : v x v y) :
                                  v (x + y) = min (v x) (v y)
                                  theorem AddValuation.map_eq_of_lt_sub {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (h : v x < v (y - x)) :
                                  v y = v x
                                  theorem AddValuation.IsEquiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : AddValuation.IsEquiv v₁ v₂) :
                                  theorem AddValuation.IsEquiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {Γ''₀ : Type u_6} [LinearOrderedAddCommMonoidWithTop Γ''₀] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} {v₃ : AddValuation R Γ''₀} (h₁₂ : AddValuation.IsEquiv v₁ v₂) (h₂₃ : AddValuation.IsEquiv v₂ v₃) :
                                  theorem AddValuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Ring R] {v : AddValuation R Γ₀} {v' : AddValuation R Γ₀} (h : v = v') :
                                  theorem AddValuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v : AddValuation R Γ₀} {v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : Monotone f) (inf : Function.Injective f) (h : AddValuation.IsEquiv v v') :
                                  theorem AddValuation.IsEquiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} {S : Type u_7} [Ring S] (f : S →+* R) (h : AddValuation.IsEquiv v₁ v₂) :

                                  comap preserves equivalence.

                                  theorem AddValuation.IsEquiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : AddValuation.IsEquiv v₁ v₂) {r : R} {s : R} :
                                  v₁ r = v₁ s v₂ r = v₂ s
                                  theorem AddValuation.IsEquiv.ne_top {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : AddValuation.IsEquiv v₁ v₂) {r : R} :
                                  v₁ r v₂ r
                                  def AddValuation.supp {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) :

                                  The support of an additive valuation v : R → Γ₀ is the ideal of R where v x = ⊤

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem AddValuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) (x : R) :
                                    theorem AddValuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) (a : R) {s : R} (h : s AddValuation.supp v) :
                                    v (a + s) = v a

                                    Notation for WithZero (Multiplicative ℕ)

                                    Equations
                                    Instances For

                                      Notation for WithZero (Multiplicative ℤ)

                                      Equations
                                      Instances For