Rank one valuations

We define rank one valuations.

Main Definitions

• RankOne : A valuation v has rank one if it is nontrivial and its image is contained in ℝ≥0. Note that this class contains the data of the inclusion of the codomain of v into ℝ≥0.

Tags

valuation, rank one

class Valuation.RankOne {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Type u_2

A valuation has rank one if it is nontrivial and its image is contained in ℝ≥0. Note that this class includes the data of an inclusion morphism Γ₀ → ℝ≥0.

• hom : Γ₀ →*₀ NNReal

  The inclusion morphism from Γ₀ to ℝ≥0.

• strictMono' : StrictMono ⇑(Valuation.RankOne.hom v)
• nontrivial' : ∃ (r : R), v r ≠ 0 ∧ v r ≠ 1

theorem Valuation.RankOne.strictMono' {R : Type u_1} : ∀ {inst : Ring R} {Γ₀ : Type u_2} {inst_1 : LinearOrderedCommGroupWithZero Γ₀} {v : Valuation R Γ₀} [self : v.RankOne], StrictMono ⇑(Valuation.RankOne.hom v)

theorem Valuation.RankOne.nontrivial' {R : Type u_1} : ∀ {inst : Ring R} {Γ₀ : Type u_2} {inst_1 : LinearOrderedCommGroupWithZero Γ₀} {v : Valuation R Γ₀} [self : v.RankOne], ∃ (r : R), v r ≠ 0 ∧ v r ≠ 1

theorem Valuation.RankOne.strictMono {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] : StrictMono ⇑(Valuation.RankOne.hom v)

theorem Valuation.RankOne.nontrivial {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] : ∃ (r : R), v r ≠ 0 ∧ v r ≠ 1

theorem Valuation.RankOne.zero_of_hom_zero {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] {x : Γ₀} (hx : (Valuation.RankOne.hom v) x = 0) : x = 0

If v is a rank one valuation and x : Γ₀ has image 0 under RankOne.hom v, then x = 0.

theorem Valuation.RankOne.hom_eq_zero_iff {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] {x : Γ₀} : (Valuation.RankOne.hom v) x = 0 ↔ x = 0

If v is a rank one valuation, thenx : Γ₀ has image 0 under RankOne.hom v if and only if x = 0.

def Valuation.RankOne.unit {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] : Γ₀ˣ

A nontrivial unit of Γ₀, given that there exists a rank one v : Valuation R Γ₀.

Equations

• Valuation.RankOne.unit v = Units.mk0 (v ⋯.choose) ⋯

theorem Valuation.RankOne.unit_ne_one {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] : Valuation.RankOne.unit v ≠ 1

A proof that RankOne.unit v ≠ 1.