Formal balls are an extraordinarily useful notion in the study of quasi-metric, and even hemi-metric spaces: see Section 7.3 of the book, and [1]. Is there any way of extending the notion to the case of quasi-uniform spaces? This is what I would like to start investigating in this post. In particular, this post is pretty experimental, and I don’t make any guarantee that any of what I am going to say leads to anything of any interest whatsoever.

Let me remind you of what formal balls are and a bit of what you can do with them.

- Given a hemi-metric space
*X*,*d*, its space**B**(*X*,*d*) of formal balls is the set of pairs (formal balls) of the form (*x*,*r*) where*x*is a point in*X*and*r*is a non-negative real. - Formal balls are preordered (and, in fact, ordered if
*d*is a quasi-metric, not just a hemi-metric) by (*x,r*) ≤^{d+}(*y*,*s*) if and only if*d*(*x*,*y*) ≤*r*–*s*. - The Kostanek-Waszkiewicz theorem (Theorem 7.4.27 in the book) states that
**B**(*X*,*d*) is a dcpo if and only if*X*,*d*is Yoneda-complete. - The Romaguera-Valero theorem (Theorem 7.3.11) states that
*X*,*d*is Smyth-complete if and only if**B**(*X*,*d*) is a continuous dcpo with ≺^{d+}as way-below relation, where (*x*,*r*) ≺^{d+}(*y*,*s*) is defined by*d*(*x*,*y*) <*r*–*s*. - A deeper understanding of the latter is obtained by realizing that
**B**(*X*,*d*) itself has a hemi-metric*d*^{+}, defined by*d*^{+}((*x*,*r*), (*y*,*s*)) ≝ max(*d*(*x*,*y*)–*r*+*s*, 0), that**B**(*X*,*d*) is a c-space in the open ball topology of*d*^{+}, and that ≺^{d+}is the relation we would expect to be of some interest in a c-space, namely: (*x*,*r*) ≺^{d+}(*y*,*s*) if and only if (*y*,*s*) is in the interior of the upward closure of (*x*,*r*). Then*X*,*d*is Smyth-complete if and only if**B**(*X*,*d*) is sober in the open ball topology of*d*^{+}(Theorem 8.3.40). - One can build a completion
**S**(*X*,*d*),*d*^{+}as follows (section 7.5, see also [2]). Its elements are rounded ideals of formal balls, built from the abstract basis_{H}**B**(*X*,*d*), ≺^{d+}. This is an abstract basis because c-spaces and abstract bases are essentially the same thing (Exercise 8.3.46). And the quasi-metric*d*^{+}is the Hausdorff-Hoare quasi-metric, defined by_{H}*d*^{+}(_{H}*D*,*D’*) ≝ sup_{(x,r) ∈ D}inf_{(y,s) ∈ D‘}*d*^{+}((*x*,*r*), (*y*,*s*)). **S**(*X*,*d*),*d*^{+}is always Yoneda-complete, and in fact algebraic Yoneda-complete (Exercise 7.5.11)._{H}**S**(*X*,*d*),*d*^{+}is the free Yoneda-complete quasi-metric space above_{H}*X*,*d*, in a precise sense (Fact 7.5.23). This notably means that there is a 1-Lipschitz map η:^{S}*X*,*d*→**S**(*X*,*d*),*d*^{+}, called the_{H}*unit*(explicitly, η(^{S}*x*) is the set of all formal balls ≺^{d+}(*x*,0)), and that every 1-Lipschitz map*f*:*X*,*d*→*Y*,*d’*to a Yoneda-complete quasi-metric space*Y*,*d’*extends uniquely to a 1-Lipschitz*continuous*map*f*† :**S**(*X*,*d*),*d*^{+}→_{H}*Y*,*d’*; and by extending I mean that*f*† o η=^{S}*f*(Propositoin 7.5.22).**S**(*X*,*d*),*d*^{+}is isomorphic to_{H}*X*,*d*through the unit ηif and only if^{S}*X*,*d*is Smyth-complete, if and ony if ηis bijective (Proposition 7.5.15).^{S}**S**(*X*,*d*),*d*^{+}coincides with the usual Cauchy completion when_{H}*d*is a metric, up to natural isometry (Exercise 7.5.21).

I will suggest a notion of formal ball for quasi-uniform spaces. Not everything will run as smoothly as in the hemi-metric case, but let me say that this is promising so far.

In the sequel, we fix a quasi-uniform space *X*, with quasi-uniformity ** U**.

## A proposal for formal balls in the quasi-uniform setting

Given a hemi-metric space *X*, *d*, a formal ball is a pair (*x*,*r*) where *x* is a point of *X* and *r* is a non-negative real number. Up to some degree of approximation, we may encode *r* by the set [≤*r*] ≝ {(*x*,*y*) | *d*(*x*,*y*)≤*r*}. This is an entourage, provided that *r*>0.

Let me define quasi-uniform formal balls by analogy, as pairs (*x*, *R*) where *x* is a point of *X* and *R* is an entourage, in ** U**. Of course, the entourage

*R*plays the rôle of a radius here. Let

**B**

_{0}(

*X*,

**) denote the set of all quasi-uniform formal balls on**

*U**X*, with quasi-unifomity

**.**

*U*There is one thing we are missing with this proposal: there is no analogue of the formal balls (*x*,*r*) with *r*=0. Indeed, [≤0] is *not* generally an entourage. This is a problem inasmuch as this prevents us from embedding *X* into **B**_{0}(*X*,** U**), as we could do it in the hemi-metric case, through the map

*x*↦ (

*x*,0). We may fix this by taking the disjoint union of

**B**

_{0}(

*X*,

**) with**

*U**X*itself, for example, but I will not do this.

There is a further issue with taking entourages as an extended form of radii. The closest analogue of addition of radii is relation composition, since [≤*r*] o [≤*s*] ⊆ [≤*r*+*s*], but this is not a perfect analogy, since we only have an inclusion here, not an equality. Worse, that ‘addition’ obtained as relation composition is *not commutative*, and not invertible. This is a source of constant trouble… but we will learn to live with it.

All right, how do we order our new kind of formal balls? I must say I have had several ideas, but only one seems to give any kind of decent results.

## The preordering ≤^{U+} on formal balls

^{U+}We *pre*order formal balls by: (*x*,*R*) ≤**^{U+}** (

*y*,

*S*) if and only if

*R*⊇

*S*and

*R*[

*x*] ⊇

*S*[

*y*]. Beware that this is a preordering, not an ordering in general.

That looks like this comes from nowhere; but look carefully at the proof of the proposition, seen last time, that every Smyth-complete space *X* is quasi-sober in its induced topology: this is exactly the relation that we had used there.

Let us compare this relation ≤**^{U+}** on quasi-uniform formal balls with the usual ordering on formal balls we had in the quasi-metric case (Fact 7.3.2 in the book): in the quasi-metric setting, (

*x*,

*r*) is below (

*y*,

*s*) if and only if

*d*(

*x*,

*y*)≤

*r*–

*s*. That implies that the open ball of radius

*r*centered at

*x*contains the open ball of radius

*s*centers at

*y*, namely that

*R*[

*x*] ⊇

*S*[

*y*], where

*R*≝ [≤

*r*] and

*S*≝ [≤

*s*], but is not equivalent to it. That also implies

*r*≥

*s*, which implies

*R*⊇

*S*.

Hence ≤**^{U+}** is somewhat close to the usual ordering on quasi-metric formal balls. However, as I mentioned above, ≤

**is certainly not an ordering in general, which sets it apart from the usual ordering ≤**

^{U+}

^{d}**we have on formal balls. In fact, for every**

^{+}*R*∈

*U*_{0}, for any two points

*x*and

*y*such that

*R*[

*x*]=

*R*[

*y*], we will have both (

*x*,

*R*) ≤

**(**

^{U+}*y*,

*R*) and (

*y*,

*R*) ≤

**(**

^{U+}*x*,

*R*), even when

*x*≠

*y*. That happens even when the induced topology of

**is T**

*U*_{0}.

## The abstract basis of formal balls

The space of formal balls of a hemi-metric space is an abstract basis (Lemma 7.3.10 in the book), where (*x*,*r*) ≺ (*y*,*s*) if and only if *d*(*x*,*y*) < *r*–*s*. In the book, this is deduced from the fact that it is a c-space, one given the open ball topology of a new hemi-metric *d*^{+}. None of this seems to work quite as well with quasi-uniform spaces, but we can define a structure of an abstract basis on **B**_{0}(*X*,** U**) directly, by analogy, as follows.

In the hemi-metric case, notice that (*x*,*r*) ≺ (*y*,*s*) if and only if there is a *t*>0 such that (*x*,*r*) ≤^{d+}(*y*,*t*+*s*). By analogy, in the quasi-uniform case, we declare that (*x*,*R*) ≺^{U+} (*y*,*S*) if and only if there is an entourage *T* ∈ ** U** such that (

*x*,

*R*) ≤

^{U+}(

*y*,

*T*o

*S*). (Or equivalently,

*R*⊇

*T*o

*S*and

*R*[

*x*] ⊇

*T*[

*S*[

*y*]].)

Note that I am using *T* o *S* as an analogue of radius addition *t*+*s*. While it seems that I could have used *S* o *T* instead, that would definitely not work so well.

In the sequel, I will use the following often.

**Fact.** For every two entourages *R* and *S*, *R* o *S* is again an entourage.

Indeed, since *R* is reflexive, *R* o *S* contains *S*, and any binary relation that contains an entourage is an entourage.

**Lemma A.** The relation ≺^{U+} turns **B**_{0}(*X*,** U**) into an abstract basis.

First, a bit of notation, which we will reuse often. For every entourage *R*, there is an entourage *S* such that *S* o *S* ⊆ *R*. Let me call such an *S* a *splitter* of *R*. Please allow me to write ½*R* for such a splitter: in the quasi-metric case, if *R*=[≤*r*], then we can take ½*R*=*S* to be [≤½*r*]. There is nothing canonical in the choice of ½*R*=*S*, though. However, splitters always satisfy ½*R* o ½*R* ⊆ *R*.

*Proof.* We must check that ≺^{U+} is transitive and interpolative (see Lemma 5.1.32 in the book).

Transitivity is easier. Let us assume that (*x*_{1},*R*_{1}) ≺^{U+} (*x*_{2},*R*_{2}) ≺^{U+} (*x*_{3},*R*_{3}). There are two entourages *T*_{1} and *T*_{2} such that *R*_{1} ⊇ *T*_{1} o *R*_{2}, *R*_{1}[*x*_{1}] ⊇ *T*_{1}[*R*_{2}[*x*_{2}]], *R*_{2} ⊇ *T*_{2} o *R*_{3}, and *R*_{2}[*x*_{2}] ⊇ *T*_{2}[*R*_{3}[*x*_{3}]]. It follows that *R*_{1} ⊇ *T*_{1} o *T*_{2} o *R*_{3} and *R*_{1}[*x*_{1}] ⊇ *T*_{1}[*T*_{2}[*R*_{3}[*x*_{3}]]]. One can rewrite those as *R*_{1} ⊇ (*T*_{1} o *T*_{2}) o *R*_{3} and *R*_{1}[*x*_{1}] ⊇ (*T*_{1} o *T*_{2})[*R*_{3}[*x*_{3}]]. Since *T*_{1} o *T*_{2} is an entourage (by the Fact above), this establishes that (*x*_{1},*R*_{1}) ≺^{U+} (*x*_{3},*R*_{3}).

We turn to interpolation. We assume that we have *n*+1 formal balls (*x*_{1},*R*_{1}), …, (*x*_{n},*R*_{n}) and (*y*,*S*), and that (*x*_{i},*R*_{i}) ≺^{U+} (*y*,*S*) for every *i*, 1≤*i*≤*n*. Hence we have *n* entourages *T*_{1}, …, *T*_{n} such that *R*_{i} ⊇ *T*_{i} o * S* and

*R*_{i}[

*x*_{i}] ⊇

*T*_{i}[

*[*

*S**]] for every*

*y**i*, 1≤

*i*≤

*n*. We consider splitters ½

*T*

_{i}of each of the entourages

*T*

_{i}. Then

*T’*≝ ½

*T*

_{1}∩ … ∩ ½

*T*

_{n}is again an entourage. Let us define

*S’*as

*T’*o

*S*(an entourage!), and let us check that (

*y*,

*S’*) ≺

^{U+}(

*y*,

*S*) and that (

*x*

_{i},

*R*

_{i}) ≺

^{U+}(

*y*,

*S’*) for every

*i*, 1≤

*i*≤

*n*.

- (
*y*,*S’*) ≺^{U+}(*y*,*S*) is because*S’*⊇*T’*o*S*and*S’*[*y*] ⊇*T*‘[*S*[*y*]]; in fact those are equalities, not just inclusions. - (
*x*_{i},*R*_{i}) ≺^{U+}(*y*,*S’*) is because*R*_{i}⊇ ½*T*_{i}o‘ and*S**R*_{i}[*x*_{i}] ⊇ ½*T*_{i}[‘[*S*]]. We justify those inclusions as follows. For the first one, ½*y**T*_{i}o‘ is equal to ½*S**T*_{i}o*T’*o*S*, which is included in ½*T*_{i}o ½*T*_{i}o*S*, hence in*T*_{i}o*S*, and that is included in*R*_{i}. For the second one, every point*z*of ½*T*_{i}[‘[*S*]] is such that (*y**y*,*z*) is in ½*T*_{i}o‘, which is included in*S*o*T*_{i}, as we have just seen; so*S**z*is in*T*_{i}[[*S*]], and this is included in*y**R*_{i}[*x*_{i}]. ☐

## The rounded ideal completion of **B**_{0}(*X*,*U*)

*U*

Once we have an abstract basis *B*, ≺, taking its rounded ideal completion **RI**(*B*, ≺) gives you a continuous dcpo (Proposition 5.1.33) with a basis that is essentially *B* itself, modulo an encoding of element *b* of *B* as rounded ideals ⇓*b*, and with a way below relation defined by *x*≪*y* if and only if *x* ⊆ ⇓*b* for some *b* in *y*.

Hence we do have a continuous dcpo **RI**(**B**_{0}(*X*,** U**), ≺

^{U+}). Its elements are the rounded ideals

*D*of formal balls, namely the sets of formal balls such that:

*D*is downwards-closed: for every (*y*,*S*) in*D*, for every formal ball (*x*,*R*) ≺^{U+}(*y*,*S*), (*x*,*R*) is in*D*;*D*is directed: for every natural number*n*(including the cases*n*=0 and*n*=1), and for any collection of*n*formal balls (*x*_{1},*R*_{1}), …, (*x*_{n},*R*_{n}) in*S*, there is a further formal ball (*y*,*S*) in*D*such that (*x*_{i},*R*_{i}) ≺^{U+}(*y*,*S*) for every*i*, 1≤*i*≤*n*.

In the hemi-metric case, we had a similar construction **RI**(**B**(*X*,*d*), ≺), and there was a subset of it, consisting of those rounded ideals that had *aperture zero*. That subset was **S**(*X*,*d*), the formal ball completion of *X*,*d*. Let us imitate that. The *aperture* of a rounded ideal *D* is the infimum of the radii *r* of those formal balls (*x*,*r*) that occur in *D*.

One may be tempted to define the aperture of a quasi-uniform rounded ideal as being the intersection of all the entourages *R* that appear in radius position in those formal balls (*x*,*R*) that occur in *D*, but that would lead nowhere. That intersection may fail to be an entourage, but what is far worse is that this intersection does not have any remarkable property per se.

Instead, let me say that a rounded ideal *D* ∈ **RI**(**B**(*X*,*d*), ≺) has *aperture zero* if and only if for every entourage *R* ∈ ** U**, there is an element (

*y*,

*S*) in

*D*such that

*S*is included in

*R*.

Still by analogy, let **S**(*X*,** U**) be the subset of

**RI**(

**B**(

*X*,

*d*), ≺) of those rounded ideals with aperture zero.

## The formal ball completion

We can turn **S**(*X*,** U**) into a quasi-uniform space—one which we would like to call its formal ball completion—but this is starting to get difficult. We first observe that

*X*(quasi-)embeds into

**S**(

*X*,

**).**

*U***Lemma B.** For every *y* in *X*, the set η(*y*) ≝ {(*x*,*R*) ∈ **B**_{0}(*X*,** U**) | for some

*S*∈

**, (**

*U**x*,

*R*) ≤

^{U+}(

*y*,

*S*)} is an element of

**S**(

*X*,

**).**

*U*Proof. We must first check that η(*y*) is a rounded ideal.

- Downward closure. If (
*x*_{1},*R*_{1}) ≺^{U+}(*x*_{2},*R*_{2}) and (*x*_{2},*R*_{2}) is in η(*y*), then there is an entourage*T*such that*R*_{1}⊇o*T**R*_{2},*R*_{1}[*x*_{1}] ⊇[*T**R*_{2}[*x*_{2}]], and there is an entourage*S*such that*R*_{2}⊇*S*and*R*_{2}[*x*_{2}] ⊇*S*[*y*]. Then*R*_{1}⊇o*T**S*and*R*_{1}[*x*_{1}] ⊇[*T*[*S*]], so (*y**x*_{1},*R*_{1}) is in η(*y*). - Directedness. Let (
*x*_{1},*R*_{1}), …, (*x*_{n},*R*_{n}) be elements of η(*y*). Hence there are*n*entourages*S*_{1}, …,*S*_{n}such that*R*_{i}⊇*S*_{i}and*R*_{i}[*x*_{i}] ⊇*S*_{i}[] for every*y**i*, 1≤*i*≤*n*. We consider splitters ½*S*_{i}of each of the entourages*S*_{i}. Then*S’*≝ ½*S*_{1}∩ … ∩ ½*S*_{n}is again an entourage. We check that (*y*,*S’*) ∈ η(*y*) and that (*x*_{i},*R*_{i}) ≺^{U+}(*y*,*S’*) for every*i*, 1≤*i*≤*n*.- (
*y*,*S’*) ∈ η(*y*): this boils down to the existence of an entourage*S*such that (*y*,*S’*) ≤^{U+}(*y*,*S*); we simply take*S*≝*S’*. - (
*x*_{i},*R*_{i}) ≺^{U+}(*y*,*S’*): we check that*R*_{i}⊇*S’*o*S’*and that*R*_{i}[*x*_{i}] ⊇[*S*‘*S’*[]], using the fact that*y**S’*⊆ ½*S*_{i}and that ½*S*_{i}o ½*S*_{i}⊆*S*_{i}.

- (

Next, we must check that η(*y*) has aperture zero. For every entourage *R* in ** U**, (

*y*,

*R*) is in η(

*y*): indeed (

*y*,

*R*) ≤

^{U+}(

*y*,

*S*) where

*S*is simply equal to

*R*. ☐

This defines a map η : *X* → **S**(*X*,** U**). Note that η(

*y*) is also the set of formal balls (

*x*,

*R*) such that

*R*[

*x*] is a neighborhood of

*y*in the induced topology of

**. Indeed, if (**

*U**x*,

*R*) is in η(

*y*), then (

*x*,

*R*) ≤

^{U+}(

*y*,

*S*) for some entourage

*S*. In particular, the neighborhood

*S*[

*y*] of

*y*is included in

*R*[

*x*]. In the converse direction, if

*R*[

*x*] is a neighborhood of

*y*, then it contains a neighborhood

*T*[

*y*], for some entourage

*T*. In particular, it contains the smaller neighborhood

*S*[

*y*], where

*S*≝

*R*∩

*T*. Since

*R*contains

*S*, we obtain that (

*x*,

*R*) ≤

^{U+}(

*y*,

*S*), so that (

*x*,

*R*) is in η(

*y*).

**Lemma C.** η is monotone and order-reflecting, that is, for all *x*,*y* in *X*, *x*≤*y* in the specialization preordering of *X* if and only if η(*x*) ⊆ η(*y*).

Proof. If *x*≤*y*, then let us consider any element (*z*,*T*) of η(*x*). Hence *T*[*z*] is a neighborhood of *x*, and therefore also of *y*, since all open subsets are upwards closed in the specialization preordering. It follows that (*z*,*T*) is in η(*y*).

Conversely, let us assume that η(*x*) ⊆ η(*y*). At the end of the proof of Lemma B, we have seen that for every entourage *R*, (*x*,*R*) is in η(*x*). Hence (*x*,*R*) is also in η(*y*), meaning that *R*[*x*] is a neighborhood of *y*—in particular, it contains *y*. Since *R* is arbitrary, every open neighborhood of *x* contains *y*, and therefore *x*≤*y*. ☐

In particular, if *X* is T_{0} in the topology induced by ** U**, then η is injective, which is good news.

What should we take as a quasi-uniformity on **S**(*X*,** U**)? We do not have much choice, really: we should take the

*largest*quasi-uniformity that makes η uniformly continuous. That always exists because of the following, pretty high-level statement.

**Proposition.** The collection of all quasi-uniformities on a set *Z* is a complete lattice. Given any class of maps *f _{i}* :

*Y*→

_{i}*Z*,

*i*∈

*I*, where each

*Y*is a quasi-uniform space, there is a largest quasi-uniformity on

_{i}*Z*that makes all the maps

*f*uniformly continuous.

_{i}*Proof.* For the first part, let *U** _{j}*,

*j*∈

*J*, be a family of quasi-uniformities on

*Z*. In particular, they are elements of

**F**(

**Refl**(

*Z*)), the poset of filters of binary reflexive relations on

*Z*. For every distributive bounded lattice

*L*, its poset

**F**(

*L*) of filters is a complete lattice, in which the supremum of a family

*F*of filters is the collection of infima of finitely many elements from ∪

*F*. In the case at hand, that means that we can build the supremum

**of the filters**

*U*

*U**,*

_{j}*j*∈

*J*, inside

**(**

**F****(**

**Refl***Z*)), as the finite intersections of binary relations

*R*

_{1}∩ … ∩

*R*

_{n}(

*n*≥0; if

*n*=0, this is the relation relating every pair of elements, and that is indeed a reflexive relation). It now suffices to observe that this filter

**is a quasi-uniformity: then**

*U***will be the desired supremum of the family (**

*U*

*U**)*

_{j}_{j ∈ J}in the poset of quasi-uniformities on

*Z*. In order to show this, let

*R*≝

*R*

_{1}∩ … ∩

*R*

_{n}be any element of

**.**

*U**R*

_{1}is an element of some

*U**, and therefore has a splitter ½*

_{j}*R*

_{1}in

*U**. We do the same with*

_{j}*R*

_{2}, …,

*R*

_{n}, and we let

*R’*be (½

*R*

_{1}) ∩ … ∩ (½

*R*

_{n}). Since ½

*R*

_{1}, …, ½

*R*

_{n}are all in some

*U**(not necessarily the same one),*

_{j}*R’*is in

**. Moreover, it is clear that**

*U**R’*o

*R’*is included in

*R*. Hence

**is a quasi-uniformity, as promised.**

*U*This shows that the poset of all quasi-uniformities has all suprema. It follows that it also has all infima: in order to compute the infimum of a family *F*, compute the supremum of its family of lower bounds.

We turn to the second part. Note, by the way, that we take a *class* of maps, not necessarily a set of maps here. Let *F* be the collection of quasi-uniformities on *Z* that make all the maps *f _{i}* uniformly continuous. (This is a set, even when those maps form a proper class.) Let

**be the supremum of**

*U**F*in the complete lattice of quasi-uniformities on

*Z*. We claim that

**is again in**

*U**F*, so that

**will indeed be the**

*U**largest*quasi-uniformity that makes all the maps

*f*uniformly continuous. To this end, let

_{i}*R*≝

*R*

_{1}∩ … ∩

*R*

_{n}be any element of

**, where each**

*U**R*is in some quasi-uniformity that occurs as an element of

_{j}*F*. Let us also fix an arbitrary

*i*∈

*I*. We must show that (

*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*) is an entourage of

*Y*. We realize that (

_{i}*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*) is equal to (

*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*_{1}) ∩ … ∩ (

*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*

_{n}). Now

*R*_{1}is in some quasi-uniformity

*U**that occurs as an element of*

_{j}*F*. By definition of

*F*,

*is uniformly continuous from*

*f*_{i}*Y*to

_{i}*Z*with the quasi-uniformity

*U**: so (*

_{j}*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*_{1}) is an entourage of

*Y*. We do the same with

_{i}*R*

_{2}, …,

*R*

_{n}. Therefore (

*×*

*f*_{i}*)*

*f*_{i}^{–1}(

*R*) is a finite intersection of entourages of

*Y*, and is therefore itself an entourage of

_{i}*Y*. It follows that

_{i}*f*is uniformly continuous from

_{i}*Y*to

_{i}*Z*with the quasi-uniformity

**. ☐**

*U*The latter proposition has an interesting categorical reading. It shows that the forgetful functor from the category **QUnif** of quasi-uniform spaces and uniformly continuous maps to **Set** is *topological*. (Well, it almost does. Let me spare the details.) I can only recommend reading Chapter VI of [3] for an introduction to this pretty amazing piece of category theory. It immediately follows that **QUnif** is complete, cocomplete, has regular factorizations, separators and coseparators, and (since it is also fiber-small) is also wellpowered and co-wellpowered, among other miracles (whatever all that may mean, if you do not know already).

But let us return to our topic. We equip **S**(*X*,** U**) with the largest quasi-uniformity

*U*^{+}that makes η :

*X*→

**S**(

*X*,

**) uniformly continuous. I have no concrete description of that quasi-uniformity, though. But we now have a quasi-uniform space**

*U***S**(

*X*,

**), and a uniformly continuous map η :**

*U**X*→

**S**(

*X*,

**), which is injective if**

*U**X*is T

_{0}.

## Conclusion

Let me stop there. This post is already long enough. However, let me ask a few questions, which I may or may not answer in the future.

- Is there any concrete description of the quasi-uniformity
*U*^{+}on**S**(*X*,)?*U* - Is
**S**(*X*,) is isomorphic to the*U**Smyth-completion*of*X*[4, Section V]? - By analogy with hemi-metric spaces, on may define a quasi-uniform space as complete (or ‘Yoneda-complete’) if and only if η is surjective. (I may explain why in a later post.) Is there a more concrete way of defining that form of completeness?
- With that notion of completeness, is
**S**(*X*,) complete? Remember that the formal ball completion of a hemi-metric case is not just (Yoneda-)complete, but even algebraic complete.*U* - Is it true that η is an isomorphism of quasi-uniform spaces if and only if
*X*is Smyth-complete? That would extend similar results on hemi-metric spaces. That would also follow from a positive solution to problem 2 in this list.

- Jean Goubault-Larrecq and Kok Min Ng. A few notes on formal balls. Logical Methods in Computer Science 13(4), nov. 28, 2017.
- Steven Vickers. Localic Completion of Generalized Metric Spaces I. Theory and Application of Categories 14(15), pages 328-356, 2005.
- Jiří Adámek, Horst Herrlich, and George E. Strecker.
*Abstract and concrete categories. The joy of cats.*John Wiley and Sons, Inc., 1990. Online version available here. - Michael B. Smyth. Quasi-uniformities: Reconciling domains with metric spaces. In: Main M., Melton A., Mislove M., Schmidt D. (eds) Mathematical Foundations of Programming Language Semantics. MFPS 1987. Lecture Notes in Computer Science, vol 298. Springer, Berlin, Heidelberg. doi.org/10.1007/3-540-19020-1_12

— Jean Goubault-Larrecq (January 23rd, 2021)