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