mathlib documentation

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 (order_dual Γ₀)).

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_2) (Γ₀ : Type u_3) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R] :

Type (max u_2 u_3)

to_monoid_with_zero_hom : R →*₀ Γ₀
map_add_le_max' : ∀ (x y : R), self.to_monoid_with_zero_hom.to_fun (x + y) ≤ max (self.to_monoid_with_zero_hom.to_fun x) (self.to_monoid_with_zero_hom.to_fun y)

The type of Γ₀-valued valuations on R.

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

@[class]

structure valuation_class (F : Type u_1) (R : Type u_2) (Γ₀ : Type u_3) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R] :

Type (max u_1 u_2 u_3)

to_monoid_with_zero_hom_class : monoid_with_zero_hom_class F R Γ₀
map_add_le_max : ∀ (f : F) (x y : R), ⇑f (x + y) ≤ max (⇑f x) (⇑f y)

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

You should also extend this typeclass when you extend valuation.

Instances

valuation.valuation_class

@[protected, instance]

def valuation.has_coe_t (F : Type u_1) (R : Type u_2) (Γ₀ : Type u_3) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R] [valuation_class F R Γ₀] :

has_coe_t F (valuation R Γ₀)

Equations

valuation.has_coe_t F R Γ₀ = {coe := λ (f : F), {to_monoid_with_zero_hom := {to_fun := ⇑f, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}}

@[protected, instance]

def valuation.valuation_class {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] :

valuation_class (valuation R Γ₀) R Γ₀

Equations

valuation.valuation_class = {to_monoid_with_zero_hom_class := {coe := λ (f : valuation R Γ₀), f.to_monoid_with_zero_hom.to_fun, coe_injective' := _, map_mul := _, map_one := _, map_zero := _}, map_add_le_max := _}

@[protected, instance]

def valuation.has_coe_to_fun {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] :

has_coe_to_fun (valuation R Γ₀) (λ (_x : valuation R Γ₀), R → Γ₀)

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

Equations

valuation.has_coe_to_fun = fun_like.has_coe_to_fun

@[simp]

theorem valuation.to_fun_eq_coe {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

v.to_monoid_with_zero_hom.to_fun = ⇑v

@[ext]

theorem valuation.ext {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] {v₁ v₂ : valuation R Γ₀} (h : ∀ (r : R), ⇑v₁ r = ⇑v₂ r) :

v₁ = v₂

@[simp, norm_cast]

theorem valuation.coe_coe {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

@[simp]

theorem valuation.map_zero {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

⇑v 0 = 0

@[simp]

theorem valuation.map_one {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

⇑v 1 = 1

@[simp]

theorem valuation.map_mul {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (x y : R) :

⇑v (x * y) = (⇑v x) * ⇑v y

@[simp]

theorem valuation.map_add {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (x y : R) :

⇑v (x + y) ≤ max (⇑v x) (⇑v y)

theorem valuation.map_add_le {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {x y : R} {g : Γ₀} (hx : ⇑v x ≤ g) (hy : ⇑v y ≤ g) :

⇑v (x + y) ≤ g

theorem valuation.map_add_lt {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {x y : R} {g : Γ₀} (hx : ⇑v x < g) (hy : ⇑v y < g) :

⇑v (x + y) < g

theorem valuation.map_sum_le {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ (i : ι), i ∈ s → ⇑v (f i) ≤ g) :

⇑v (∑ (i : ι) in s, f i) ≤ g

theorem valuation.map_sum_lt {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g ≠ 0) (hf : ∀ (i : ι), i ∈ s → ⇑v (f i) < g) :

⇑v (∑ (i : ι) in s, f i) < g

theorem valuation.map_sum_lt' {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : 0 < g) (hf : ∀ (i : ι), i ∈ s → ⇑v (f i) < g) :

⇑v (∑ (i : ι) in s, f i) < g

@[simp]

theorem valuation.map_pow {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (x : R) (n : ℕ) :

⇑v (x ^ n) = ⇑v x ^ n

theorem valuation.ext_iff {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] {v₁ v₂ : valuation R Γ₀} :

v₁ = v₂ ↔ ∀ (r : R), ⇑v₁ r = ⇑v₂ r

Deprecated. Use fun_like.ext_iff.

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

A valuation gives a preorder on the underlying ring.

Equations

v.to_preorder = preorder.lift ⇑v

@[simp]

theorem valuation.zero_iff {Γ₀ : Type u_3} [linear_ordered_comm_monoid_with_zero Γ₀] [nontrivial Γ₀] {K : Type u_1} [division_ring K] (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 {Γ₀ : Type u_3} [linear_ordered_comm_monoid_with_zero Γ₀] [nontrivial Γ₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) {x : K} :

⇑v x ≠ 0 ↔ x ≠ 0

theorem valuation.unit_map_eq {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (u : Rˣ) :

↑(⇑(units.map ↑v) u) = ⇑v ↑u

def valuation.comap {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] {S : Type u_1} [ring S] (f : S →+* R) (v : valuation R Γ₀) :

valuation S Γ₀

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

Equations

valuation.comap f v = {to_monoid_with_zero_hom := {to_fun := ⇑v ∘ ⇑f, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

@[simp]

theorem valuation.comap_id {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

valuation.comap (ring_hom.id R) v = v

theorem valuation.comap_comp {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {S₁ : Type u_1} {S₂ : Type u_4} [ring S₁] [ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :

valuation.comap (g.comp f) v = valuation.comap f (valuation.comap g v)

def valuation.map {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] (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 = {to_monoid_with_zero_hom := {to_fun := ⇑f ∘ ⇑v, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

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

Prop

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

Equations

v₁.is_equiv v₂ = ∀ (r s : R), ⇑v₁ r ≤ ⇑v₁ s ↔ ⇑v₂ r ≤ ⇑v₂ s

@[simp]

theorem valuation.map_inv {Γ₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) {x : K} :

⇑v x⁻¹ = (⇑v x)⁻¹

@[simp]

theorem valuation.map_zpow {Γ₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) {x : K} {n : ℤ} :

⇑v (x ^ n) = ⇑v x ^ n

theorem valuation.map_units_inv {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (x : Rˣ) :

⇑v ↑x⁻¹ = (⇑v ↑x)⁻¹

@[simp]

theorem valuation.map_neg {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (x : R) :

⇑v (-x) = ⇑v x

theorem valuation.map_sub_swap {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (x y : R) :

⇑v (x - y) = ⇑v (y - x)

theorem valuation.map_sub {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (x y : R) :

⇑v (x - y) ≤ max (⇑v x) (⇑v y)

theorem valuation.map_sub_le {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) {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_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) {x y : R} (h : ⇑v x ≠ ⇑v y) :

⇑v (x + y) = max (⇑v x) (⇑v y)

theorem valuation.map_eq_of_sub_lt {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) {x y : R} (h : ⇑v (y - x) < ⇑v x) :

⇑v y = ⇑v x

def valuation.lt_add_subgroup {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (γ : Γ₀ˣ) :

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

Equations

v.lt_add_subgroup γ = {carrier := {x : R | ⇑v x < ↑γ}, add_mem' := _, zero_mem' := _, neg_mem' := _}

theorem valuation.is_equiv.refl {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] {v : valuation R Γ₀} :

theorem valuation.is_equiv.symm {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) :

v₂.is_equiv v₁

theorem valuation.is_equiv.trans {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} {Γ''₀ : Type u_5} [linear_ordered_comm_monoid_with_zero Γ''₀] [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} {v₃ : valuation R Γ''₀} (h₁₂ : v₁.is_equiv v₂) (h₂₃ : v₂.is_equiv v₃) :

v₁.is_equiv v₃

theorem valuation.is_equiv.of_eq {R : Type u_2} {Γ₀ : Type u_3} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] {v v' : valuation R Γ₀} (h : v = v') :

theorem valuation.is_equiv.map {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v v' : valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : monotone ⇑f) (inf : function.injective ⇑f) (h : v.is_equiv v') :

(valuation.map f hf v).is_equiv (valuation.map f hf v')

theorem valuation.is_equiv.comap {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} {S : Type u_1} [ring S] (f : S →+* R) (h : v₁.is_equiv v₂) :

(valuation.comap f v₁).is_equiv (valuation.comap f v₂)

comap preserves equivalence.

theorem valuation.is_equiv.val_eq {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (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_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [ring R] [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) {r : R} :

⇑v₁ r ≠ 0 ↔ ⇑v₂ r ≠ 0

theorem valuation.is_equiv_of_map_strict_mono {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_comm_monoid_with_zero Γ₀] [linear_ordered_comm_monoid_with_zero Γ'₀] [ring R] {v : valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : strict_mono ⇑f) :

(valuation.map f _ v).is_equiv v

theorem valuation.is_equiv_of_val_le_one {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_comm_group_with_zero Γ₀] [linear_ordered_comm_group_with_zero Γ'₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) (v' : valuation K Γ'₀) (h : ∀ {x : K}, ⇑v x ≤ 1 ↔ ⇑v' x ≤ 1) :

def valuation.supp {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (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' := _}

@[simp]

theorem valuation.mem_supp_iff {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (x : R) :

x ∈ v.supp ↔ ⇑v x = 0

@[protected, instance]

def valuation.supp.ideal.is_prime {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) [nontrivial Γ₀] [no_zero_divisors Γ₀] :

v.supp.is_prime

The support of a valuation is a prime ideal.

theorem valuation.map_add_supp {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) (a : R) {s : R} (h : s ∈ v.supp) :

⇑v (a + s) = ⇑v a

def valuation.on_quot_val {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {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

v.on_quot_val hJ = λ (q : R ⧸ J), quotient.lift_on' q ⇑v _

def valuation.on_quot {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {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

v.on_quot hJ = {to_monoid_with_zero_hom := {to_fun := v.on_quot_val hJ, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

@[simp]

theorem valuation.on_quot_comap_eq {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {J : ideal R} (hJ : J ≤ v.supp) :

valuation.comap (ideal.quotient.mk J) (v.on_quot hJ) = v

theorem valuation.comap_supp {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {S : Type u_1} [comm_ring S] (f : S →+* R) :

(valuation.comap f v).supp = ideal.comap f v.supp

theorem valuation.self_le_supp_comap {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (J : ideal R) (v : valuation (R ⧸ J) Γ₀) :

J ≤ (valuation.comap (ideal.quotient.mk J) v).supp

@[simp]

theorem valuation.comap_on_quot_eq {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (J : ideal R) (v : valuation (R ⧸ J) Γ₀) :

(valuation.comap (ideal.quotient.mk J) v).on_quot _ = v

theorem valuation.supp_quot {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) {J : ideal R} (hJ : J ≤ v.supp) :

(v.on_quot hJ).supp = ideal.map (ideal.quotient.mk J) v.supp

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

theorem valuation.supp_quot_supp {R : Type u_2} {Γ₀ : Type u_3} [comm_ring R] [linear_ordered_comm_monoid_with_zero Γ₀] (v : valuation R Γ₀) :

(v.on_quot le_rfl).supp = 0

@[nolint]

def add_valuation (R : Type u_2) [ring R] (Γ₀ : Type u_3) [linear_ordered_add_comm_monoid_with_top Γ₀] :

Type (max u_2 u_3)

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

Equations

add_valuation R Γ₀ = valuation R (multiplicative (order_dual Γ₀))

@[protected, instance]

def add_valuation.has_coe_to_fun (R : Type u_2) (Γ₀ : Type u_3) [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] :

has_coe_to_fun (add_valuation R Γ₀) (λ (_x : add_valuation R Γ₀), R → Γ₀)

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

Equations

add_valuation.has_coe_to_fun R Γ₀ = {coe := λ (v : add_valuation R Γ₀), v.to_monoid_with_zero_hom.to_fun}

def add_valuation.of {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [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) :

add_valuation R Γ₀

An alternate constructor of add_valuation, that doesn't reference multiplicative (order_dual Γ₀)

Equations

add_valuation.of f h0 h1 hadd hmul = {to_monoid_with_zero_hom := {to_fun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul}, map_add_le_max' := hadd}

@[simp]

theorem add_valuation.of_apply {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [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} :

⇑(add_valuation.of f h0 h1 hadd hmul) r = f r

def add_valuation.valuation {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) :

valuation R (multiplicative (order_dual Γ₀))

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

Equations

v.valuation = v

@[simp]

theorem add_valuation.valuation_apply {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (r : R) :

⇑(v.valuation) r = ⇑multiplicative.of_add (⇑order_dual.to_dual (⇑v r))

@[simp]

theorem add_valuation.map_zero {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) :

@[simp]

theorem add_valuation.map_one {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) :

⇑v 1 = 0

@[simp]

theorem add_valuation.map_mul {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x y : R) :

⇑v (x * y) = ⇑v x + ⇑v y

@[simp]

theorem add_valuation.map_add {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x y : R) :

min (⇑v x) (⇑v y) ≤ ⇑v (x + y)

theorem add_valuation.map_le_add {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {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_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {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_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ (i : ι), i ∈ s → g ≤ ⇑v (f i)) :

g ≤ ⇑v (∑ (i : ι) in s, f i)

theorem add_valuation.map_lt_sum {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g ≠ ⊤) (hf : ∀ (i : ι), i ∈ s → g < ⇑v (f i)) :

g < ⇑v (∑ (i : ι) in s, f i)

theorem add_valuation.map_lt_sum' {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {ι : Type u_1} {s : finset ι} {f : ι → R} {g : Γ₀} (hg : g < ⊤) (hf : ∀ (i : ι), i ∈ s → g < ⇑v (f i)) :

g < ⇑v (∑ (i : ι) in s, f i)

@[simp]

theorem add_valuation.map_pow {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x : R) (n : ℕ) :

⇑v (x ^ n) = n • ⇑v x

@[ext]

theorem add_valuation.ext {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] {v₁ v₂ : add_valuation R Γ₀} (h : ∀ (r : R), ⇑v₁ r = ⇑v₂ r) :

v₁ = v₂

theorem add_valuation.ext_iff {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] {v₁ v₂ : add_valuation R Γ₀} :

v₁ = v₂ ↔ ∀ (r : R), ⇑v₁ r = ⇑v₂ r

def add_valuation.to_preorder {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) :

A valuation gives a preorder on the underlying ring.

Equations

v.to_preorder = preorder.lift ⇑v

@[simp]

theorem add_valuation.top_iff {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [nontrivial Γ₀] {K : Type u_1} [division_ring K] (v : add_valuation K Γ₀) {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 {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [nontrivial Γ₀] {K : Type u_1} [division_ring K] (v : add_valuation K Γ₀) {x : K} :

⇑v x ≠ ⊤ ↔ x ≠ 0

def add_valuation.comap {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] {S : Type u_1} [ring S] (f : S →+* R) (v : add_valuation R Γ₀) :

add_valuation S Γ₀

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

Equations

add_valuation.comap f v = valuation.comap f v

@[simp]

theorem add_valuation.comap_id {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) :

add_valuation.comap (ring_hom.id R) v = v

theorem add_valuation.comap_comp {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {S₁ : Type u_1} {S₂ : Type u_4} [ring S₁] [ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :

add_valuation.comap (g.comp f) v = add_valuation.comap f (add_valuation.comap g v)

def add_valuation.map {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] (f : Γ₀ →+ Γ'₀) (ht : ⇑f ⊤ = ⊤) (hf : monotone ⇑f) (v : add_valuation R Γ₀) :

add_valuation R Γ'₀

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

Equations

add_valuation.map f ht hf v = valuation.map {to_fun := ⇑f, map_zero' := ht, map_one' := _, map_mul' := _} _ v

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

Prop

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

Equations

v₁.is_equiv v₂ = valuation.is_equiv v₁ v₂

@[simp]

theorem add_valuation.map_inv {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] {K : Type u_1} [division_ring K] (v : add_valuation K Γ₀) {x : K} :

⇑v x⁻¹ = -⇑v x

theorem add_valuation.map_units_inv {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x : Rˣ) :

⇑v ↑x⁻¹ = -⇑v ↑x

@[simp]

theorem add_valuation.map_neg {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x : R) :

⇑v (-x) = ⇑v x

theorem add_valuation.map_sub_swap {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x y : R) :

⇑v (x - y) = ⇑v (y - x)

theorem add_valuation.map_sub {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) (x y : R) :

min (⇑v x) (⇑v y) ≤ ⇑v (x - y)

theorem add_valuation.map_le_sub {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {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_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y : R} (h : ⇑v x ≠ ⇑v y) :

⇑v (x + y) = min (⇑v x) (⇑v y)

theorem add_valuation.map_eq_of_lt_sub {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y : R} (h : ⇑v x < ⇑v (y - x)) :

⇑v y = ⇑v x

theorem add_valuation.is_equiv.refl {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] {v : add_valuation R Γ₀} :

theorem add_valuation.is_equiv.symm {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {v₁ : add_valuation R Γ₀} {v₂ : add_valuation R Γ'₀} (h : v₁.is_equiv v₂) :

v₂.is_equiv v₁

theorem add_valuation.is_equiv.trans {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {Γ''₀ : Type u_5} [linear_ordered_add_comm_monoid_with_top Γ''₀] {v₁ : add_valuation R Γ₀} {v₂ : add_valuation R Γ'₀} {v₃ : add_valuation R Γ''₀} (h₁₂ : v₁.is_equiv v₂) (h₂₃ : v₂.is_equiv v₃) :

v₁.is_equiv v₃

theorem add_valuation.is_equiv.of_eq {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [ring R] {v v' : add_valuation R Γ₀} (h : v = v') :

theorem add_valuation.is_equiv.map {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {v v' : add_valuation R Γ₀} (f : Γ₀ →+ Γ'₀) (ht : ⇑f ⊤ = ⊤) (hf : monotone ⇑f) (inf : function.injective ⇑f) (h : v.is_equiv v') :

(add_valuation.map f ht hf v).is_equiv (add_valuation.map f ht hf v')

theorem add_valuation.is_equiv.comap {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {v₁ : add_valuation R Γ₀} {v₂ : add_valuation R Γ'₀} {S : Type u_1} [ring S] (f : S →+* R) (h : v₁.is_equiv v₂) :

(add_valuation.comap f v₁).is_equiv (add_valuation.comap f v₂)

comap preserves equivalence.

theorem add_valuation.is_equiv.val_eq {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {v₁ : add_valuation R Γ₀} {v₂ : add_valuation R Γ'₀} (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_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_4} [linear_ordered_add_comm_monoid_with_top Γ₀] [linear_ordered_add_comm_monoid_with_top Γ'₀] [ring R] {v₁ : add_valuation R Γ₀} {v₂ : add_valuation R Γ'₀} (h : v₁.is_equiv v₂) {r : R} :

⇑v₁ r ≠ ⊤ ↔ ⇑v₂ r ≠ ⊤

def add_valuation.supp {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) :

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

Equations

v.supp = valuation.supp v

@[simp]

theorem add_valuation.mem_supp_iff {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) (x : R) :

x ∈ v.supp ↔ ⇑v x = ⊤

theorem add_valuation.map_add_supp {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) (a : R) {s : R} (h : s ∈ v.supp) :

⇑v (a + s) = ⇑v a

def add_valuation.on_quot_val {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) {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

v.on_quot_val hJ = valuation.on_quot_val v hJ

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

add_valuation (R ⧸ J) Γ₀

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

Equations

v.on_quot hJ = valuation.on_quot v hJ

@[simp]

theorem add_valuation.on_quot_comap_eq {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) {J : ideal R} (hJ : J ≤ v.supp) :

add_valuation.comap (ideal.quotient.mk J) (v.on_quot hJ) = v

theorem add_valuation.comap_supp {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) {S : Type u_1} [comm_ring S] (f : S →+* R) :

(add_valuation.comap f v).supp = ideal.comap f v.supp

theorem add_valuation.self_le_supp_comap {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (J : ideal R) (v : add_valuation (R ⧸ J) Γ₀) :

J ≤ (add_valuation.comap (ideal.quotient.mk J) v).supp

@[simp]

theorem add_valuation.comap_on_quot_eq {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (J : ideal R) (v : add_valuation (R ⧸ J) Γ₀) :

(add_valuation.comap (ideal.quotient.mk J) v).on_quot _ = v

theorem add_valuation.supp_quot {R : Type u_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) {J : ideal R} (hJ : J ≤ v.supp) :

(v.on_quot hJ).supp = ideal.map (ideal.quotient.mk J) v.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_2} {Γ₀ : Type u_3} [linear_ordered_add_comm_monoid_with_top Γ₀] [comm_ring R] (v : add_valuation R Γ₀) :

(v.on_quot le_rfl).supp = 0