# mathlibdocumentation

ring_theory.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” ([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" is_equiv 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.

The support of a valuation v : valuation R Γ₀ is supp v. If J is an ideal of R with h : J ⊆ supp v then the induced valuation on R / J = ideal.quotient J is on_quot v h.

## Main definitions #

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

• valuation.is_equiv, the heterogeneous equivalence relation on valuations

• valuation.supp, the support of a valuation

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

## Implementation Details #

add_valuation R Γ₀ is implemented as valuation R (multiplicative Γ₀)ᵒᵈ.

## Notation #

In the discrete_valuation locale:

## TODO #

If ever someone extends valuation, we should fully comply to the fun_like by migrating the boilerplate lemmas to valuation_class.

@[nolint]
structure valuation (R : Type u_3) (Γ₀ : Type u_4) [ring R] :
Type (max u_3 u_4)

The type of Γ₀-valued valuations on R.

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

Instances for valuation
@[class]
structure valuation_class (F : Type u_2) (R : Type u_3) (Γ₀ : Type u_4) [ring R] :
Type (max u_2 u_3 u_4)

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

You should also extend this typeclass when you extend valuation.

Instances of this typeclass
Instances of other typeclasses for valuation_class
• valuation_class.has_sizeof_inst
@[protected, instance]
def valuation.has_coe_t (F : Type u_2) (R : Type u_3) (Γ₀ : Type u_4) [ring R] [ Γ₀] :
Γ₀)
Equations
@[protected, instance]
def valuation.valuation_class {R : Type u_3} {Γ₀ : Type u_4} [ring R]  :
valuation_class Γ₀) R Γ₀
Equations
@[protected, instance]
def valuation.has_coe_to_fun {R : Type u_3} {Γ₀ : Type u_4} [ring R]  :
has_coe_to_fun Γ₀) (λ (_x : Γ₀), R → Γ₀)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem valuation.to_fun_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
@[ext]
theorem valuation.ext {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v₁ v₂ : Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
v₁ = v₂
@[simp, norm_cast]
theorem valuation.coe_coe {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
@[simp]
theorem valuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
v 0 = 0
@[simp]
theorem valuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
v 1 = 1
@[simp]
theorem valuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x * y) = v x * v y
@[simp]
theorem valuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x + y) linear_order.max (v x) (v y)
theorem valuation.map_add_le {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x 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 : Γ₀) {x 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 : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ (i : ι), i sv (f i) g) :
v (s.sum (λ (i : ι), f i)) g
theorem valuation.map_sum_lt {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g 0) (hf : ∀ (i : ι), i sv (f i) < g) :
v (s.sum (λ (i : ι), f i)) < g
theorem valuation.map_sum_lt' {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : 0 < g) (hf : ∀ (i : ι), i sv (f i) < g) :
v (s.sum (λ (i : ι), f i)) < g
@[simp]
theorem valuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x : R) (n : ) :
v (x ^ n) = v x ^ n
theorem valuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v₁ v₂ : Γ₀} :
v₁ = v₂ ∀ (r : R), v₁ r = v₂ r

Deprecated. Use fun_like.ext_iff.

def valuation.to_preorder {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :

A valuation gives a preorder on the underlying ring.

Equations
@[simp]
theorem valuation.zero_iff {K : Type u_1} {Γ₀ : Type u_4} [nontrivial Γ₀] (v : Γ₀) {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} [nontrivial Γ₀] (v : Γ₀) {x : K} :
v x 0 x 0
theorem valuation.unit_map_eq {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (u : Rˣ) :
def valuation.comap {R : Type u_3} {Γ₀ : Type u_4} [ring R] {S : Type u_1} [ring S] (f : S →+* R) (v : Γ₀) :
Γ₀

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

Equations
@[simp]
theorem valuation.comap_apply {R : Type u_3} {Γ₀ : Type u_4} [ring R] {S : Type u_1} [ring S] (f : S →+* R) (v : Γ₀) (s : S) :
v) s = v (f s)
@[simp]
theorem valuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
= v
theorem valuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {S₁ : Type u_1} {S₂ : Type u_2} [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] (f : Γ₀ →*₀ Γ'₀) (hf : monotone f) (v : Γ₀) :
Γ'₀

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

Equations
def valuation.is_equiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] (v₁ : Γ₀) (v₂ : Γ'₀) :
Prop

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

Equations
@[simp]
theorem valuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x : R) :
v (-x) = v x
theorem valuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x - y) = v (y - x)
theorem valuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x - y) linear_order.max (v x) (v y)
theorem valuation.map_sub_le {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x 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 : Γ₀) {x y : R} (h : v x v y) :
v (x + y) = linear_order.max (v x) (v y)
theorem valuation.map_add_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x 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 : Γ₀) {x 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 : Γ₀) {x 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 : Γ₀) {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 : Γ₀) {x : R} (h : v x < 1) :
v (1 - x) = 1
theorem valuation.one_lt_val_iff {K : Type u_1} {Γ₀ : Type u_4} (v : Γ₀) {x : K} (h : x 0) :
1 < v x v x⁻¹ < 1
def valuation.lt_add_subgroup {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (γ : Γ₀ˣ) :

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

Equations
@[refl]
theorem valuation.is_equiv.refl {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v : Γ₀} :
@[symm]
theorem valuation.is_equiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) :
v₂.is_equiv v₁
@[trans]
theorem valuation.is_equiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} {v₃ : Γ''₀} (h₁₂ : v₁.is_equiv v₂) (h₂₃ : v₂.is_equiv v₃) :
v₁.is_equiv v₃
theorem valuation.is_equiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v v' : Γ₀} (h : v = v') :
theorem valuation.is_equiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v v' : Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : monotone f) (inf : function.injective f) (h : v.is_equiv v') :
hf v).is_equiv hf v')
theorem valuation.is_equiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} {S : Type u_1} [ring S] (f : S →+* R) (h : v₁.is_equiv v₂) :
v₁).is_equiv v₂)

comap preserves equivalence.

theorem valuation.is_equiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) {r s : R} :
v₁ r = v₁ s v₂ r = v₂ s
theorem valuation.is_equiv.ne_zero {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) {r : R} :
v₁ r 0 v₂ r 0
theorem valuation.is_equiv_of_map_strict_mono {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v : Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : strict_mono f) :
_ v).is_equiv v
theorem valuation.is_equiv_of_val_le_one {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) (h : ∀ {x : K}, v x 1 v' x 1) :
theorem valuation.is_equiv_iff_val_le_one {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) :
v.is_equiv v' ∀ {x : K}, v x 1 v' x 1
theorem valuation.is_equiv_iff_val_eq_one {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) :
v.is_equiv v' ∀ {x : K}, v x = 1 v' x = 1
theorem valuation.is_equiv_iff_val_lt_one {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) :
v.is_equiv v' ∀ {x : K}, v x < 1 v' x < 1
theorem valuation.is_equiv_iff_val_sub_one_lt_one {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) :
v.is_equiv v' ∀ {x : K}, v (x - 1) < 1 v' (x - 1) < 1
theorem valuation.is_equiv_tfae {K : Type u_1} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} (v : Γ₀) (v' : Γ'₀) :
[v.is_equiv 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} [comm_ring R] (v : Γ₀) :

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

Equations
Instances for valuation.supp
@[simp]
theorem valuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) (x : R) :
x v.supp v x = 0
@[protected, instance]
def valuation.supp.ideal.is_prime {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) [nontrivial Γ₀] [no_zero_divisors Γ₀] :

The support of a valuation is a prime ideal.

theorem valuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) (a : R) {s : R} (h : s v.supp) :
v (a + s) = v a
def valuation.on_quot_val {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
R J → Γ₀

If hJ : J ⊆ supp v then on_quot_val hJ is the induced function on R/J as a function. Note: it's just the function; the valuation is on_quot hJ.

Equations
def valuation.on_quot {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
valuation (R J) Γ₀

The extension of valuation v on R to valuation on R/J if J ⊆ supp v

Equations
@[simp]
theorem valuation.on_quot_comap_eq {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ) = v
theorem valuation.comap_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {S : Type u_1} [comm_ring S] (f : S →+* R) :
v).supp = v.supp
theorem valuation.self_le_supp_comap {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (J : ideal R) (v : valuation (R J) Γ₀) :
J v).supp
@[simp]
theorem valuation.comap_on_quot_eq {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (J : ideal R) (v : valuation (R J) Γ₀) :
v).on_quot _ = v
theorem valuation.supp_quot {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ).supp =

The quotient valuation on R/J has support supp(v)/J if J ⊆ supp v.

theorem valuation.supp_quot_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) :
@[nolint, irreducible]
def add_valuation (R : Type u_3) [ring R] (Γ₀ : Type u_4)  :
Type (max u_3 u_4)

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

Equations
@[protected, instance]
def add_valuation.has_coe_to_fun (R : Type u_3) (Γ₀ : Type u_4) [ring R] :
has_coe_to_fun Γ₀) (λ (_x : Γ₀), R → Γ₀)

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

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

An alternate constructor of add_valuation, that doesn't reference multiplicative Γ₀ᵒᵈ

Equations
@[simp]
theorem add_valuation.of_apply {R : Type u_3} {Γ₀ : Type u_4} [ring R] (f : R → Γ₀) {h0 : f 0 = } {h1 : f 1 = 0} {hadd : ∀ (x y : R), linear_order.min (f x) (f y) f (x + y)} {hmul : ∀ (x y : R), f (x * y) = f x + f y} {r : R} :
h0 h1 hadd hmul) r = f r
def add_valuation.valuation {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :

The valuation associated to an add_valuation (useful if the latter is constructed using add_valuation.of).

Equations
@[simp]
theorem add_valuation.valuation_apply {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (r : R) :
@[simp]
theorem add_valuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
v 0 =
@[simp]
theorem add_valuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
v 1 = 0
@[simp]
theorem add_valuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x * y) = v x + v y
@[simp]
theorem add_valuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
linear_order.min (v x) (v y) v (x + y)
theorem add_valuation.map_le_add {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x y : R} {g : Γ₀} (hx : g v x) (hy : g v y) :
g v (x + y)
theorem add_valuation.map_lt_add {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x y : R} {g : Γ₀} (hx : g < v x) (hy : g < v y) :
g < v (x + y)
theorem add_valuation.map_le_sum {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ (i : ι), i sg v (f i)) :
g v (s.sum (λ (i : ι), f i))
theorem add_valuation.map_lt_sum {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g ) (hf : ∀ (i : ι), i sg < v (f i)) :
g < v (s.sum (λ (i : ι), f i))
theorem add_valuation.map_lt_sum' {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g < ) (hf : ∀ (i : ι), i sg < v (f i)) :
g < v (s.sum (λ (i : ι), f i))
@[simp]
theorem add_valuation.map_pow {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x : R) (n : ) :
v (x ^ n) = n v x
@[ext]
theorem add_valuation.ext {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v₁ v₂ : Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
v₁ = v₂
theorem add_valuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v₁ v₂ : Γ₀} :
v₁ = v₂ ∀ (r : R), v₁ r = v₂ r
def add_valuation.to_preorder {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :

A valuation gives a preorder on the underlying ring.

Equations
@[simp]
theorem add_valuation.top_iff {K : Type u_1} {Γ₀ : Type u_4} [nontrivial Γ₀] (v : Γ₀) {x : K} :
v x = x = 0

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

theorem add_valuation.ne_top_iff {K : Type u_1} {Γ₀ : Type u_4} [nontrivial Γ₀] (v : Γ₀) {x : K} :
v x x 0
def add_valuation.comap {R : Type u_3} {Γ₀ : Type u_4} [ring R] {S : Type u_1} [ring S] (f : S →+* R) (v : Γ₀) :
Γ₀

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

Equations
@[simp]
theorem add_valuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) :
= v
theorem add_valuation.comap_comp {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {S₁ : Type u_1} {S₂ : Type u_2} [ring S₁] [ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
def add_valuation.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : monotone f) (v : Γ₀) :
Γ'₀

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

Equations
def add_valuation.is_equiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] (v₁ : Γ₀) (v₂ : Γ'₀) :
Prop

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

Equations
@[simp]
theorem add_valuation.map_inv {K : Type u_1} {Γ₀ : Type u_4} (v : Γ₀) {x : K} :
@[simp]
theorem add_valuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x : R) :
v (-x) = v x
theorem add_valuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
v (x - y) = v (y - x)
theorem add_valuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) (x y : R) :
linear_order.min (v x) (v y) v (x - y)
theorem add_valuation.map_le_sub {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x y : R} {g : Γ₀} (hx : g v x) (hy : g v y) :
g v (x - y)
theorem add_valuation.map_add_of_distinct_val {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x y : R} (h : v x v y) :
v (x + y) = linear_order.min (v x) (v y)
theorem add_valuation.map_eq_of_lt_sub {R : Type u_3} {Γ₀ : Type u_4} [ring R] (v : Γ₀) {x y : R} (h : v x < v (y - x)) :
v y = v x
@[refl]
theorem add_valuation.is_equiv.refl {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v : Γ₀} :
@[symm]
theorem add_valuation.is_equiv.symm {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) :
v₂.is_equiv v₁
@[trans]
theorem add_valuation.is_equiv.trans {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {Γ''₀ : Type u_6} {v₁ : Γ₀} {v₂ : Γ'₀} {v₃ : Γ''₀} (h₁₂ : v₁.is_equiv v₂) (h₂₃ : v₂.is_equiv v₃) :
v₁.is_equiv v₃
theorem add_valuation.is_equiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [ring R] {v v' : Γ₀} (h : v = v') :
theorem add_valuation.is_equiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v v' : Γ₀} (f : Γ₀ →+ Γ'₀) (ht : f = ) (hf : monotone f) (inf : function.injective f) (h : v.is_equiv v') :
ht hf v).is_equiv ht hf v')
theorem add_valuation.is_equiv.comap {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} {S : Type u_1} [ring S] (f : S →+* R) (h : v₁.is_equiv v₂) :
v₁).is_equiv v₂)

comap preserves equivalence.

theorem add_valuation.is_equiv.val_eq {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) {r s : R} :
v₁ r = v₁ s v₂ r = v₂ s
theorem add_valuation.is_equiv.ne_top {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [ring R] {v₁ : Γ₀} {v₂ : Γ'₀} (h : v₁.is_equiv v₂) {r : R} :
v₁ r v₂ r
def add_valuation.supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) :

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

Equations
@[simp]
theorem add_valuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) (x : R) :
x v.supp v x =
theorem add_valuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) (a : R) {s : R} (h : s v.supp) :
v (a + s) = v a
def add_valuation.on_quot_val {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
R J → Γ₀

If hJ : J ⊆ supp v then on_quot_val hJ is the induced function on R/J as a function. Note: it's just the function; the valuation is on_quot hJ.

Equations
def add_valuation.on_quot {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :

The extension of valuation v on R to valuation on R/J if J ⊆ supp v

Equations
@[simp]
theorem add_valuation.on_quot_comap_eq {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ) = v
theorem add_valuation.comap_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {S : Type u_1} [comm_ring S] (f : S →+* R) :
v).supp = v.supp
theorem add_valuation.self_le_supp_comap {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (J : ideal R) (v : add_valuation (R J) Γ₀) :
@[simp]
theorem add_valuation.comap_on_quot_eq {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (J : ideal R) (v : add_valuation (R J) Γ₀) :
_ = v
theorem add_valuation.supp_quot {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) {J : ideal R} (hJ : J v.supp) :
(v.on_quot hJ).supp =

The quotient valuation on R/J has support supp(v)/J if J ⊆ supp v.

theorem add_valuation.supp_quot_supp {R : Type u_3} {Γ₀ : Type u_4} [comm_ring R] (v : Γ₀) :