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 valution 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 [ValuativeTopology 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) : rel x y ∨ rel y x
• rel_trans {z y x : R} : rel x y → rel y z → rel x z
• rel_add {x y z : R} : rel x z → rel y z → rel (x + y) z
• rel_mul_right {x y : R} (z : R) : rel x y → rel (x * z) (y * z)
• rel_mul_cancel {x y z : R} : ¬rel z 0 → rel (x * z) (y * z) → rel x y
• not_rel_one_zero : ¬rel 1 0

def valuativeRel : Lean.TrailingParserDescr

The relation operator arising from ValuativeRel.

Equations

• valuativeRel = Lean.ParserDescr.trailingNode `valuativeRel 50 50 (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) : ValuativeRel.rel 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) : ValuativeRel.rel x y ↔ x ≤ y

@[simp]

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

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

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

Alias of ValuativeRel.rel_refl.

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

Alias of ValuativeRel.rel_rfl.

@[simp]

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

theorem ValuativeRel.rel_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (z : R) : rel x y → rel (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} : rel x y → rel y z → rel x z

Alias of ValuativeRel.rel_trans.

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

theorem ValuativeRel.rel.trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : rel y z) (h2 : rel x y) : rel 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 : rel x y) (h2 : rel x' y') : rel (x * x') (y * y')

theorem ValuativeRel.rel_add_cases {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : rel (x + y) x ∨ rel (x + y) 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 | ¬ValuativeRel.rel x 0}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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₁ : rel (x * ↑s) (y * ↑t)) (h₂ : rel (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) : rel (x * ↑s) (y * ↑t) ∧ rel (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)), rel (x * ↑t) (y * ↑s) → rel (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)), rel (x * ↑t) (y * ↑s) → rel (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)), rel (x * ↑t) (y * ↑s) → rel (y * ↑s) (x * ↑t) → rel (z * ↑u) (w * ↑v) → rel (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)), rel (x * ↑t) (y * ↑s) → rel (y * ↑s) (x * ↑t) → rel (z * ↑u) (w * ↑v) → rel (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 ↔ rel (x * ↑s) (y * ↑t) ∧ rel (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 ↔ rel 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 ↔ rel x ↑y ∧ rel (↑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)), rel (x * ↑t) (y * ↑s) → rel (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)), rel (x * ↑t) (y * ↑s) → rel (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)), rel (x * ↑t) (y * ↑s) → rel (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 ↔ rel (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 ↔ rel (x * ↑s) (y * ↑t) ∧ ¬rel (y * ↑t) (x * ↑s)

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 : ¬rel 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)), rel (x * ↑t) (y * ↑s) → rel (y * ↑s) (x * ↑t) → f x s = f y t) (x : R) : ValueGroupWithZero.lift f hf ((valuation R) x) = f x 1

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₂

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) => ValuativeRel.rel 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 valutaive 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 | ValuativeRel.rel 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 ↔ rel 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 IsRankOne.

• 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] : IsNontrivial R ↔ (valuation R).IsNontrivial

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, δ ≤ γ

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

class ValuativeTopology (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) : s ∈ nhds 0 ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {x : R | (ValuativeRel.valuation R) x < ↑γ} ⊆ s

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) : ValuativeRel.rel ((algebraMap A B) a) ((algebraMap A B) b) ↔ ValuativeRel.rel 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✝

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

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

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