Mathlib.Topology.UniformSpace.AbsoluteValue

Module docstring

{"# 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 "}

AbsoluteValue.uniformSpace definition

: UniformSpace R

Full source

/-- The uniform structure coming from an absolute value. -/
def uniformSpace : UniformSpace R :=
  .ofFun (fun x y => abv (y - x)) (by simp) (fun x y => abv.map_sub y x)
    (fun _ _ _ => (abv.sub_le _ _ _).trans_eq (add_comm _ _))
    fun ε ε0 => ⟨ε / 2, half_pos ε0, fun _ h₁ _ h₂ => (add_lt_add h₁ h₂).trans_eq (add_halves ε)⟩

Uniform structure induced by an absolute value

Informal description

The uniform space structure on a commutative ring $R$ induced by an absolute value $abv : R \to \mathbb{K}$, where $\mathbb{K}$ is a linearly ordered field. The uniformity is defined by the entourages $\{(x, y) \in R \times R \mid abv(y - x) < \varepsilon\}$ for all $\varepsilon > 0$ in $\mathbb{K}$. This construction generalizes the metric space uniformity when $R$ is $\mathbb{Q}$, $\mathbb{R}$, or $\mathbb{C}$ and $\mathbb{K} = \mathbb{R}$.

AbsoluteValue.hasBasis_uniformity theorem

: 𝓤[abv.uniformSpace].HasBasis ((0 : 𝕜) < ·) fun ε => {p : R × R | abv (p.2 - p.1) < ε}

Full source

theorem hasBasis_uniformity :
    𝓤[abv.uniformSpace].HasBasis ((0 : 𝕜) < ·) fun ε => { p : R × R | abv (p.2 - p.1) < ε } :=
  UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Basis for Uniformity Induced by Absolute Value

Informal description

The uniformity $\mathfrak{U}$ on a commutative ring $R$ induced by an absolute value $abv: R \to \mathbb{K}$ (where $\mathbb{K}$ is a linearly ordered field) has a basis consisting of sets of the form $\{(x, y) \in R \times R \mid abv(y - x) < \varepsilon\}$ for all $\varepsilon > 0$ in $\mathbb{K}$.