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.

Tags

norm, nonarchimedean, nontrivial, valuation, rank one

def NormedField.valuation {K : Type u_1} [hK : NormedField K] (h : IsNonarchimedean norm) : Valuation K NNReal

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

Equations

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

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

def NormedField.toValued {K : Type u_1} [hK : NormedField K] (h : IsNonarchimedean norm) : Valued K NNReal

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

Equations

• NormedField.toValued h = let __src := PseudoMetricSpace.toUniformSpace; let __src_1 := NonUnitalNormedRing.toNormedAddCommGroup; Valued.mk (NormedField.valuation h) ⋯

def Valued.norm {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] : L → ℝ

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

Equations

• Valued.norm x = ↑((Valuation.RankOne.hom Valued.v) (Valued.v x))

theorem Valued.norm_nonneg {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] (x : L) : 0 ≤ Valued.norm x

theorem Valued.norm_add_le {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] (x : L) (y : L) : Valued.norm (x + y) ≤ max (Valued.norm x) (Valued.norm y)

theorem Valued.norm_eq_zero {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] {x : L} (hx : Valued.norm x = 0) : x = 0

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

The normed field structure determined by a rank one valuation.

Equations

• Valued.toNormedField L Γ₀ = let __src := inferInstance; NormedField.mk ⋯ ⋯