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:

• 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 [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

• 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 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)

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

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

The type of Γ₀-valued valuations on R.

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

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 : F → R → Γ₀
• 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.

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 ∈ s → ↑v (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 ∈ s → ↑v (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 ∈ s → ↑v (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 Γ₀) : Preorder R

A valuation gives a preorder on the underlying ring.

Equations

• Valuation.toPreorder v = Preorder.lift ↑v

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.

@[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 Γ₀) : Valuation.comap (RingHom.id R) v = v

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) : Valuation.comap (RingHom.comp g f) v = Valuation.comap f (Valuation.comap g v)

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.

def Valuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] (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

• Valuation.IsEquiv v₁ v₂ = ∀ (r s : R), ↑v₁ r ≤ ↑v₁ s ↔ ↑v₂ r ≤ ↑v₂ s

@[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 Γ₀) (γ : Γ₀ˣ) : AddSubgroup 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.

theorem Valuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} : Valuation.IsEquiv v v

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₂) : 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₃) : 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') : Valuation.IsEquiv 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') : Valuation.IsEquiv (Valuation.map f hf v) (Valuation.map f hf 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₂) : Valuation.IsEquiv (Valuation.comap f v₁) (Valuation.comap f 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) : Valuation.IsEquiv (Valuation.map f (_ : Monotone ↑f) v) v

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) : Valuation.IsEquiv v v'

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 Γ₀) : Ideal 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.

@[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

instance Valuation.instIsPrimeToSemiringToCommSemiringSupp {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Nontrivial Γ₀] [NoZeroDivisors Γ₀] : Ideal.IsPrime (Valuation.supp v)

The support of a valuation is a prime ideal.

Equations

• @Valuation.instIsPrimeToSemiringToCommSemiringSupp = @Valuation.instIsPrimeToSemiringToCommSemiringSupp.proof_1

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) : Valuation.supp (Valuation.comap f v) = Ideal.comap f (Valuation.supp v)

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

• AddValuation R Γ₀ = Valuation R (Multiplicative Γ₀ᵒᵈ)

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

• AddValuation.instFunLikeAddValuation R Γ₀ = { coe := fun v => v.toFun, coe_injective' := (_ : ∀ (f g : AddValuation R Γ₀), (fun v => v.toFun) f = (fun v => v.toFun) g → f = g) }

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 }

@[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 Γ₀) : Valuation R (Multiplicative Γ₀ᵒᵈ)

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

Equations

• AddValuation.valuation v = v

@[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

• AddValuation.asFun v = ↑v

@[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 ∈ s → g ≤ ↑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 ∈ s → g < ↑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 ∈ s → g < ↑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 Γ₀) : Preorder R

A valuation gives a preorder on the underlying ring.

Equations

• AddValuation.toPreorder v = Preorder.lift ↑v

@[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

• AddValuation.comap f v = Valuation.comap f v

@[simp]

theorem AddValuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) : AddValuation.comap (RingHom.id R) v = v

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) : AddValuation.comap (RingHom.comp g f) v = AddValuation.comap f (AddValuation.comap g v)

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.

def AddValuation.IsEquiv {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] (v₁ : AddValuation R Γ₀) (v₂ : AddValuation R Γ'₀) : Prop

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

Equations

• AddValuation.IsEquiv v₁ v₂ = Valuation.IsEquiv v₁ v₂

@[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.refl {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Ring R] {v : AddValuation R Γ₀} : AddValuation.IsEquiv v v

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₂) : 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₃) : 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') : AddValuation.IsEquiv 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') : AddValuation.IsEquiv (AddValuation.map f ht hf v) (AddValuation.map f ht hf 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₂) : AddValuation.IsEquiv (AddValuation.comap f v₁) (AddValuation.comap f 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 Γ₀) : Ideal R

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

Equations

• AddValuation.supp v = Valuation.supp v

@[simp]

theorem AddValuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) (x : R) : x ∈ AddValuation.supp v ↔ ↑v x = ⊤

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

def DiscreteValuation.termℕₘ₀ : Lean.ParserDescr

Notation for WithZero (Multiplicative ℕ)

Equations

• DiscreteValuation.termℕₘ₀ = Lean.ParserDescr.node `DiscreteValuation.termℕₘ₀ 1024 (Lean.ParserDescr.symbol "ℕₘ₀")

def DiscreteValuation.termℤₘ₀ : Lean.ParserDescr

Notation for WithZero (Multiplicative ℤ)

Equations

• DiscreteValuation.termℤₘ₀ = Lean.ParserDescr.node `DiscreteValuation.termℤₘ₀ 1024 (Lean.ParserDescr.symbol "ℤₘ₀")