Correspondence between nontrivial nonarchimedean norms and rank one valuations

Nontrivial nonarchimedean norms correspond to rank one valuations.

Main Definitions

• NormedField.toValued : the valued field structure on a nonarchimedean normed field K, determined by the norm.
• Valued.toNormedField : the normed field structure determined by a rank one valuation.

Main Results

• The valuation of a normed field has rank at most one.

Tags

norm, nonarchimedean, nontrivial, valuation, rank one

def NormedField.valuation {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] : Valuation K NNReal

The valuation on a nonarchimedean normed field K defined as nnNorm.

Equations

• NormedField.valuation = { toFun := nnNorm, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem NormedField.valuation_apply {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] (x : K) : valuation x = ‖x‖₊

@[instance_reducible]

noncomputable instance NormedField.instRankLeOneNNRealValuation {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] : valuation.RankLeOne

The valuation of a normed field has rank at most one

Equations

• NormedField.instRankLeOneNNRealValuation = { hom' := MonoidWithZeroHom.ValueGroup₀.embedding, strictMono' := ⋯ }

@[instance_reducible]

def NormedField.toValued {K : Type u_1} [hK : NormedField K] [IsUltrametricDist K] : Valued K NNReal

The valued field structure on a nonarchimedean normed field K, determined by the norm.

Equations

• NormedField.toValued = { toUniformSpace := PseudoMetricSpace.toUniformSpace, toIsUniformAddGroup := ⋯, v := NormedField.valuation, is_topological_valuation := ⋯ }

@[instance_reducible]

noncomputable instance NormedField.instRankOneNNRealValuation {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] : valuation.RankOne

Equations

• NormedField.instRankOneNNRealValuation = { hom' := MonoidWithZeroHom.ValueGroup₀.embedding, strictMono' := ⋯, toIsNontrivial := ⋯ }

noncomputable def Valuation.norm {R : Type u_1} [Ring R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankLeOne] : R → ℝ

The norm function determined by a rank one valuation on a field L.

Equations

• v.norm x = ↑((Valuation.RankLeOne.hom' v) (v.restrict x))

theorem Valuation.norm_def {R : Type u_1} [Ring R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankLeOne] {x : R} : v.norm x = ↑((RankLeOne.hom' v) (v.restrict x))

theorem Valuation.norm_nonneg {R : Type u_1} [Ring R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankLeOne] (x : R) : 0 ≤ v.norm x

theorem Valuation.norm_add_le {R : Type u_1} [Ring R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankLeOne] (x y : R) : v.norm (x + y) ≤ max (v.norm x) (v.norm y)

theorem Valuation.norm_eq_zero {L : Type u_2} [DivisionRing L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀) [v.RankLeOne] {x : L} (hx : v.norm x = 0) : x = 0

theorem Valuation.norm_pos_iff_valuation_pos {R : Type u_1} [Ring R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [hv : v.RankLeOne] {x : R} : 0 < v.norm x ↔ 0 < v x

noncomputable def Valuation.absoluteValue {L : Type u_2} [DivisionRing L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀) [hv : v.RankLeOne] : AbsoluteValue L ℝ

Absolute value corresponding to a valuation of rank at most one.

Equations

• v.absoluteValue = { toFun := v.norm, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

@[simp]

theorem Valuation.absoluteValue_apply {L : Type u_2} [DivisionRing L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀) [hv : v.RankLeOne] (a✝ : L) : v.absoluteValue a✝ = v.norm a✝

@[instance_reducible]

noncomputable def Valued.toNormedField (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : NormedField L

The normed field structure determined by a rank one valuation.

Equations

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

theorem Valued.isNonarchimedean_norm (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : IsNonarchimedean fun (x : L) => ‖x‖

instance Valued.instIsUltrametricDist (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : IsUltrametricDist L

theorem Valued.coe_valuation_eq_rankOne_hom_comp_valuation (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : ⇑NormedField.valuation = ⇑(Valuation.RankOne.hom v) ∘ ⇑v.restrict

theorem Valued.toNormedField.norm_def {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : ‖x‖ = ↑((Valuation.RankOne.hom v) (v.restrict x))

@[simp]

theorem Valued.toNormedField.norm_le_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x x' : L} : ‖x‖ ≤ ‖x'‖ ↔ v x ≤ v x'

@[simp]

theorem Valued.toNormedField.norm_lt_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x x' : L} : ‖x‖ < ‖x'‖ ↔ v x < v x'

@[simp]

theorem Valued.toNormedField.norm_le_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : ‖x‖ ≤ 1 ↔ v x ≤ 1

@[simp]

theorem Valued.toNormedField.norm_lt_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : ‖x‖ < 1 ↔ v x < 1

@[simp]

theorem Valued.toNormedField.one_le_norm_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : 1 ≤ ‖x‖ ↔ 1 ≤ v x

@[simp]

theorem Valued.toNormedField.one_lt_norm_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : 1 < ‖x‖ ↔ 1 < v x

theorem Valued.toNormedField.norm_eq_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] {x : L} : ‖x‖ = 1 ↔ v x = 1

theorem Valued.toNormedField.setOfPred_mem_integer_eq_closedBall {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : {x : L | x ∈ v.integer} = Metric.closedBall 0 1

@[deprecated Valued.toNormedField.setOfPred_mem_integer_eq_closedBall (since := "2026-07-09")]

theorem Valued.toNormedField.setOf_mem_integer_eq_closedBall {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : {x : L | x ∈ v.integer} = Metric.closedBall 0 1

Alias of Valued.toNormedField.setOfPred_mem_integer_eq_closedBall.

@[instance_reducible]

noncomputable def Valued.toNontriviallyNormedField (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : v.RankOne] : NontriviallyNormedField L

The nontrivially normed field structure determined by a rank one valuation.

Equations

• Valued.toNontriviallyNormedField L Γ₀ = { toNormedField := Valued.toNormedField L Γ₀, non_trivial := ⋯ }