Rank one valuations

We define rank one valuations.

Main Definitions

• RankOne : A valuation has rank one if it is nontrivial and its image (defined as MonoidWithZeroHom.valueGroup₀ v) is contained in ℝ≥0. Note that this class includes the data of an inclusion morphism MonoidWithZeroHom.valueGroup₀ v → ℝ≥0.
• RankOne.restrict_RankOne is the RankOne instance for the restriction of a valuation to its image, as defined in

Tags

valuation, rank one

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

A valuation has rank at most one if its image (defined as MonoidWithZeroHom.valueGroup₀ v) is contained in ℝ≥0. Note that this class includes the data of an inclusion morphism MonoidWithZeroHom.valueGroup₀ v → ℝ≥0.

• hom' : MonoidWithZeroHom.ValueGroup₀ v →*₀ NNReal

  The inclusion morphism from Γ₀ to ℝ≥0.

• strictMono' : StrictMono ⇑(hom' v)

class Valuation.RankOne {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) extends v.RankLeOne, 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.

• hom' : MonoidWithZeroHom.ValueGroup₀ v →*₀ NNReal
• strictMono' : StrictMono ⇑(hom' v)
• exists_val_nontrivial : ∃ (x : R), v x ≠ 0 ∧ v x ≠ 1

theorem Valuation.nonempty_rankOne_iff_mulArchimedean {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} [v.IsNontrivial] : Nonempty v.RankOne ↔ MulArchimedean (MonoidWithZeroHom.ValueGroup₀ v)

@[reducible, inline]

abbrev Valuation.RankOne.hom {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankOne] : MonoidWithZeroHom.ValueGroup₀ v →*₀ NNReal

The inclusion morphism from Γ₀ to ℝ≥0.

Equations

• Valuation.RankOne.hom v = Valuation.RankLeOne.hom' v

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

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

theorem Valuation.RankOne.zero_of_hom_zero {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankOne] {x : MonoidWithZeroHom.ValueGroup₀ v} (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} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankOne] {x : MonoidWithZeroHom.ValueGroup₀ v} : (hom v) x = 0 ↔ x = 0

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

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

A proof that RankOne.unit v ≠ 1.

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

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

@[implicit_reducible]

noncomputable instance Valuation.RankOne.restrict_RankOne {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u_3) [Field K] (v : Valuation K Γ₀) [v.RankOne] : v.restrict.RankOne

Equations

• Valuation.RankOne.restrict_RankOne K v = { hom' := (Valuation.RankOne.hom v).comp MonoidWithZeroHom.ValueGroup₀.embedding, strictMono' := ⋯, toIsNontrivial := ⋯ }

@[simp]

theorem Valuation.RankOne.restrict_RankOne_hom_eq {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u_3) [Field K] (v : Valuation K Γ₀) [v.RankOne] : hom v.restrict = (hom v).comp MonoidWithZeroHom.ValueGroup₀.embedding

theorem Valuation.RankOne.exists_val_lt {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) [v.RankOne] {γ : NNReal} (hγ : γ ≠ 0) : ∃ (x : K), x ≠ 0 ∧ (hom v) (v.restrict x) < γ

@[implicit_reducible]

def Valuation.RankLeOne.rankOne_of_exists {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [DivisionRing K] (v : Valuation K Γ₀) [v.RankLeOne] (H : ∃ (x : K), x ≠ 0 ∧ v x ≠ 1) : v.RankOne

If a valuation has rank at most one and is non trivial, then it has rank one

Equations

• Valuation.RankLeOne.rankOne_of_exists v H = { toRankLeOne := inst✝, toIsNontrivial := ⋯ }

@[implicit_reducible]

def Valuation.RankLeOne.rankOne_of_nontrivial {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [DivisionRing K] (v : Valuation K Γ₀) [v.RankLeOne] (H : Nontrivial (MonoidWithZeroHom.ValueGroup₀ v)ˣ) : v.RankOne

If a valuation has rank at most one and is non trivial, then it has rank one

Equations

• Valuation.RankLeOne.rankOne_of_nontrivial v H = { toRankLeOne := inst✝, toIsNontrivial := ⋯ }

theorem Valuation.RankLeOne.exists_val_lt {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [Field K] (v : Valuation K Γ₀) [v.RankLeOne] : Subsingleton (MonoidWithZeroHom.ValueGroup₀ v)ˣ ∨ ∀ {γ : NNReal}, γ ≠ 0 → ∃ (x : K), x ≠ 0 ∧ (hom' v) (v.restrict x) < γ

@[implicit_reducible]

noncomputable 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 = { hom' := e.emb.comp MonoidWithZeroHom.ValueGroup₀.embedding, strictMono' := ⋯, toIsNontrivial := ⋯ }

@[implicit_reducible]

noncomputable 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

noncomputable 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)).comp (ValuativeRel.ValueGroupWithZero.embed (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

theorem ValuativeRel.isRankLeOne_iff_mulArchimedean {R : Type u_3} [CommRing R] [ValuativeRel R] : IsRankLeOne R ↔ MulArchimedean (ValueGroupWithZero R)

theorem ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [CommRing R] [ValuativeRel R] [MulArchimedean Γ₀] (v : Valuation R Γ₀) [v.Compatible] : IsRankLeOne R