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 Γ₀) extends v.IsNontrivial : 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.

• exists_val_nontrivial : ∃ (x : R), v x ≠ 0 ∧ v x ≠ 1
• hom : Γ₀ →*₀ NNReal

  The inclusion morphism from Γ₀ to ℝ≥0.

• strictMono' : StrictMono ⇑(hom v)

theorem Valuation.RankOne.strictMono {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.RankOne] : StrictMono ⇑(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 : (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 : Γ₀} : (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] : unit v ≠ 1

A proof that RankOne.unit v ≠ 1.

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

def Valuation.RankOne.ofRankLeOneStruct {R : Type u_3} [CommRing R] [ValuativeRel R] [ValuativeRel.IsNontrivial R] (e : ValuativeRel.RankLeOneStruct R) : (ValuativeRel.valuation R).RankOne

A valuative relation has a rank one valuation when it is both nontrivial and the rank is at most one.

Equations

• Valuation.RankOne.ofRankLeOneStruct e = { toIsNontrivial := ⋯, hom := e.emb, strictMono' := ⋯ }

instance instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne {R : Type u_3} [CommRing R] [ValuativeRel R] [ValuativeRel.IsNontrivial R] [ValuativeRel.IsRankLeOne R] : (ValuativeRel.valuation R).RankOne

Equations

• instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne = Valuation.RankOne.ofRankLeOneStruct ⋯.some

def Valuation.RankOne.rankLeOneStruct {R : Type u_3} [CommRing R] [ValuativeRel R] (e : (ValuativeRel.valuation R).RankOne) : ValuativeRel.RankLeOneStruct R

Convert between the rank one statement on valuative relation's induced valuation.

Equations

• e.rankLeOneStruct = { emb := Valuation.RankOne.hom (ValuativeRel.valuation R), strictMono := ⋯ }

theorem ValuativeRel.isRankLeOne_of_rankOne {R : Type u_3} [CommRing R] [ValuativeRel R] [h : (valuation R).RankOne] : IsRankLeOne R

theorem ValuativeRel.isNontrivial_of_rankOne {R : Type u_3} [CommRing R] [ValuativeRel R] [h : (valuation R).RankOne] : IsNontrivial R