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.

References

• [N. Bourbaki, Topologie générale][bourbaki1966]

Tags

absolute value, uniform spaces

def AbsoluteValue.uniformSpace {𝕜 : Type u_1} [LinearOrderedField 𝕜] {R : Type u_2} [CommRing R] (abv : AbsoluteValue R 𝕜) : UniformSpace R

The uniform structure coming from an absolute value.

Equations

• AbsoluteValue.uniformSpace abv = UniformSpace.ofFun (fun (x y : R) => abv (y - x)) ⋯ ⋯ ⋯ ⋯

theorem AbsoluteValue.hasBasis_uniformity {𝕜 : Type u_1} [LinearOrderedField 𝕜] {R : Type u_2} [CommRing R] (abv : AbsoluteValue R 𝕜) : Filter.HasBasis (uniformity R) (fun (x : 𝕜) => 0 < x) fun (ε : 𝕜) => {p : R × R | abv (p.2 - p.1) < ε}