Valuative Relations

In this file we introduce a class called ValuativeRel R for a ring R. This bundles a relation rel : R → R → Prop on R which mimics a preorder on R arising from a valuation. We introduce the notation x ≤ᵥ y for this relation.

Recall that the equivalence class of a valuation is completely characterized by such a preorder. Thus, we can think of ValuativeRel R as a way of saying that R is endowed with an equivalence class of valuations.

Main Definitions

• ValuativeRel R endows a commutative ring R with a relation arising from a valuation. This is equivalent to fixing an equivalence class of valuations on R. Use the notation x ≤ᵥ y for this relation.
• ValuativeRel.valuation R is the "canonical" valuation associated to ValuativeRel R, taking values in ValuativeRel.ValueGroupWithZero R.
• Given a valuation v on R and an instance [ValuativeRel R], writing [v.Compatible] ensures that the relation x ≤ᵥ y is equivalent to v x ≤ v y. Note that it is possible to have [v.Compatible] and [w.Compatible] for two different valuations on R.
• If we have both [ValuativeRel R] and [TopologicalSpace R], then writing [IsValuativeTopology R] ensures that the topology on R agrees with the one induced by the valuation.
• Given [ValuativeRel A], [ValuativeRel B] and [Algebra A B], the class [ValuativeExtension A B] ensures that the algebra map A → B is compatible with the valuations on A and B. For example, this can be used to talk about extensions of valued fields.

Remark

The last two axioms in ValuativeRel, namely rel_mul_cancel and not_rel_one_zero, are used to ensure that we have a well-behaved valuation taking values in a value group (with zero). In principle, it should be possible to drop these two axioms and obtain a value monoid, however, such a value monoid would not necessarily embed into an ordered abelian group with zero. Similarly, without these axioms, the support of the valuation need not be a prime ideal. We have thus opted to include these two axioms and obtain a ValueGroupWithZero associated to a ValuativeRel in order to best align with the literature about valuations on commutative rings.

Future work could refactor ValuativeRel by dropping the rel_mul_cancel and not_rel_one_zero axioms, opting to make these mixins instead.

Projects

The ValuativeRel class should eventually replace the existing Valued typeclass. Once such a refactor happens, ValuativeRel could be renamed to Valued.

class ValuativeRel (R : Type u_1) [CommRing R] : Type u_1

The class [ValuativeRel R] class introduces an operator x ≤ᵥ y : Prop for x y : R which is the natural relation arising from (the equivalence class of) a valuation on R. More precisely, if v is a valuation on R then the associated relation is x ≤ᵥ y ↔ v x ≤ v y. Use this class to talk about the case where R is equipped with an equivalence class of valuations.

• rel : R → R → Prop

  The relation operator arising from ValuativeRel.

• rel_total (x y : R) : x ≤ᵥ y ∨ y ≤ᵥ x
• rel_trans {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z
• rel_add {x y z : R} : x ≤ᵥ z → y ≤ᵥ z → x + y ≤ᵥ z
• rel_mul_right {x y : R} (z : R) : x ≤ᵥ y → x * z ≤ᵥ y * z
• rel_mul_cancel {x y z : R} : ¬z ≤ᵥ 0 → x * z ≤ᵥ y * z → x ≤ᵥ y
• not_rel_one_zero : ¬1 ≤ᵥ 0

theorem ValuativeRel.ext {R : Type u_1} {inst✝ : CommRing R} {x y : ValuativeRel R} (rel : rel = rel) : x = y

theorem ValuativeRel.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : ValuativeRel R} : x = y ↔ rel = rel

def «term_≤ᵥ_» : Lean.TrailingParserDescr

The relation operator arising from ValuativeRel.

Equations

• «term_≤ᵥ_» = Lean.ParserDescr.trailingNode `«term_≤ᵥ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ᵥ ") (Lean.ParserDescr.cat `term 51))

class Valuation.Compatible {R : Type u_1} {Γ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ) [ValuativeRel R] : Prop

We say that a valuation v is Compatible if the relation x ≤ᵥ y is equivalent to v x ≤ x y.

• rel_iff_le (x y : R) : x ≤ᵥ y ↔ v x ≤ v y

class ValuativePreorder (R : Type u_1) [CommRing R] [ValuativeRel R] [Preorder R] : Prop

A preorder on a ring is said to be "valuative" if it agrees with the valuative relation.

• rel_iff_le (x y : R) : x ≤ᵥ y ↔ x ≤ y

def ValuativeRel.srel {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : Prop

The strict version of the valuative relation.

Equations

• (x <ᵥ y) = ¬y ≤ᵥ x

def ValuativeRel.«term_<ᵥ_» : Lean.TrailingParserDescr

The strict version of the valuative relation.

Equations

• ValuativeRel.«term_<ᵥ_» = Lean.ParserDescr.trailingNode `ValuativeRel.«term_<ᵥ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᵥ ") (Lean.ParserDescr.cat `term 51))

theorem ValuativeRel.srel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : x <ᵥ y ↔ ¬y ≤ᵥ x

@[simp]

theorem ValuativeRel.not_srel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : ¬x <ᵥ y ↔ y ≤ᵥ x

@[simp]

theorem ValuativeRel.rel_refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

theorem ValuativeRel.rel_rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

theorem ValuativeRel.rel.refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

Alias of ValuativeRel.rel_refl.

theorem ValuativeRel.rel.rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

Alias of ValuativeRel.rel_rfl.

@[simp]

theorem ValuativeRel.zero_rel {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : 0 ≤ᵥ x

@[simp]

theorem ValuativeRel.zero_srel_one {R : Type u_1} [CommRing R] [ValuativeRel R] : 0 <ᵥ 1

theorem ValuativeRel.rel_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (z : R) : x ≤ᵥ y → z * x ≤ᵥ z * y

instance ValuativeRel.instTransRel {R : Type u_1} [CommRing R] [ValuativeRel R] : Trans rel rel rel

Equations

• ValuativeRel.instTransRel = { trans := ⋯ }

theorem ValuativeRel.rel.trans {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z

Alias of ValuativeRel.rel_trans.

theorem ValuativeRel.rel_trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

theorem ValuativeRel.rel.trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

Alias of ValuativeRel.rel_trans'.

theorem ValuativeRel.rel_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y'

theorem ValuativeRel.rel_add_cases {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : x + y ≤ᵥ x ∨ x + y ≤ᵥ y

theorem ValuativeRel.zero_srel_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y

def ValuativeRel.posSubmonoid (R : Type u_1) [CommRing R] [ValuativeRel R] : Submonoid R

The submonoid of elements x : R whose valuation is positive.

Equations

• ValuativeRel.posSubmonoid R = { carrier := {x : R | 0 <ᵥ x}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem ValuativeRel.posSubmonoid_def {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ∈ posSubmonoid R ↔ 0 <ᵥ x

@[simp]

theorem ValuativeRel.right_cancel_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (u : ↥(posSubmonoid R)) : x * ↑u ≤ᵥ y * ↑u ↔ x ≤ᵥ y

@[simp]

theorem ValuativeRel.left_cancel_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (u : ↥(posSubmonoid R)) : ↑u * x ≤ᵥ ↑u * y ↔ x ≤ᵥ y

@[simp]

theorem ValuativeRel.val_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ↑x ≠ 0

def ValuativeRel.valueSetoid (R : Type u_1) [CommRing R] [ValuativeRel R] : Setoid (R × ↥(posSubmonoid R))

The setoid used to construct ValueGroupWithZero R.

Equations

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

def ValuativeRel.ValueGroupWithZero (R : Type u_1) [CommRing R] [ValuativeRel R] : Type u_1

The "canonical" value group-with-zero of a ring with a valuative relation.

Equations

• ValuativeRel.ValueGroupWithZero R = Quotient (ValuativeRel.valueSetoid R)

def ValuativeRel.ValueGroupWithZero.mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero R

Construct an element of the value group-with-zero from an element r : R and y : posSubmonoid R. This should be thought of as v r / v y.

Equations

• ValuativeRel.ValueGroupWithZero.mk x y = ⟦(x, y)⟧

theorem ValuativeRel.ValueGroupWithZero.sound {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} (h₁ : x * ↑s ≤ᵥ y * ↑t) (h₂ : y * ↑t ≤ᵥ x * ↑s) : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s

theorem ValuativeRel.ValueGroupWithZero.exact {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} (h : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s) : x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s

theorem ValuativeRel.ValueGroupWithZero.ind {R : Type u_1} [CommRing R] [ValuativeRel R] {motive : ValueGroupWithZero R → Prop} (mk : ∀ (x : R) (y : ↥(posSubmonoid R)), motive (ValueGroupWithZero.mk x y)) (t : ValueGroupWithZero R) : motive t

def ValuativeRel.ValueGroupWithZero.lift {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (t : ValueGroupWithZero R) : α

Lifts a function R → posSubmonoid R → α to the value group-with-zero of R.

Equations

• ValuativeRel.ValueGroupWithZero.lift f hf t = Quotient.lift (fun (x : R × ↥(ValuativeRel.posSubmonoid R)) => match x with | (x, y) => f x y) ⋯ t

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) = f x y

def ValuativeRel.ValueGroupWithZero.lift₂ {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → R → ↥(posSubmonoid R) → α) (hf : ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u) (t₁ t₂ : ValueGroupWithZero R) : α

Lifts a function R → posSubmonoid R → R → posSubmonoid R → α to the value group-with-zero of R.

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift₂_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → R → ↥(posSubmonoid R) → α) (hf : ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u) (x y : R) (z w : ↥(posSubmonoid R)) : ValueGroupWithZero.lift₂ f hf (ValueGroupWithZero.mk x z) (ValueGroupWithZero.mk y w) = f x z y w

theorem ValuativeRel.ValueGroupWithZero.mk_eq_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s

instance ValuativeRel.instZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Zero (ValueGroupWithZero R)

Equations

• ValuativeRel.instZeroValueGroupWithZero = { zero := ValuativeRel.ValueGroupWithZero.mk 0 1 }

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_eq_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x y = 0 ↔ x ≤ᵥ 0

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ValueGroupWithZero.mk 0 x = 0

instance ValuativeRel.instOneValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : One (ValueGroupWithZero R)

Equations

• ValuativeRel.instOneValueGroupWithZero = { one := ValuativeRel.ValueGroupWithZero.mk 1 1 }

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_self {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ValueGroupWithZero.mk (↑x) x = 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_one_one {R : Type u_1} [CommRing R] [ValuativeRel R] : ValueGroupWithZero.mk 1 1 = 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_eq_one {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ ↑y ∧ ↑y ≤ᵥ x

theorem ValuativeRel.ValueGroupWithZero.lift_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) : ValueGroupWithZero.lift f hf 0 = f 0 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_one {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) : ValueGroupWithZero.lift f hf 1 = f 1 1

instance ValuativeRel.instMulValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Mul (ValueGroupWithZero R)

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_mul_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (a b : R) (c d : ↥(posSubmonoid R)) : ValueGroupWithZero.mk a c * ValueGroupWithZero.mk b d = ValueGroupWithZero.mk (a * b) (c * d)

theorem ValuativeRel.ValueGroupWithZero.lift_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Type u_2} [Mul α] (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s) (a b : ValueGroupWithZero R) : ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

instance ValuativeRel.instCommMonoidWithZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : CommMonoidWithZero (ValueGroupWithZero R)

Equations

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

instance ValuativeRel.instLEValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LE (ValueGroupWithZero R)

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_le_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (t s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x t ≤ ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t

instance ValuativeRel.instLinearOrderValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LinearOrder (ValueGroupWithZero R)

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_lt_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (t s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * ↑s <ᵥ y * ↑t

instance ValuativeRel.instBotValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Bot (ValueGroupWithZero R)

Equations

• ValuativeRel.instBotValueGroupWithZero = { bot := 0 }

theorem ValuativeRel.ValueGroupWithZero.bot_eq_zero {R : Type u_1} [CommRing R] [ValuativeRel R] : ⊥ = 0

instance ValuativeRel.instOrderBotValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : OrderBot (ValueGroupWithZero R)

Equations

• ValuativeRel.instOrderBotValueGroupWithZero = { toBot := ValuativeRel.instBotValueGroupWithZero, bot_le := ⋯ }

instance ValuativeRel.instIsOrderedMonoidValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : IsOrderedMonoid (ValueGroupWithZero R)

instance ValuativeRel.instInvValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Inv (ValueGroupWithZero R)

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.inv_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) (hx : ¬x ≤ᵥ 0) : (ValueGroupWithZero.mk x y)⁻¹ = ValueGroupWithZero.mk ↑y ⟨x, hx⟩

instance ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LinearOrderedCommGroupWithZero (ValueGroupWithZero R)

The value group-with-zero is a linearly ordered commutative group with zero.

Equations

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

def ValuativeRel.valuation (R : Type u_1) [CommRing R] [ValuativeRel R] : Valuation R (ValueGroupWithZero R)

The "canonical" valuation associated to a valuative relation.

Equations

• ValuativeRel.valuation R = { toFun := fun (r : R) => ValuativeRel.ValueGroupWithZero.mk r 1, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

instance ValuativeRel.instCompatibleValueGroupWithZeroValuation {R : Type u_1} [CommRing R] [ValuativeRel R] : (valuation R).Compatible

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_valuation {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (x : R) : ValueGroupWithZero.lift f hf ((valuation R) x) = f x 1

theorem ValuativeRel.valuation_eq_zero_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : (valuation R) x = 0 ↔ x ≤ᵥ 0

theorem ValuativeRel.valuation_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : (valuation R) ↑x ≠ 0

theorem ValuativeRel.ValueGroupWithZero.mk_eq_div {R : Type u_1} [CommRing R] [ValuativeRel R] (r : R) (s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk r s = (valuation R) r / (valuation R) ↑s

def ValuativeRel.ofValuation {S : Type u_2} {Γ : Type u_3} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : ValuativeRel S

Construct a valuative relation on a ring using a valuation.

Equations

• ValuativeRel.ofValuation v = { rel := fun (x y : S) => v x ≤ v y, rel_total := ⋯, rel_trans := ⋯, rel_add := ⋯, rel_mul_right := ⋯, rel_mul_cancel := ⋯, not_rel_one_zero := ⋯ }

theorem Valuation.Compatible.ofValuation {S : Type u_2} {Γ : Type u_3} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : v.Compatible

theorem ValuativeRel.isEquiv {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₁ : Type u_2} {Γ₂ : Type u_3} [LinearOrderedCommMonoidWithZero Γ₁] [LinearOrderedCommMonoidWithZero Γ₂] (v₁ : Valuation R Γ₁) (v₂ : Valuation R Γ₂) [v₁.Compatible] [v₂.Compatible] : v₁.IsEquiv v₂

theorem Valuation.Compatible.srel_iff_lt {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} [v.Compatible] {x y : R} : x <ᵥ y ↔ v x < v y

@[simp]

theorem Valuation.apply_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ : Type u_2} [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)) : v ↑x ≠ 0

@[deprecated Valuation.apply_posSubmonoid_ne_zero (since := "2025-08-06")]

theorem ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatible {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ : Type u_2} [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : ↥(posSubmonoid R)) : v ↑x ≠ 0

Alias of Valuation.apply_posSubmonoid_ne_zero.

@[simp]

theorem Valuation.apply_posSubmonoid_pos {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ : Type u_2} [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)) : 0 < v ↑x

def ValuativeRel.WithPreorder (R : Type u_1) : Type u_1

An alias for endowing a ring with a preorder defined as the valuative relation.

Equations

• ValuativeRel.WithPreorder R = R

instance ValuativeRel.instCommRingWithPreorder {R : Type u_1} [CommRing R] : CommRing (WithPreorder R)

The ring instance on WithPreorder R arising from the ring structure on R.

Equations

• ValuativeRel.instCommRingWithPreorder = inferInstanceAs (CommRing R)

instance ValuativeRel.instPreorderWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : Preorder (WithPreorder R)

The preorder on WithPreorder R arising from the valuative relation on R.

Equations

• ValuativeRel.instPreorderWithPreorder = { le := fun (x y : R) => x ≤ᵥ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance ValuativeRel.instWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : ValuativeRel (WithPreorder R)

The valuative relation on WithPreorder R arising from the valuative relation on R. This is defined as the preorder itself.

Equations

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

instance ValuativeRel.instValuativePreorderWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : ValuativePreorder (WithPreorder R)

def ValuativeRel.supp (R : Type u_1) [CommRing R] [ValuativeRel R] : Ideal R

The support of the valuation on R.

Equations

• ValuativeRel.supp R = { carrier := {x : R | x ≤ᵥ 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem ValuativeRel.supp_def {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ∈ supp R ↔ x ≤ᵥ 0

theorem ValuativeRel.supp_eq_valuation_supp {R : Type u_1} [CommRing R] [ValuativeRel R] : supp R = (valuation R).supp

instance ValuativeRel.instIsPrimeSupp {R : Type u_1} [CommRing R] [ValuativeRel R] : (supp R).IsPrime

structure ValuativeRel.RankLeOneStruct (R : Type u_1) [CommRing R] [ValuativeRel R] : Type u_1

An auxiliary structure used to define IsRankLeOne.

• emb : ValueGroupWithZero R →*₀ NNReal

  The embedding of the value group-with-zero into the nonnegative reals.

• strictMono : StrictMono ⇑self.emb

class ValuativeRel.IsRankLeOne (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

We say that a ring with a valuative relation is of rank one if there exists a strictly monotone embedding of the "canonical" value group-with-zero into the nonnegative reals, and the image of this embedding contains some element different from 0 and 1.

• nonempty : Nonempty (RankLeOneStruct R)

class ValuativeRel.IsNontrivial (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

We say that a valuative relation on a ring is nontrivial if the value group-with-zero is nontrivial, meaning that it has an element which is different from 0 and 1.

• condition : ∃ (γ : ValueGroupWithZero R), γ ≠ 0 ∧ γ ≠ 1

theorem ValuativeRel.isNontrivial_iff_nontrivial_units {R : Type u_1} [CommRing R] [ValuativeRel R] : IsNontrivial R ↔ Nontrivial (ValueGroupWithZero R)ˣ

theorem ValuativeRel.isNontrivial_iff_isNontrivial {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] : IsNontrivial R ↔ v.IsNontrivial

instance ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] [IsNontrivial R] (v : Valuation R Γ₀) [v.Compatible] : v.IsNontrivial

theorem ValuativeRel.ValueGroupWithZero.mk_eq_valuation {K : Type u_2} [Field K] [ValuativeRel K] (x : K) (y : ↥(posSubmonoid K)) : ValueGroupWithZero.mk x y = (valuation K) (x / ↑y)

theorem ValuativeRel.exists_valuation_div_valuation_eq {R : Type u_1} [CommRing R] [ValuativeRel R] (γ : ValueGroupWithZero R) : ∃ (a : R) (b : ↥(posSubmonoid R)), (valuation R) a / (valuation R) ↑b = γ

theorem ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq {R : Type u_1} [CommRing R] [ValuativeRel R] (γ : (ValueGroupWithZero R)ˣ) : ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)), (valuation R) ↑a / (valuation R) ↑b = ↑γ

theorem ValuativeRel.valuation_surjective {K : Type u_2} [Field K] [ValuativeRel K] : Function.Surjective ⇑(valuation K)

class ValuativeRel.IsDiscrete (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

A ring with a valuative relation is discrete if its value group-with-zero has a maximal element < 1.

• has_maximal_element : ∃ γ < 1, ∀ δ < 1, δ ≤ γ

class IsValuativeTopology (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] : Prop

We say that a topology on R is valuative if the neighborhoods of 0 in R are determined by the relation · ≤ᵥ ·.

• mem_nhds_iff {s : Set R} {x : R} : s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), (fun (x_1 : R) => x + x_1) '' {z : R | (ValuativeRel.valuation R) z < ↑γ} ⊆ s

@[deprecated IsValuativeTopology (since := "2025-08-01")]

def ValuativeTopology (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] : Prop

Alias of IsValuativeTopology.

---

We say that a topology on R is valuative if the neighborhoods of 0 in R are determined by the relation · ≤ᵥ ·.

Equations

• ValuativeTopology = IsValuativeTopology

noncomputable def ValuativeRel.ValueGroupWithZero.embed {R : Type u_1} {Γ : Type u_2} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [h : v.Compatible] : ValueGroupWithZero R →*₀ Γ

Any valuation compatible with the valuative relation can be factored through the value group.

Equations

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

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embed_mk {R : Type u_1} {Γ : Type u_2} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : R) (s : ↥(posSubmonoid R)) : (embed v) (ValueGroupWithZero.mk x s) = v x / v ↑s

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embed_valuation {R : Type u_1} [CommRing R] [ValuativeRel R] (γ : ValueGroupWithZero R) : (embed (valuation R)) γ = γ

theorem ValuativeRel.ValueGroupWithZero.embed_strictMono {R : Type u_1} {Γ : Type u_2} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] : StrictMono ⇑(embed v)

theorem ValuativeRel.one_apply_posSubmonoid {R : Type u_1} {Γ : Type u_2} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] (x : ↥(posSubmonoid R)) : 1 ↑x = 1

For any x ∈ posSubmonoid R, the trivial valuation 1 : Valuation R Γ sends x to 1. In fact, this is true for any x ≠ 0. This lemma is a special case useful for shorthand of x ∈ posSubmonoid R → x ≠ 0.

class ValuativeExtension (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] : Prop

If B is an A algebra and both A and B have valuative relations, we say that B|A is a valuative extension if the valuative relation on A is induced by the one on B.

• rel_iff_rel (a b : A) : (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b

theorem ValuativeExtension.srel_iff_srel {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (a b : A) : (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b

def ValuativeExtension.mapPosSubmonoid (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : ↥(ValuativeRel.posSubmonoid A) →* ↥(ValuativeRel.posSubmonoid B)

The morphism of posSubmonoids associated to an algebra map. This is used in constructing ValuativeExtension.mapValueGroupWithZero.

Equations

• ValuativeExtension.mapPosSubmonoid A B = { toFun := fun (x : ↥(ValuativeRel.posSubmonoid A)) => match x with | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ValuativeExtension.mapPosSubmonoid_apply_coe (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (x✝ : ↥(ValuativeRel.posSubmonoid A)) : ↑((mapPosSubmonoid A B) x✝) = (algebraMap A B) ↑x✝

instance ValuativeExtension.compatible_comap (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] {Γ : Type u_3} [LinearOrderedCommMonoidWithZero Γ] (w : Valuation B Γ) [w.Compatible] : (Valuation.comap (algebraMap A B) w).Compatible

def ValuativeExtension.mapValueGroupWithZero (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : ValuativeRel.ValueGroupWithZero A →*₀ ValuativeRel.ValueGroupWithZero B

The map on value groups-with-zero associated to the structure morphism of an algebra.

Equations

• ValuativeExtension.mapValueGroupWithZero A B = ValuativeRel.ValueGroupWithZero.embed (Valuation.comap (algebraMap A B) (ValuativeRel.valuation B))

@[simp]

theorem ValuativeExtension.mapValueGroupWithZero_mk {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (r : A) (s : ↥(ValuativeRel.posSubmonoid A)) : (mapValueGroupWithZero A B) (ValuativeRel.ValueGroupWithZero.mk r s) = ValuativeRel.ValueGroupWithZero.mk ((algebraMap A B) r) ((mapPosSubmonoid A B) s)

@[simp]

theorem ValuativeExtension.mapValueGroupWithZero_valuation {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (a : A) : (mapValueGroupWithZero A B) ((ValuativeRel.valuation A) a) = (ValuativeRel.valuation B) ((algebraMap A B) a)

instance ValuativeRel.instMulArchimedeanValueGroupWithZeroOfIsRankLeOne {R : Type u_1} [CommRing R] [ValuativeRel R] [IsRankLeOne R] : MulArchimedean (ValueGroupWithZero R)

Any rank-at-most-one valuation has a mul-archimedean value group. The converse (for any compatible valuation) is ValuativeRel.isRankLeOne_iff_mulArchimedean which is in a later file since it requires a larger theory of reals.