# 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.IsNontrivial` is the class of non-trivial valuations, namely those for which there is an element in the ring whose valuation is `≠ 0` and `≠ 1`.

- `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 `WithZero` locale, `Mᵐ⁰` is a shorthand for `WithZero (Multiplicative M)`.

## TODO #

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

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

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

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

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

  The valuation of a sum is less than or equal to the maximum of the valuations.

Instances For

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

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

You should also extend this typeclass when you extend `Valuation`.

- map_mul (f : F) (x y : R) : f (x * y) = f x * f y
- map_one (f : F) : f 1 = 1
- map_zero (f : F) : f 0 = 0
- map_add_le_max (f : F) (x y : R) : f (x + y) ≤ max (f x) (f y)

  The valuation of a sum is less than or equal to the maximum of the valuations.

Instances

source
instance instCoeTCValuationOfValuationClass (F : Type u_2) (R : Type u_3) (Γ₀ : Type u_4) [LinearOrderedCommMonoidWithZero Γ₀] [Ring R] [FunLike F R Γ₀] [ValuationClass F R Γ₀] :
CoeTC F (Valuation R Γ₀)
Equations

- instCoeTCValuationOfValuationClass F R Γ₀ = { coe := fun (f : F) => { toFun := ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ } }

source
instance Valuation.instFunLike {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
FunLike (Valuation R Γ₀) R Γ₀
Equations

- Valuation.instFunLike = { coe := fun (f : Valuation R Γ₀) => (↑f.toMonoidWithZeroHom).toFun, coe_injective' := ⋯ }

source
instance Valuation.instValuationClass {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
ValuationClass (Valuation R Γ₀) R Γ₀
source
@[simp]
theorem Valuation.coe_mk {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (f : R →*₀ Γ₀) (h : ∀ (x y : R), (↑f).toFun (x + y) ≤ max ((↑f).toFun x) ((↑f).toFun y)) :
⇑{ toMonoidWithZeroHom := f, map_add_le_max' := h } = ⇑f
source
theorem Valuation.toFun_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
(↑v.toMonoidWithZeroHom).toFun = ⇑v
source
@[simp]
theorem Valuation.toMonoidWithZeroHom_coe_eq_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
⇑v.toMonoidWithZeroHom = ⇑v
source
theorem Valuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v₁ v₂ : Valuation R Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
v₁ = v₂
source
theorem Valuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v₁ v₂ : Valuation R Γ₀} :
v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
source
@[simp]
theorem Valuation.coe_coe {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
⇑↑v = ⇑v
source
theorem Valuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
v 0 = 0
source
theorem Valuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
v 1 = 1
source
theorem Valuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x y : R) :
v (x * y) = v x * v y
source
theorem Valuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x y : R) :
v (x + y) ≤ max (v x) (v y)
source
@[simp]
theorem Valuation.map_add' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x y : R) :
v (x + y) ≤ v x ∨ v (x + y) ≤ v y
source
theorem Valuation.map_add_le {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} {g : Γ₀} (hx : v x ≤ g) (hy : v y ≤ g) :
v (x + y) ≤ g
source
theorem Valuation.map_add_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} {g : Γ₀} (hx : v x < g) (hy : v y < g) :
v (x + y) < g
source
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 ∈ s, v (f i) ≤ g) :
v (∑ i ∈ s, f i) ≤ g
source
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 ∈ s, v (f i) < g) :
v (∑ i ∈ s, f i) < g
source
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 ∈ s, v (f i) < g) :
v (∑ i ∈ s, f i) < g
source
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
source
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

- v.toPreorder = Preorder.lift ⇑v

Instances For

source
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`.

source
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
source
theorem Valuation.pos_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K} :
0 < v x ↔ x ≠ 0
source
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
source
theorem Valuation.ne_zero_of_unit {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] (v : Valuation K Γ₀) (x : K ˣ) :
v ↑x ≠ 0
source
theorem Valuation.ne_zero_of_isUnit {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] (v : Valuation K Γ₀) (x : K) (hx : IsUnit x) :
v x ≠ 0
source
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

- Valuation.comap f v = { toFun := ⇑v ∘ ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

Instances For

source
@[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) :
(comap f v) s = v (f s)
source
@[simp]
theorem Valuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
comap (RingHom.id R) v = v
source
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) :
comap (g.comp f) v = comap f (comap g v)
source
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

- Valuation.map f hf v = { toFun := ⇑f ∘ ⇑v, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

Instances For

source
@[simp]
theorem Valuation.map_apply {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] (f : Γ₀ →*₀ Γ'₀) (hf : Monotone ⇑f) (v : Valuation R Γ₀) (r : R) :
(map f hf v) r = f (v r)
source
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

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

Instances For

source
@[simp]
theorem Valuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) :
v (-x) = v x
source
theorem Valuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x y : R) :
v (x - y) = v (y - x)
source
theorem Valuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x y : R) :
v (x - y) ≤ max (v x) (v y)
source
theorem Valuation.map_sub_le {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} {g : Γ₀} (hx : v x ≤ g) (hy : v y ≤ g) :
v (x - y) ≤ g
source
theorem Valuation.map_sub_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} {g : Γ₀} (hx : v x < g) (hy : v y < g) :
v (x - y) < g
source
@[simp]
theorem Valuation.le_one_of_subsingleton {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Subsingleton R] (v : Valuation R Γ₀) {x : R} :
v x ≤ 1
source
theorem Valuation.map_add_of_distinct_val {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v x ≠ v y) :
v (x + y) = max (v x) (v y)
source
theorem Valuation.map_add_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v x < v y) :
v (x + y) = v y
source
theorem Valuation.map_add_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v y < v x) :
v (x + y) = v x
source
theorem Valuation.map_sub_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v x < v y) :
v (x - y) = v y
source
theorem Valuation.map_sum_eq_of_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {ι : Type u_7} [DecidableEq ι] {s : Finset ι} {f : ι → R} {j : ι} (hj : j ∈ s) (hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)) :
v (∑ i ∈ s, f i) = v (f j)
source
theorem Valuation.map_sub_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v y < v x) :
v (x - y) = v x
source
theorem Valuation.map_eq_of_sub_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (h : v (y - x) < v x) :
v y = v x
source
theorem Valuation.map_sub_of_left_eq_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (hx : v x = 0) :
v (x - y) = v y
source
theorem Valuation.map_sub_of_right_eq_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (hy : v y = 0) :
v (x - y) = v x
source
theorem Valuation.map_add_of_left_eq_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (hx : v x = 0) :
v (x + y) = v y
source
theorem Valuation.map_add_of_right_eq_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} (hy : v y = 0) :
v (x + y) = v x
source
theorem Valuation.map_one_add_of_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x : R} (h : v x < 1) :
v (1 + x) = 1
source
theorem Valuation.map_one_sub_of_lt {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x : R} (h : v x < 1) :
v (1 - x) = 1
source
def Valuation.congr {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] (f : Γ₀ ≃*o Γ'₀) :
Valuation R Γ₀ ≃ Valuation R Γ'₀

An ordered monoid isomorphism `Γ₀ ≃ Γ'₀` induces an equivalence `Valuation R Γ₀ ≃ Valuation R Γ'₀`.

Equations

- Valuation.congr f = { toFun := Valuation.map ↑f ⋯, invFun := Valuation.map ↑f.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
instance Valuation.one (R : Type u_3) (Γ₀ : Type u_4) [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] :
One (Valuation R Γ₀)

The trivial valuation, sending everything to 1 other than 0.

Equations

- Valuation.one R Γ₀ = { one := let __spread.0 := 1; { toMonoidWithZeroHom := __spread.0, map_add_le_max' := ⋯ } }

source
theorem Valuation.one_apply_def {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] (x : R) :
1 x = if x = 0 then 0 else 1
source
@[simp]
theorem Valuation.toMonoidWithZeroHom_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] :
toMonoidWithZeroHom 1 = 1
source
theorem Valuation.one_apply_of_ne_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] {x : R} (hx : x ≠ 0) :
1 x = 1
source
@[simp]
theorem Valuation.one_apply_eq_zero_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] [Nontrivial Γ₀] {x : R} :
1 x = 0 ↔ x = 0
source
theorem Valuation.one_apply_le_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] (x : R) :
1 x ≤ 1
source
@[simp]
theorem Valuation.one_apply_lt_one_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] [Nontrivial Γ₀] {x : R} :
1 x < 1 ↔ x = 0
source
@[simp]
theorem Valuation.one_apply_eq_one_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] [Nontrivial Γ₀] {x : R} :
1 x = 1 ↔ x ≠ 0
source
theorem Valuation.map_inv {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_7} [DivisionRing R] (v : Valuation R Γ₀) (x : R) :
v x⁻¹ = (v x)⁻¹
source
theorem Valuation.map_div {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_7} [DivisionRing R] (v : Valuation R Γ₀) (x y : R) :
v (x / y) = v x / v y
source
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
source
theorem Valuation.one_le_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
source
theorem Valuation.val_lt_one_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) :
v x < 1 ↔ 1 < v x⁻¹
source
theorem Valuation.val_le_one_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) :
v x ≤ 1 ↔ 1 ≤ v x⁻¹
source
theorem Valuation.val_eq_one_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {x : K} :
v x = 1 ↔ v x⁻¹ = 1
source
theorem Valuation.val_le_one_or_val_inv_lt_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) (x : K) :
v x ≤ 1 ∨ v x⁻¹ < 1
source
theorem Valuation.val_le_one_or_val_inv_le_one {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) (x : K) :
v x ≤ 1 ∨ v x⁻¹ ≤ 1

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

source
def Valuation.leAddSubgroup {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀) :
AddSubgroup R

The subgroup of elements whose valuation is less than or equal to a certain value.

Equations

- v.leAddSubgroup γ = { carrier := {x : R | v x ≤ γ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source
@[simp]
theorem Valuation.mem_leAddSubgroup_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀} {x : R} :
x ∈ v.leAddSubgroup γ ↔ v x ≤ γ
source
theorem Valuation.leAddSubgroup_monotone {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :
Monotone v.leAddSubgroup
source
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

- v.ltAddSubgroup γ = { carrier := {x : R | v x < ↑γ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source
@[simp]
theorem Valuation.coe_ltAddSubgroup {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ ˣ) :
↑(v.ltAddSubgroup γ) = {x : R | v x < ↑γ}
source
@[simp]
theorem Valuation.mem_ltAddSubgroup_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀ ˣ} {x : R} :
x ∈ v.ltAddSubgroup γ ↔ v x < ↑γ
source
theorem Valuation.ltAddSubgroup_monotone {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :
Monotone v.ltAddSubgroup
source
theorem Valuation.ltAddSubgroup_le_leAddSubgroup {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ ˣ) :
v.ltAddSubgroup γ ≤ v.leAddSubgroup ↑γ
source
@[simp]
theorem Valuation.leAddSubgroup_zero {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_7} [Field K] (v : Valuation K Γ₀) :
v.leAddSubgroup 0 = ⊥
source
class Valuation.IsNontrivial {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
Prop

A valuation on a ring is nontrivial if there exists an element with valuation not equal to `0` or `1`.

- exists_val_nontrivial : ∃ (x : R), v x ≠ 0 ∧ v x ≠ 1

Instances

source
theorem Valuation.IsNontrivial.nontrivial_codomain {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.IsNontrivial] :
Nontrivial Γ₀
source
theorem Valuation.not_isNontrivial_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [IsDomain R] [DecidablePred fun (x : R) => x = 0] :
¬IsNontrivial 1
source
theorem Valuation.isNontrivial_iff_exists_unit {Γ₀ : Type u_4} [LinearOrderedCommMonoidWithZero Γ₀] {K : Type u_7} [Field K] {w : Valuation K Γ₀} :
w.IsNontrivial ↔ ∃ (x : K ˣ), w ↑x ≠ 1

For fields, being nontrivial is equivalent to the existence of a unit with valuation not equal to `1`.

source
theorem Valuation.IsNontrivial.exists_lt_one {K : Type u_7} [Field K] {Γ₀ : Type u_8} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation K Γ₀} [hv : v.IsNontrivial] :
∃ (x : K), v x ≠ 0 ∧ v x < 1
source
theorem Valuation.isNontrivial_iff_exists_lt_one {K : Type u_7} [Field K] {Γ₀ : Type u_8} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) :
v.IsNontrivial ↔ ∃ (x : K), x ≠ 0 ∧ v x < 1
source
theorem Valuation.IsNontrivial.exists_one_lt {K : Type u_7} [Field K] {Γ₀ : Type u_8} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation K Γ₀} [hv : v.IsNontrivial] :
∃ (x : K), v x ≠ 0 ∧ 1 < v x
source
theorem Valuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} :
v.IsEquiv v
source
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 : v₁.IsEquiv v₂) :
v₂.IsEquiv v₁
source
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₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) :
v₁.IsEquiv v₃
source
theorem Valuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v v' : Valuation R Γ₀} (h : v = v') :
v.IsEquiv v'
source
theorem Valuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone ⇑f) (inf : Function.Injective ⇑f) (h : v.IsEquiv v') :
(Valuation.map f hf v).IsEquiv (Valuation.map f hf v')
source
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 : v₁.IsEquiv v₂) :
(Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)

`comap` preserves equivalence.

source
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 : v₁.IsEquiv v₂) {r s : R} :
v₁ r = v₁ s ↔ v₂ r = v₂ s
source
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 : v₁.IsEquiv v₂) {r : R} :
v₁ r ≠ 0 ↔ v₂ r ≠ 0
source
theorem Valuation.IsEquiv.lt_iff_lt {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv v₂) {x y : R} :
v₁ x < v₁ y ↔ v₂ x < v₂ y
source
theorem Valuation.IsEquiv.le_one_iff_le_one {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv v₂) {x : R} :
v₁ x ≤ 1 ↔ v₂ x ≤ 1
source
theorem Valuation.IsEquiv.eq_one_iff_eq_one {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv v₂) {x : R} :
v₁ x = 1 ↔ v₂ x = 1
source
theorem Valuation.IsEquiv.lt_one_iff_lt_one {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} (h : v₁.IsEquiv v₂) {x : R} :
v₁ x < 1 ↔ v₂ x < 1
source
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) :
(map f ⋯ v).IsEquiv v
source
theorem Valuation.isEquiv_iff_val_lt_val {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} :
v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
source
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) :
v.IsEquiv v'
source
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 Γ'₀} :
v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
source
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 Γ'₀} :
v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
source
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 Γ'₀} :
v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1
source
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 Γ'₀} :
v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
source
theorem Valuation.IsEquiv.val_sub_one_lt_one_iff {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} :
v.IsEquiv v' → ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Alias of the forward direction of `Valuation.isEquiv_iff_val_sub_one_lt_one`.

source
theorem Valuation.isEquiv_tfae {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
[v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {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
source
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

- v.supp = { carrier := {x : R | v x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
@[simp]
theorem Valuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (x : R) :
x ∈ v.supp ↔ v x = 0
source
instance Valuation.instIsPrimeSuppOfNontrivialOfNoZeroDivisors {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Nontrivial Γ₀] [NoZeroDivisors Γ₀] :
v.supp.IsPrime

The support of a valuation is a prime ideal.

source
theorem Valuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (a : R) {s : R} (h : s ∈ v.supp) :
v (a + s) = v a
source
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) :
(comap f v).supp = Ideal.comap f v.supp
source
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 Γ₀ ᵒᵈ)

Instances For

source
instance AddValuation.instFunLike (R : Type u_6) (Γ₀ : Type u_7) [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
FunLike (AddValuation R Γ₀) R Γ₀

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

Equations

- AddValuation.instFunLike R Γ₀ = { coe := fun (v : AddValuation R Γ₀) => (↑v.toMonoidWithZeroHom).toFun, coe_injective' := ⋯ }

source
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 = { toFun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul, map_add_le_max' := hadd }

Instances For

source
@[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} :
(of f h0 h1 hadd hmul) r = f r
source
def AddValuation.toValuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
AddValuation R Γ₀ ≃ Valuation R (Multiplicative Γ₀ ᵒᵈ)

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

Equations

- AddValuation.toValuation = Equiv.refl (AddValuation R Γ₀)

Instances For

source
def AddValuation.ofValuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
Valuation R (Multiplicative Γ₀ ᵒᵈ) ≃ AddValuation R Γ₀

The `AddValuation` associated to a `Valuation`.

Equations

- AddValuation.ofValuation = Equiv.refl (Valuation R (Multiplicative Γ₀ ᵒᵈ))

Instances For

source
@[simp]
theorem AddValuation.ofValuation_symm_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
ofValuation.symm = toValuation
source
@[simp]
theorem AddValuation.toValuation_symm_eq {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] :
toValuation.symm = ofValuation
source
@[simp]
theorem AddValuation.ofValuation_toValuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
ofValuation (toValuation v) = v
source
@[simp]
theorem AddValuation.toValuation_ofValuation {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : Valuation R (Multiplicative Γ₀ ᵒᵈ)) :
toValuation (ofValuation v) = v
source
@[simp]
theorem AddValuation.toValuation_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (r : R) :
(toValuation v) r = Multiplicative.ofAdd (OrderDual.toDual (v r))
source
@[simp]
theorem AddValuation.ofValuation_apply {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : Valuation R (Multiplicative Γ₀ ᵒᵈ)) (r : R) :
(ofValuation v) r = OrderDual.ofDual (Multiplicative.toAdd (v r))
source
@[simp]
theorem AddValuation.map_zero {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
v 0 = ⊤
source
@[simp]
theorem AddValuation.map_one {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
v 1 = 0
source
@[deprecated "Use `⇑v` instead" (since := "2025-09-04")]
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.

Deprecated since it is unused.

Equations

- v.asFun = ⇑v

Instances For

source
@[simp]
theorem AddValuation.map_mul {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x y : R) :
v (x * y) = v x + v y
source
theorem AddValuation.map_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x y : R) :
min (v x) (v y) ≤ v (x + y)
source
@[simp]
theorem AddValuation.map_add' {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x y : R) :
v x ≤ v (x + y) ∨ v y ≤ v (x + y)
source
theorem AddValuation.map_le_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} {g : Γ₀} (hx : g ≤ v x) (hy : g ≤ v y) :
g ≤ v (x + y)
source
theorem AddValuation.map_lt_add {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} {g : Γ₀} (hx : g < v x) (hy : g < v y) :
g < v (x + y)
source
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 ∈ s, g ≤ v (f i)) :
g ≤ v (∑ i ∈ s, f i)
source
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 ∈ s, g < v (f i)) :
g < v (∑ i ∈ s, f i)
source
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 ∈ s, g < v (f i)) :
g < v (∑ i ∈ s, f i)
source
@[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
source
theorem AddValuation.ext {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {v₁ v₂ : AddValuation R Γ₀} (h : ∀ (r : R), v₁ r = v₂ r) :
v₁ = v₂
source
theorem AddValuation.ext_iff {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {v₁ v₂ : AddValuation R Γ₀} :
v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
source
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

- v.toPreorder = Preorder.lift ⇑v

Instances For

source
@[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`.

source
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
source
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

Instances For

source
@[simp]
theorem AddValuation.comap_id {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) :
comap (RingHom.id R) v = v
source
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) :
comap (g.comp f) v = comap f (comap g v)
source
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

- AddValuation.map f ht hf v = Valuation.map { toFun := ⇑f, map_zero' := ht, map_one' := ⋯, map_mul' := ⋯ } ⋯ v

Instances For

source
@[simp]
theorem AddValuation.map_apply {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone ⇑f) (v : AddValuation R Γ₀) (r : R) :
(map f ht hf v) r = f (v r)
source
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

- v₁.IsEquiv v₂ = Valuation.IsEquiv v₁ v₂

Instances For

source
@[simp]
theorem AddValuation.map_neg {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x : R) :
v (-x) = v x
source
theorem AddValuation.map_sub_swap {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x y : R) :
v (x - y) = v (y - x)
source
theorem AddValuation.map_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) (x y : R) :
min (v x) (v y) ≤ v (x - y)
source
theorem AddValuation.map_le_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} {g : Γ₀} (hx : g ≤ v x) (hy : g ≤ v y) :
g ≤ v (x - y)
source
theorem AddValuation.map_add_of_distinct_val {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (h : v x ≠ v y) :
v (x + y) = min (v x) (v y)
source
theorem AddValuation.map_add_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (h : v x < v y) :
v (x + y) = v x
source
theorem AddValuation.map_add_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (hx : v y < v x) :
v (x + y) = v y
source
theorem AddValuation.map_sub_eq_of_lt_left {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (hx : v x < v y) :
v (x - y) = v x
source
theorem AddValuation.map_sub_eq_of_lt_right {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (hx : v y < v x) :
v (x - y) = v y
source
theorem AddValuation.map_eq_of_lt_sub {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀) {x y : R} (h : v x < v (y - x)) :
v y = v x
source
@[simp]
theorem AddValuation.map_inv {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] (v : AddValuation K Γ₀) {x : K} :
v x⁻¹ = -v x
source
@[simp]
theorem AddValuation.map_div {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} [LinearOrderedAddCommGroupWithTop Γ₀] (v : AddValuation K Γ₀) {x y : K} :
v (x / y) = v x - v y
source
theorem AddValuation.IsEquiv.refl {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Ring R] {v : AddValuation R Γ₀} :
v.IsEquiv v
source
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 : v₁.IsEquiv v₂) :
v₂.IsEquiv v₁
source
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₁₂ : v₁.IsEquiv v₂) (h₂₃ : v₂.IsEquiv v₃) :
v₁.IsEquiv v₃
source
theorem AddValuation.IsEquiv.of_eq {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [Ring R] {v v' : AddValuation R Γ₀} (h : v = v') :
v.IsEquiv v'
source
theorem AddValuation.IsEquiv.map {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedAddCommMonoidWithTop Γ₀] [LinearOrderedAddCommMonoidWithTop Γ'₀] [Ring R] {v v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone ⇑f) (inf : Function.Injective ⇑f) (h : v.IsEquiv v') :
(AddValuation.map f ht hf v).IsEquiv (AddValuation.map f ht hf v')
source
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 : v₁.IsEquiv v₂) :
(AddValuation.comap f v₁).IsEquiv (AddValuation.comap f v₂)

`comap` preserves equivalence.

source
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 : v₁.IsEquiv v₂) {r s : R} :
v₁ r = v₁ s ↔ v₂ r = v₂ s
source
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 : v₁.IsEquiv v₂) {r : R} :
v₁ r ≠ ⊤ ↔ v₂ r ≠ ⊤
source
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

- v.supp = Valuation.supp v

Instances For

source
@[simp]
theorem AddValuation.mem_supp_iff {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) (x : R) :
x ∈ v.supp ↔ v x = ⊤
source
theorem AddValuation.map_add_supp {R : Type u_3} {Γ₀ : Type u_4} [LinearOrderedAddCommMonoidWithTop Γ₀] [CommRing R] (v : AddValuation R Γ₀) (a : R) {s : R} (h : s ∈ v.supp) :
v (a + s) = v a
source
def Valuation.toAddValuation {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
Valuation R Γ₀ ≃ AddValuation R (Additive Γ₀)ᵒᵈ

The `AddValuation` associated to a `Valuation`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Valuation.ofAddValuation {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
AddValuation R (Additive Γ₀)ᵒᵈ ≃ Valuation R Γ₀

The `Valuation` associated to a `AddValuation`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Valuation.ofAddValuation_symm_eq {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
ofAddValuation.symm = toAddValuation
source
@[simp]
theorem Valuation.toAddValuation_symm_eq {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] :
toAddValuation.symm = ofAddValuation
source
@[simp]
theorem Valuation.ofAddValuation_toAddValuation {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
ofAddValuation (toAddValuation v) = v
source
@[simp]
theorem Valuation.toValuation_ofValuation {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : AddValuation R (Additive Γ₀)ᵒᵈ) :
toAddValuation (ofAddValuation v) = v
source
@[simp]
theorem Valuation.toAddValuation_apply {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (r : R) :
(toAddValuation v) r = OrderDual.toDual (Additive.ofMul (v r))
source
@[simp]
theorem Valuation.ofAddValuation_apply {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : AddValuation R (Additive Γ₀)ᵒᵈ) (r : R) :
(ofAddValuation v) r = Additive.toMul (OrderDual.ofDual (v r))
source
instance Valuation.instCommMonoidWithZeroSubtypeMemSubmonoidMrange {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
CommMonoidWithZero ↥(MonoidHom.mrange v)
Equations

- v.instCommMonoidWithZeroSubtypeMemSubmonoidMrange = inferInstanceAs (CommMonoidWithZero ↥(MonoidHom.mrange ↑v))

source
@[simp]
theorem Valuation.val_mrange_zero {R : Type u_3} {Γ₀ : Type u_5} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) :
↑0 = 0
source
instance Valuation.instCommGroupWithZeroSubtypeMemSubmonoidMrange {K : Type u_4} {Γ₀ : Type u_6} [LinearOrderedCommGroupWithZero Γ₀] [DivisionRing K] (v : Valuation K Γ₀) :
CommGroupWithZero ↥(MonoidHom.mrange v)
Equations

- v.instCommGroupWithZeroSubtypeMemSubmonoidMrange = inferInstanceAs (CommGroupWithZero ↥(MonoidHom.mrange ↑v))