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] [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) : NormedField.valuation x = ‖x‖₊

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 = Valued.mk NormedField.valuation ⋯

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

Equations

• NormedField.instRankOneNNRealValuation = { hom := MonoidWithZeroHom.id NNReal, strictMono' := NormedField.instRankOneNNRealValuation.proof_1, nontrivial' := ⋯ }

def Valued.norm {L : Type u_1} [Field L] {Γ₀ : Type u_2} [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_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] (x : L) : 0 ≤ Valued.norm x

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

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

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

The normed field structure determined by a rank one valuation.

Equations

• Valued.toNormedField L Γ₀ = NormedField.mk ⋯ ⋯

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

instance Valued.instIsUltrametricDist (L : Type u_1) [Field L] (Γ₀ : Type u_2) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.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 : Valued.v.RankOne] : ⇑NormedField.valuation = ⇑(Valuation.RankOne.hom Valued.v) ∘ ⇑Valued.v

@[simp]

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

@[simp]

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

@[simp]

theorem Valued.toNormedField.norm_le_one_iff {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] {x : L} : ‖x‖ ≤ 1 ↔ Valued.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 : Valued.v.RankOne] {x : L} : ‖x‖ < 1 ↔ Valued.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 : Valued.v.RankOne] {x : L} : 1 ≤ ‖x‖ ↔ 1 ≤ Valued.v x

@[simp]

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

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

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

Equations

• Valued.toNontriviallyNormedField = NontriviallyNormedField.mk ⋯