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.

@[simp]

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

@[implicit_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

@[implicit_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.

@[implicit_reducible]

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

noncomputable def Valuation.norm {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀) [hv : v.RankOne] : L → ℝ

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

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

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

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

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

theorem Valuation.norm_pos_iff_valuation_pos {L : Type u_1} [Field L] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀) [hv : v.RankOne] {x : L} : 0 < v.norm x ↔ 0 < v x

@[implicit_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.

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.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

@[implicit_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.