Conditions to have an ultrametric norm on a division ring

This file provides ways of constructing an instance of IsUltrametricDist based on facts about the existing norm.

Main results

• isUltrametricDist_of_forall_norm_natCast_le_one: a norm in a division ring is ultrametric if the norm of the image of a natural is less than or equal to one

• isUltrametricDist_iff_forall_norm_natCast_le_one: a norm in a division ring is ultrametric if and only if the norm of the image of a natural is less than or equal to one

Implementation details

The proof relies on a bounded-from-above argument. The main result has a longer proof to be able to be applied in noncommutative division rings.

Tags

ultrametric, nonarchimedean

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one {R : Type u_1} [NormedDivisionRing R] (h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1) : IsUltrametricDist R

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one {R : Type u_1} [NormedDivisionRing R] (h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1) : IsUltrametricDist R

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one {R : Type u_1} [NormedDivisionRing R] (h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1) : IsUltrametricDist R

theorem IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm {R : Type u_1} [NormedDivisionRing R] (h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)) : IsUltrametricDist R

This technical lemma is used in the proof of isUltrametricDist_of_forall_norm_natCast_le_one.

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one {R : Type u_1} [NormedDivisionRing R] (h : ∀ (n : ℕ), ‖↑n‖ ≤ 1) : IsUltrametricDist R

To prove that a normed division ring is nonarchimedean, it suffices to prove that the norm of the image of any natural is less than or equal to one.

theorem isUltrametricDist_iff_forall_norm_natCast_le_one {R : Type u_1} [NormedDivisionRing R] : IsUltrametricDist R ↔ ∀ (n : ℕ), ‖↑n‖ ≤ 1