Uniform structure induced by an absolute value
We build a uniform space structure on a commutative ring R equipped with an absolute value into
a linear ordered field 𝕜. Of course in the case R is ℚ, ℝ or ℂ and
𝕜 = ℝ, we get the same thing as the metric space construction, and the general construction
follows exactly the same path.
Implementation details
Note that we import data.real.cau_seq because this is where absolute values are defined, but
the current file does not depend on real numbers. TODO: extract absolute values from that
data.real folder.
References
- [N. Bourbaki, Topologie générale][bourbaki1966]
Tags
absolute value, uniform spaces
def
is_absolute_value.uniform_space_core
{𝕜 : Type u_1}
[discrete_linear_ordered_field 𝕜]
{R : Type u_2}
[comm_ring R]
(abv : R → 𝕜)
[is_absolute_value abv] :
The uniformity coming from an absolute value.
Equations
- is_absolute_value.uniform_space_core abv = {uniformity := ⨅ (ε : 𝕜) (H : ε > 0), filter.principal {p : R × R | abv (p.snd - p.fst) < ε}, refl := _, symm := _, comp := _}
def
is_absolute_value.uniform_space
{𝕜 : Type u_1}
[discrete_linear_ordered_field 𝕜]
{R : Type u_2}
[comm_ring R]
(abv : R → 𝕜)
[is_absolute_value abv] :
The uniform structure coming from an absolute value.
Equations
theorem
is_absolute_value.mem_uniformity
{𝕜 : Type u_1}
[discrete_linear_ordered_field 𝕜]
{R : Type u_2}
[comm_ring R]
(abv : R → 𝕜)
[is_absolute_value abv]
{s : set (R × R)} :
s ∈ (is_absolute_value.uniform_space_core abv).uniformity ↔ ∃ (ε : 𝕜) (H : ε > 0), ∀ {a b : R}, abv (b - a) < ε → (a, b) ∈ s