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

Tags

absolute value, uniform spaces

@[instance_reducible]

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

The uniform structure coming from an absolute value.

Equations

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

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