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

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

def valuation.to_monoid_hom {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] :
valuation R Γ₀R →* Γ₀

The monoid_hom underlying a valuation.

@[nolint]
structure valuation (R : Type u_1) (Γ₀ : Type u_2) [linear_ordered_comm_group_with_zero Γ₀] [ring R] :
Type (max u_1 u_2)

The type of Γ₀-valued valuations on R.

@[instance]
def valuation.has_coe_to_fun (R : Type u_1) (Γ₀ : Type u_2) [linear_ordered_comm_group_with_zero Γ₀] [ring R] :

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

Equations
@[instance]
def valuation.has_coe (R : Type u_1) (Γ₀ : Type u_2) [linear_ordered_comm_group_with_zero Γ₀] [ring R] :
has_coe (valuation R Γ₀) (R →* Γ₀)

A valuation is coerced to a monoid morphism R → Γ₀.

Equations
@[simp]
theorem valuation.coe_coe {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) :

@[simp]
theorem valuation.map_zero {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) :
v 0 = 0

@[simp]
theorem valuation.map_one {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) :
v 1 = 1

@[simp]
theorem valuation.map_mul {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (x y : R) :
v (x * y) = (v x) * v y

@[simp]
theorem valuation.map_add {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (x y : R) :
v (x + y) max (v x) (v y)

@[simp]
theorem valuation.map_pow {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (x : R) (n : ) :
v (x ^ n) = v x ^ n

@[ext]
theorem valuation.ext {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] {v₁ v₂ : valuation R Γ₀} :
(∀ (r : R), v₁ r = v₂ r)v₁ = v₂

theorem valuation.ext_iff {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] {v₁ v₂ : valuation R Γ₀} :
v₁ = v₂ ∀ (r : R), v₁ r = v₂ r

def valuation.to_preorder {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] :
valuation R Γ₀preorder R

A valuation gives a preorder on the underlying ring.

Equations
@[simp]
theorem valuation.zero_iff {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {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_2} [linear_ordered_comm_group_with_zero Γ₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) {x : K} :
v x 0 x 0

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

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

@[simp]
theorem valuation.unit_map_eq {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (u : units R) :

theorem valuation.map_neg_one {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) :
v (-1) = 1

@[simp]
theorem valuation.map_neg {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (x : R) :
v (-x) = v x

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

theorem valuation.map_sub_le_max {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) (x y : R) :
v (x - y) max (v x) (v y)

theorem valuation.map_add_of_distinct_val {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) {x y : R} :
v x v yv (x + y) = max (v x) (v y)

theorem valuation.map_eq_of_sub_lt {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) {x y : R} :
v (y - x) < v xv y = v x

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

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

Equations
@[simp]
theorem valuation.comap_id {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] (v : valuation R Γ₀) :

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

def valuation.map {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] (f : Γ₀ →* Γ'₀) :
f 0 = 0monotone fvaluation R Γ₀valuation R Γ'₀

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

Equations
def valuation.is_equiv {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] :
valuation R Γ₀valuation R Γ'₀ → Prop

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

Equations
theorem valuation.is_equiv.refl {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] {v : valuation R Γ₀} :

theorem valuation.is_equiv.symm {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} :
v₁.is_equiv v₂v₂.is_equiv v₁

theorem valuation.is_equiv.trans {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] {Γ''₀ : Type u_4} [linear_ordered_comm_group_with_zero Γ''₀] [ring R] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} {v₃ : valuation R Γ''₀} :
v₁.is_equiv v₂v₂.is_equiv v₃v₁.is_equiv v₃

theorem valuation.is_equiv.of_eq {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [ring R] {v v' : valuation R Γ₀} :
v = v'v.is_equiv v'

theorem valuation.is_equiv.map {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {v v' : valuation R Γ₀} (f : Γ₀ →* Γ'₀) (h₀ : f 0 = 0) (hf : monotone f) :
function.injective fv.is_equiv v'(valuation.map f h₀ hf v).is_equiv (valuation.map f h₀ hf v')

theorem valuation.is_equiv.comap {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} {S : Type u_4} [ring S] (f : S →+* R) :
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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] [ring R] {v : valuation R Γ₀} (f : Γ₀ →* Γ'₀) (h₀ : f 0 = 0) (H : strict_mono f) :
(valuation.map f h₀ _ v).is_equiv v

theorem valuation.is_equiv_of_val_le_one {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {Γ'₀ : Type u_3} [linear_ordered_comm_group_with_zero Γ'₀] {K : Type u_1} [division_ring K] (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
(∀ {x : K}, v x 1 v' x 1)v.is_equiv v'

def valuation.supp {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] :
valuation R Γ₀ideal R

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

Equations
@[simp]
theorem valuation.mem_supp_iff {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) (x : R) :
x v.supp v x = 0

@[instance]
def valuation.ideal.is_prime {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) :

The support of a valuation is a prime ideal.

theorem valuation.map_add_supp {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) (a : R) {s : R} :
s v.suppv (a + s) = v a

def valuation.on_quot_val {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) {J : ideal R} :
J v.suppJ.quotient → Γ₀

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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) {J : ideal R} :
J v.suppvaluation J.quotient Γ₀

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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) {J : ideal R} (hJ : J v.supp) :

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

theorem valuation.self_le_supp_comap {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (J : ideal R) (v : valuation J.quotient Γ₀) :

@[simp]
theorem valuation.comap_on_quot_eq {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (J : ideal R) (v : valuation J.quotient Γ₀) :

theorem valuation.supp_quot {R : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) {J : ideal R} (hJ : 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_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] [comm_ring R] (v : valuation R Γ₀) :
(v.on_quot _).supp = 0