What is a uniform space? How some computer scientists think about completions.

This is post 2 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in an undergraduate mathematics course. These definitions play a role in Lean because it’s important to set things up in the maximal generality for which they make sense, to avoid having to duplicate work. This post is about uniform spaces, and it mentions filters, which is the subject of the first post, so you might want to read that one first.

As a first year undergraduate I learnt that the reals were complete: every Cauchy sequence converges. As a second year undergraduate I learnt what it meant more generally for a metric space to be complete: every Cauchy sequence converges. However, my second year lecturer stressed that completeness was not a topological property. The example they gave was that the real numbers were homeomorphic to the open interval $(-1,1)$ (the function $\tanh$ being an example of a homeomorphism), and the reals were complete, yet $(-1,1)$ was not. At the time, I thought this was the end of the story.

Around a decade later I became interested in non-archimedean analysis, and here I saw some constructions which confused me. In fact in some sense I can trace my confusion back to the construction of the $p$ -adic integers. One can complete the integers using the $p$ -adic metric to get $\mathbb{Z}_p$ , the $p$ -adic integers, and a very slick way to do this is to define $\mathbb{Z}_p=\lim_n\mathbb{Z}/p^n\mathbb{Z}$ , the projective limit. Whilst this can be dressed up as the completion of a metric space with respect to the $p$ -adic metric, it looks like something more fundamental than that is going on. Later on I learnt about the profinite completion of a discrete group $G$ as $\projlim_U G/U$ as $U$ runs over the finite index subgroups. Where is the metric now? In what sense is the resulting space complete if it’s not even a metric space? Do I have to put some sort of artificial metric on $G$ somehow?

Skip forward another decade and I became interested in Huber’s adic spaces as a foundation for non-archimedean geometry. I learnt a vast amount from Torsten Wedhorn’s unpublished notes, which are the notes that we are using in our perfectoid spaces project. These notes contain really clear and precise definitions of pretty much everything they use. By definition 5.31 it was clear to me that I was missing something. Wedhorn defines what it means for an abelian topological group to be complete with no mention of a metric at all! But my 2nd year topology lecturer told me that completeness was not a topological property! What is going on?

Uniform spaces — an overview

It turns out that there’s a definition which had completely passed me by — that of a uniform space. The ever-reliable Wikipedia has an article on them of course. Before I say what they are, let me tell you some facts about them.

1) Every metric space is a uniform space; every uniform space is a topological space. Uniform spaces sit in between these two standard notions.

2) It makes sense to ask if a uniform space is complete, and indeed every uniform space has a Hausdorff completion, which is unique up to unique isomorphism and satisfies a universal property. This generalises the notion of a complete metric space.

3) Every topological group can be given the structure of a uniform space, and every compact Hausdorff topological space can be given the structure of a uniform space.

These three facts together explain everything that I was confused about above. The definition of a uniform space was due to Weil in 1937! Why don’t they teach it to undergraduates? It looks at the very least like a super sequence of example sheet questions, or a little first year mini-project or something. There’s more! You can talk about uniformly continuous maps between uniform spaces, and uniformly convergent sequences of such maps. In fact this gives us a clue as to exactly what we lose when going from a metric space to a topological space, and what we need to get back.

What does it mean for a map $f : X \to Y$ between metric spaces to be uniformly continuous? Let’s start by recalling the definition of continuity for a map between metric spaces. Continuity at $x\in X$ means that for all $\epsilon>0$ there’s a $\delta>0$ such that $d(x',x)<\delta$ implies $d(f(x'),f(x))<\epsilon$ . When teaching this we usually stress that $\delta$ depends on $\epsilon$ , but what we need to note here is that $\delta$ also in general depends on $x$ . The function $f$ is uniformly continuous if our rule for getting $\delta$ s from $\epsilon$ s can be made to be independent of $x$ , that is, if for all $\epsilon>0$ there exists $\delta>0$ such that for any $x,x'\in X$ we have $d(x',x)<\delta$ implies $d(f(x'),f(x))<\epsilon$ .

It’s clear why this notion doesn’t generalise to topological spaces. If $x_1\in X$ is arbitrary then we can consider all the open sets in the topology which contain $x_1$ ; but if $x_2$ is a second point then there’s in general no way of comparing the open neighbourhoods of $x_1$ with those of $x_2$ ; there is no way of formalising the notion that “ $x'_1$ is nearer to $x_1$ than $x'_2$ is to $x_2$ “, so we can’t write down a definition of uniform continuity for maps between topological spaces; the neighbourhoods of $x_1$ and $x_2$ are in general incomparable. A uniform structure is a way of putting this information back without going as far as adding a metric.

Uniform spaces — the definition.

The definition of a uniform space in Lean is rather intimidating for beginners; it’s in mathlib at topology/uniform/basic.lean. Let’s not worry about it just yet, let’s instead look at the definition on Wikipedia, which says that a uniformity (a.k.a. a uniform structure) on a set $X$ is a filter on $X\times X$ such that every set in the filter contains the diagonal $\{(x,x)\,|\,x\in X\}$ (that’s the first three axioms) and then some more axioms; but I think it’s worth explaining what this notion is trying to model before talking about the last two axioms. If $X$ is a metric space, the idea is that the uniformity is defined by: a subset $U\subseteq X\times X$ is in the uniformity iff there exists $\delta>0$ such that $d(x_1,x_2)<\delta$ implies $(x_1,x_2)\in U$ . The fact that every set in the uniformity contains all $(x,x)$ is the uniformity’s version of $d(x,x)=0$ ; the 5th axiom on Wikipedia, that the “transpose” of an element of the uniformity is in the uniformity, is some version of the symmetry axiom for a metric, and the fourth axiom, saying that for all $U$ in the uniformity there’s some $V$ in the uniformity with $V \circ V\subseteq U$ , is some analogue of the statement that if $d(x_1,x)<\delta/2$ and $d(x,x_2)<\delta/2$ then $d(x_1,x_2)<\delta$ .

The philosophy is that an element $U$ in the uniformity is a replacement for a positive real $\delta$ ; two points $x,y\in X$ are said to be “ $U$ -close” if $(x,y)\in U$ , the thought being that $U$ is our replacement for $\{(x,y)\in X\times X\,|\,d(x,y)<\delta\}$ .

Given a uniformity on a set $X$ , $X$ inherits a topology: a subset $V$ of $X$ is open iff for all $x\in V$ there’s some $U$ in the uniformity such that $(x,y)\in U\implies y\in V$ . The idea of course is that for fixed $x\in X$ , the things in $X$ which are $U$ -close to $x$ are a neighbourhood of $x$ .

Conversely given an abelian topological group (with group law $+$ ), there’s an associated uniformity: for any neighbourhood $V$ of zero, consider the set $U=\{(x,y)\,|\,x-y\in V\}$ ; these sets generate a filter which is a uniformity. What’s going on here is that we model the distance from $x$ to $y$ as the distance from $x-y$ to zero. If the group is not abelian then there are two uniformities, the left uniformity and the right uniformity, which may in general be different, but both of which generate the group’s topology.

Definition of a uniform space in Lean

let’s try and take it apart.


/-- This core description of a uniform space is outside of the type class hierarchy. It is useful
  for constructions of uniform spaces, when the topology is derived from the uniform space. -/
structure uniform_space.core (α : Type u) :=
(uniformity : filter (α × α))
(refl       : principal id_rel ≤ uniformity)
(symm       : tendsto prod.swap uniformity uniformity)
(comp       : uniformity.lift' (λs, comp_rel s s) ≤ uniformity)

-- [snip]

/-- A uniform space is a generalization of the "uniform" topological aspects of a
  metric space. It consists of a filter on `α × α` called the "uniformity", which
  satisfies properties analogous to the reflexivity, symmetry, and triangle properties
  of a metric.

  A metric space has a natural uniformity, and a uniform space has a natural topology.
  A topological group also has a natural uniformity, even when it is not metrizable. -/
class uniform_space (α : Type u) extends topological_space α, uniform_space.core α :=
(is_open_uniformity : ∀s, is_open s ↔ (∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ uniformity.sets))

We see that uniform_space extends topological_space (which is what we think it is) and also uniform_space.core, which is the uniformity. The statement that if $U$ is in the uniformity then the set $\{(y,x)\,|\,(x,y)\in U\}$ is too, Wikipedia’s axiom 5, is very coolly represented by the assertion that the swap function makes the uniformity filter tend to itself, or however one is supposed to talk about the tendsto predicate. The comp_rel function in Lean composes two relations, and the comp axiom is Wikipedia’s axiom 4. Of course one should not worry too much about how uniform spaces are implemented in Lean: the idea is that any standard definition or theorem about uniform spaces should be accessible via the interface (that is, the definitions and theorems that compose the majority of the uniform_space.lean file) and one should not have to worry about proving them.

Uniform continuity, and completeness

Say $f:X\to Y$ is a map between uniform spaces. Recall the definition of uniform continuity on metric spaces said that for all $\epsilon>0$ there exists $\delta>0$ such that $\delta$ -closeness on $X$ implies $\epsilon$ -closeness on $Y$ . For uniform spaces we ask that for all $U$ on $Y$ ‘s uniformity there exists $V$ on $X$ ‘s uniformity such that the pre-image of $U$ contains $V$ . In other words, we demand that the pre-image of the uniformity on $Y$ contains the uniformity on $X$ . This is nothing more than saying that the induced map $f \times f : X\times X\to Y\times Y$ satisfies tendsto (f x f) uniformity_X uniformity_Y, which is exactly the definition of uniform_continuous.

The last definition I want to mention is completeness. A uniform space is complete if every Cauchy filter converges! Let’s face it, that definition does look familiar, apart from the filter bit. So what does this mean? A filter on a uniform space $X$ is Cauchy if it contains “arbitrarily small sets”; that is, for every $U$ in the uniformity (remember $U$ is our replacement for $\epsilon>0$ ) there exists $V$ in the filter with $V\times V\subseteq U.$ A filter converges to $x\in X$ if for every neighbourhood $W$ of $x$ there’s an element $V$ of the filter with $V\subseteq W$ . The idea is that if $(x_n)$ is a sequence in $X$ then there’s a corresponding filter generated by the sets $\{x_n\,|\,n\geq N\}$ for $N=1,2,\ldots$ . Note that, as expected, the notion of convergence just depends on the topology, but the notion of Cauchy depends on the uniformity.

I guess one could now talk about the completion of a uniform topological space, but perhaps I’ve said enough; I am not sure I want to give a comprehensive account of these things, I just want mathematicians to be less scared of them. The definition of the completion of a uniform space is covered in the Wikipedia article. But the philosophy, for someone who wants to write Lean code, should be that any standard construction or definition or result about uniform spaces (for example any standard construction or definition or result about metric spaces) should already be in mathlib, and as an end user your job is not to prove it, but simply to find it.

2 Responses to What is a uniform space? How some computer scientists think about completions.

. says:

August 23, 2018 at 3:35 am

Cauchy sequences are elements of a Hom in a certain category, the simplicial category of filters, and convergence of a filter on a topological space can also be understood in terms of the same category.I do not know if this observation can be of help in formalisation or expressed nicely in Lean; perhaps it may lead to some syntax sugar….

Here are some details. Given a uniform space $X$ and a set $S$, define on $X^S$ the filter of “$\epsilon$-neighbourhoods of the diagonal”, namely a subset $A$ of $X^S$ is big iff there is a uniformity $U$ such that $(f(s’),f(s”))\in A$ for any $s’,s”\in S$. This defines a contravariant functor from the category of sets into the category of filters, call it $m(X)$.

A filter $F$ on $X$ is Cauchy iff the natural map $Hom(-,F)\rightarrow m(X)$ is well-defined.

A Cauchy sequence is a map $Hom(-,F)\rightarrow m(X)$ where $F$ is the cofinite filter on $\Bbb N$.

One can restrict these functors to the subcategory $\Delta^{op}$ of finite linear orders and consider instead simplicial filters; these characterisations continue to hold.

LikeLike

- . says:
  
  August 23, 2018 at 3:43 am
  
  correction: a subset $A$ of $X^S$ is big iff there is a uniformity $U$ such that $f\in A$ whenever $(f(s’),f(s”))\in U$ for each $s’,s”\in S$.
  
  LikeLike