# 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” ([Wed19]).

The definition of a valuation we use here is Definition 1.22 of [Wed19]. 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:

• v 0 = 0
• ∀ x y, v (x + y) ≤ max (v x) (v y)

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 [Wed19] 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 [Wed19] as the definition of equivalence.

## Main definitions #

• Valuation R Γ₀, the type of valuations on R with values in Γ₀

• Valuation.IsEquiv, the heterogeneous equivalence relation on valuations

• Valuation.supp, the support of a valuation

• AddValuation R Γ₀, the type of additive valuations on R with values in a linearly ordered additive commutative group with a top element, Γ₀.

## Implementation Details #

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

## Notation #

In the DiscreteValuation locale:

• ℕₘ₀ is a shorthand for WithZero (Multiplicative ℕ)
• ℤₘ₀ is a shorthand for WithZero (Multiplicative ℤ)

## TODO #

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

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

The type of Γ₀-valued valuations on R.

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

• toFun : RΓ₀
• map_zero' : (↑self.toMonoidWithZeroHom).toFun 0 = 0
• map_one' : (↑self.toMonoidWithZeroHom).toFun 1 = 1
• map_mul' : ∀ (x y : R), (↑self.toMonoidWithZeroHom).toFun (x * y) = (↑self.toMonoidWithZeroHom).toFun x * (↑self.toMonoidWithZeroHom).toFun y
• map_add_le_max' : ∀ (x y : R), (↑self.toMonoidWithZeroHom).toFun (x + y) max ((↑self.toMonoidWithZeroHom).toFun x) ((↑self.toMonoidWithZeroHom).toFun y)

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

Instances For
theorem Valuation.map_add_le_max' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (self : Valuation R Γ₀) (x : R) (y : R) :
(↑self.toMonoidWithZeroHom).toFun (x + y) max ((↑self.toMonoidWithZeroHom).toFun x) ((↑self.toMonoidWithZeroHom).toFun y)

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

class ValuationClass (F : Type u_7) (R : outParam (Type u_5)) (Γ₀ : outParam (Type u_6)) [Ring R] [FunLike F R Γ₀] extends :

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

You should also extend this typeclass when you extend Valuation.

• 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

Instances
theorem ValuationClass.map_add_le_max {F : Type u_7} {R : outParam (Type u_5)} {Γ₀ : outParam (Type u_6)} [Ring R] [FunLike F R Γ₀] [self : ValuationClass F R Γ₀] (f : F) (x : R) (y : R) :
f (x + y) max (f x) (f y)

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

instance instCoeTCValuationOfValuationClass (F : Type u_2) (R : Type u_3) (Γ₀ : Type u_4) [Ring R] [FunLike F R Γ₀] [ValuationClass F R Γ₀] :
CoeTC F (Valuation R Γ₀)
Equations
• = { coe := fun (f : F) => { toFun := f, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := } }
instance Valuation.instFunLike {R : Type u_3} {Γ₀ : Type u_4} [Ring R] :
FunLike (Valuation R Γ₀) R Γ₀
Equations
• Valuation.instFunLike = { coe := fun (f : Valuation R Γ₀) => (↑f.toMonoidWithZeroHom).toFun, coe_injective' := }
instance Valuation.instValuationClass {R : Type u_3} {Γ₀ : Type u_4} [Ring R] :
ValuationClass (Valuation R Γ₀) R Γ₀
Equations
• =
@[simp]
theorem Valuation.coe_mk {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (f : R →*₀ Γ₀) (h : ∀ (x y : R), (↑f).toFun (x + y) max ((↑f).toFun x) ((↑f).toFun y)) :
{ toMonoidWithZeroHom := f, map_add_le_max' := h } = f
theorem Valuation.toFun_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) :
(↑v.toMonoidWithZeroHom).toFun = v
@[simp]
theorem Valuation.toMonoidWithZeroHom_coe_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) :
v.toMonoidWithZeroHom = v
theorem Valuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀} :
v₁ = v₂ ∀ (r : R), v₁ r = v₂ r
theorem Valuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {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] (v : Valuation R Γ₀) :
v = v
theorem Valuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) :
v 0 = 0
theorem Valuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) :
v 1 = 1
theorem Valuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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] (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] (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] (v : Valuation R Γ₀) {x : R} {y : R} {g : Γ₀} (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] (v : Valuation R Γ₀) {x : R} {y : R} {g : Γ₀} (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] (v : Valuation R Γ₀) {ι : Type u_7} {s : } {f : ιR} {g : Γ₀} (hf : is, v (f i) g) :
v (∑ is, f i) g
theorem Valuation.map_sum_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) {ι : Type u_7} {s : } {f : ιR} {g : Γ₀} (hg : g 0) (hf : is, v (f i) < g) :
v (∑ is, f i) < g
theorem Valuation.map_sum_lt' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) {ι : Type u_7} {s : } {f : ιR} {g : Γ₀} (hg : 0 < g) (hf : is, v (f i) < g) :
v (∑ is, f i) < g
theorem Valuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) (x : R) (n : ) :
v (x ^ n) = v x ^ n
def Valuation.toPreorder {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) :

A valuation gives a preorder on the underlying ring.

Equations
• v.toPreorder =
Instances For
theorem Valuation.zero_iff {K : Type u_1} [] {Γ₀ : Type u_4} [] (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} [] {Γ₀ : Type u_4} [] (v : Valuation K Γ₀) {x : K} :
v x 0 x 0
theorem Valuation.unit_map_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) (u : Rˣ) :
((Units.map v) u) = v u
theorem Valuation.ne_zero_of_unit {K : Type u_1} [] {Γ₀ : Type u_4} [] (v : Valuation K Γ₀) (x : Kˣ) :
v x 0
theorem Valuation.ne_zero_of_isUnit {K : Type u_1} [] {Γ₀ : Type u_4} [] (v : Valuation K Γ₀) (x : K) (hx : ) :
v x 0
def Valuation.comap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {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
• = { toFun := v f, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := }
Instances For
@[simp]
theorem Valuation.comap_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {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] (v : Valuation R Γ₀) :
= v
theorem Valuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) {S₁ : Type u_7} {S₂ : Type u_8} [Ring S₁] [Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
Valuation.comap (g.comp f) v =
def Valuation.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (v : Valuation R Γ₀) :
Valuation R Γ'₀

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

Equations
• Valuation.map f hf v = { toFun := f v, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := }
Instances For
def Valuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] (v₁ : Valuation R Γ₀) (v₂ : Valuation R Γ'₀) :

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

Equations
• v₁.IsEquiv v₂ = ∀ (r s : R), v₁ r v₁ s v₂ r v₂ s
Instances For
@[simp]
theorem Valuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) (x : R) :
v (-x) = v x
theorem Valuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) (x : R) (y : R) :
v (x - y) = v (y - x)
theorem Valuation.map_inv {Γ₀ : Type u_4} {R : Type u_7} [] (v : Valuation R Γ₀) (x : R) :
v x⁻¹ = (v x)⁻¹
theorem Valuation.map_div {Γ₀ : Type u_4} {R : Type u_7} [] (v : Valuation R Γ₀) (x : R) (y : R) :
v (x / y) = v x / v y
theorem Valuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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] (v : Valuation R Γ₀) {x : R} {y : R} {g : Γ₀} (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] (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] (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] (v : Valuation R Γ₀) {x : R} {y : R} (h : v y < v x) :
v (x + y) = v x
theorem Valuation.map_sub_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) {x : R} {y : R} (h : v x < v y) :
v (x - y) = v y
theorem Valuation.map_sub_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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] (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] (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] (v : Valuation R Γ₀) {x : R} (h : v x < 1) :
v (1 - x) = 1
theorem Valuation.one_lt_val_iff {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) {x : K} (h : x 0) :
1 < v x v x⁻¹ < 1
theorem Valuation.one_le_val_iff {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) {x : K} (h : x 0) :
1 v x v x⁻¹ 1
theorem Valuation.val_lt_one_iff {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) {x : K} (h : x 0) :
v x < 1 1 < v x⁻¹
theorem Valuation.val_le_one_iff {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) {x : K} (h : x 0) :
v x 1 1 v x⁻¹
theorem Valuation.val_eq_one_iff {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) {x : K} :
v x = 1 v x⁻¹ = 1
theorem Valuation.val_le_one_or_val_inv_lt_one {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) (x : K) :
v x 1 v x⁻¹ < 1
theorem Valuation.val_le_one_or_val_inv_le_one {K : Type u_1} [] {Γ₀ : Type u_4} (v : Valuation K Γ₀) (x : K) :
v x 1 v x⁻¹ 1

This theorem is a weaker version of Valuation.val_le_one_or_val_inv_lt_one, but more symmetric in x and x⁻¹.

def Valuation.ltAddSubgroup {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

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

Equations
• v.ltAddSubgroup γ = { carrier := {x : R | v x < γ}, add_mem' := , zero_mem' := , neg_mem' := }
Instances For
theorem Valuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v : Valuation R Γ₀} :
v.IsEquiv v
theorem Valuation.IsEquiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv v₂) :
v₂.IsEquiv v₁
theorem Valuation.IsEquiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [Ring R] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {v₃ : Valuation R Γ''₀} (h₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) :
v₁.IsEquiv v₃
theorem Valuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v : Valuation R Γ₀} {v' : Valuation R Γ₀} (h : v = v') :
v.IsEquiv v'
theorem Valuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v : Valuation R Γ₀} {v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (inf : ) (h : v.IsEquiv v') :
(Valuation.map f hf v).IsEquiv (Valuation.map f hf v')
theorem Valuation.IsEquiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {S : Type u_7} [Ring S] (f : S →+* R) (h : v₁.IsEquiv v₂) :
(Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)

comap preserves equivalence.

theorem Valuation.IsEquiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv 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] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv 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} [Ring R] {v : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : ) :
(Valuation.map f v).IsEquiv v
theorem Valuation.isEquiv_of_val_le_one {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) (h : ∀ {x : K}, v x 1 v' x 1) :
v.IsEquiv v'
theorem Valuation.isEquiv_iff_val_le_one {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
v.IsEquiv v' ∀ {x : K}, v x 1 v' x 1
theorem Valuation.isEquiv_iff_val_eq_one {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
v.IsEquiv v' ∀ {x : K}, v x = 1 v' x = 1
theorem Valuation.isEquiv_iff_val_lt_one {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
v.IsEquiv v' ∀ {x : K}, v x < 1 v' x < 1
theorem Valuation.isEquiv_iff_val_sub_one_lt_one {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
v.IsEquiv v' ∀ {x : K}, v (x - 1) < 1 v' (x - 1) < 1
theorem Valuation.isEquiv_tfae {K : Type u_1} [] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
[v.IsEquiv 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].TFAE
def Valuation.supp {R : Type u_3} {Γ₀ : Type u_4} [] (v : Valuation R Γ₀) :

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

Equations
• v.supp = { carrier := {x : R | v x = 0}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem Valuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [] (v : Valuation R Γ₀) (x : R) :
x v.supp v x = 0
instance Valuation.instIsPrimeSuppOfNontrivialOfNoZeroDivisors {R : Type u_3} {Γ₀ : Type u_4} [] (v : Valuation R Γ₀) [] [] :
v.supp.IsPrime

The support of a valuation is a prime ideal.

Equations
• =
theorem Valuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [] (v : Valuation R Γ₀) (a : R) {s : R} (h : s v.supp) :
v (a + s) = v a
theorem Valuation.comap_supp {R : Type u_3} {Γ₀ : Type u_4} [] (v : Valuation R Γ₀) {S : Type u_7} [] (f : S →+* R) :
(Valuation.comap f v).supp = Ideal.comap f v.supp
def AddValuation (R : Type u_3) [Ring R] (Γ₀ : Type u_4) :
Type (max u_3 u_4)

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

Equations
Instances For
instance AddValuation.instFunLike (R : Type u_6) (Γ₀ : Type u_7) [Ring R] :
FunLike (AddValuation R Γ₀) R Γ₀

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

Equations
• = { coe := fun (v : AddValuation R Γ₀) => (↑v.toMonoidWithZeroHom).toFun, coe_injective' := }
def AddValuation.of {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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) :

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

Equations
• AddValuation.of f h0 h1 hadd hmul = { 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] (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} :
def AddValuation.valuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) :

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

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

A helper function for Lean to inferring types correctly

Equations
• v.asFun = v
Instances For
@[simp]
theorem AddValuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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] (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] (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] (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] (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] (v : AddValuation R Γ₀) {ι : Type u_6} {s : } {f : ιR} {g : Γ₀} (hf : is, g v (f i)) :
g v (∑ is, f i)
theorem AddValuation.map_lt_sum {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {ι : Type u_6} {s : } {f : ιR} {g : Γ₀} (hg : g ) (hf : is, g < v (f i)) :
g < v (∑ is, f i)
theorem AddValuation.map_lt_sum' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {ι : Type u_6} {s : } {f : ιR} {g : Γ₀} (hg : g < ) (hf : is, g < v (f i)) :
g < v (∑ is, f i)
@[simp]
theorem AddValuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) (x : R) (n : ) :
v (x ^ n) = n v x
theorem AddValuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ₀} :
v₁ = v₂ ∀ (r : R), v₁ r = v₂ r
theorem AddValuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
v₁ = v₂
def AddValuation.toPreorder {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) :

A valuation gives a preorder on the underlying ring.

Equations
• v.toPreorder =
Instances For
@[simp]
theorem AddValuation.top_iff {K : Type u_1} [] {Γ₀ : Type u_4} [] (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} [] {Γ₀ : Type u_4} [] (v : AddValuation K Γ₀) {x : K} :
v x x 0
def AddValuation.comap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {S : Type u_6} [Ring S] (f : S →+* R) (v : AddValuation R Γ₀) :

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] (v : AddValuation R Γ₀) :
= v
theorem AddValuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (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] (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : Monotone f) (v : AddValuation R Γ₀) :

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

Equations
Instances For
def AddValuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] (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
• v₁.IsEquiv v₂ =
Instances For
@[simp]
theorem AddValuation.map_inv {K : Type u_1} [] {Γ₀ : Type u_4} (v : AddValuation K Γ₀) {x : K} :
v x⁻¹ = -v x
@[simp]
theorem AddValuation.map_div {K : Type u_1} [] {Γ₀ : Type u_4} (v : AddValuation K Γ₀) {x : K} {y : K} :
v (x / y) = v x - v y
@[simp]
theorem AddValuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) (x : R) :
v (-x) = v x
theorem AddValuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [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} [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} [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} [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_add_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (h : v x < v y) :
v (x + y) = v x
theorem AddValuation.map_add_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (hx : v y < v x) :
v (x + y) = v y
theorem AddValuation.map_sub_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (hx : v x < v y) :
v (x - y) = v x
theorem AddValuation.map_sub_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (hx : v y < v x) :
v (x - y) = v y
theorem AddValuation.map_eq_of_lt_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] (v : AddValuation R Γ₀) {x : R} {y : R} (h : v x < v (y - x)) :
v y = v x
theorem AddValuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v : AddValuation R Γ₀} :
v.IsEquiv v
theorem AddValuation.IsEquiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : v₁.IsEquiv v₂) :
v₂.IsEquiv v₁
theorem AddValuation.IsEquiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {Γ''₀ : Type u_6} {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} {v₃ : AddValuation R Γ''₀} (h₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) :
v₁.IsEquiv v₃
theorem AddValuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] {v : AddValuation R Γ₀} {v' : AddValuation R Γ₀} (h : v = v') :
v.IsEquiv v'
theorem AddValuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v : AddValuation R Γ₀} {v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : Monotone f) (inf : ) (h : v.IsEquiv v') :
theorem AddValuation.IsEquiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} {S : Type u_7} [Ring S] (f : S →+* R) (h : v₁.IsEquiv v₂) :

comap preserves equivalence.

theorem AddValuation.IsEquiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : v₁.IsEquiv 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} [Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀} (h : v₁.IsEquiv v₂) {r : R} :
v₁ r v₂ r
def AddValuation.supp {R : Type u_3} {Γ₀ : Type u_4} [] (v : AddValuation R Γ₀) :

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

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

Notation for WithZero (Multiplicative ℕ)

Equations
Instances For

Notation for WithZero (Multiplicative ℤ)

Equations
Instances For