Quasi-uniform spaces IV: Formal balls—a proposal

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+H as follows (section 7.5, see also [2]). Its elements are rounded ideals of formal balls, built from the abstract basis 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+H is the Hausdorff-Hoare quasi-metric, defined by d+H(D, D’) ≝ sup(x,r) ∈ D inf(y,s) ∈ D‘ d+((x,r), (y,s)).
  • S(X,d), d+H is always Yoneda-complete, and in fact algebraic Yoneda-complete (Exercise 7.5.11).
  • S(X,d), d+H is the free Yoneda-complete quasi-metric space above 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+H, called the 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+H is isomorphic to X,d through the unit ηS if and only if X,d is Smyth-complete, if and ony if ηS is bijective (Proposition 7.5.15).
  • S(X,d), d+H coincides with the usual Cauchy completion when 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 B0(X,U) denote the set of all quasi-uniform formal balls on 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 B0(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 B0(X,U) with 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

We preorder 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, ≤U+ is certainly not an ordering in general, which sets it apart from the usual ordering ≤d+ we have on formal balls. In fact, for every R ∈ U0, 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 U is T0.

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 B0(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 B0(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 (x1,R1) ≺U+ (x2,R2) ≺U+ (x3,R3). There are two entourages T1 and T2 such that R1 ⊇ T1 o R2, R1[x1] ⊇ T1[R2[x2]], R2 ⊇ T2 o R3, and R2[x2] ⊇ T2[R3[x3]]. It follows that R1 ⊇ T1 o T2 o R3 and R1[x1] ⊇ T1[T2[R3[x3]]]. One can rewrite those as R1 ⊇ (T1 o T2) o R3 and R1[x1] ⊇ (T1 o T2)[R3[x3]]. Since T1 o T2 is an entourage (by the Fact above), this establishes that (x1,R1) ≺U+ (x3,R3).

We turn to interpolation. We assume that we have n+1 formal balls (x1,R1), …, (xn,Rn) and (y,S), and that (xi,Ri) ≺U+ (y,S) for every i, 1≤i≤n. Hence we have n entourages T1, …, Tn such that Ri ⊇ Ti o S and Ri[xi] ⊇ Ti[S[y]] for every i, 1≤i≤n. We consider splitters ½Ti of each of the entourages Ti. Then T’ ≝ ½T1 ∩ … ∩ ½Tn 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 (xi,Ri) ≺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.
  • (xi,Ri) ≺U+ (y,S’) is because Ri ⊇ ½Ti o S‘ and Ri[xi] ⊇ ½Ti[S‘[y]]. We justify those inclusions as follows. For the first one, ½Ti o S‘ is equal to ½Ti o T’ o S, which is included in ½Ti o ½Ti o S, hence in Ti o S, and that is included in Ri. For the second one, every point z of ½Ti[S‘[y]] is such that (y,z) is in ½Ti o S‘, which is included in Ti o S, as we have just seen; so z is in Ti[S[y]], and this is included in Ri[xi]. ☐

The rounded ideal completion of B0(X,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(B0(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 (x1,R1), …, (xn,Rn) in S, there is a further formal ball (y,S) in D such that (xi,Ri) ≺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) ∈ B0(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 (x1,R1) ≺U+ (x2,R2) and (x2,R2) is in η(y), then there is an entourage T such that R1 ⊇ T o R2, R1[x1] ⊇ T[R2[x2]], and there is an entourage S such that R2 ⊇ S and R2[x2] ⊇ S[y]. Then R1 ⊇ T o S and R1[x1] ⊇ T[S[y]], so (x1,R1) is in η(y).
  • Directedness. Let (x1,R1), …, (xn,Rn) be elements of η(y). Hence there are n entourages S1, …, Sn such that Ri ⊇ Si and Ri[xi] ⊇ Si[y] for every i, 1≤i≤n. We consider splitters ½Si of each of the entourages Si. Then S’ ≝ ½S1 ∩ … ∩ ½Sn is again an entourage. We check that (y,S’) ∈ η(y) and that (xi,Ri) ≺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’.
    • (xi,Ri) ≺U+ (y,S’): we check that Ri ⊇ S’ o S’ and that Ri[xi] ⊇ S‘[S’[y]], using the fact that S’ ⊆ ½Si and that ½Si o ½Si ⊆ Si.

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 U. Indeed, if (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 T0 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 fi : Yi → Z, i ∈ I, where each Yi is a quasi-uniform space, there is a largest quasi-uniformity on Z that makes all the maps fi uniformly continuous.

Proof. For the first part, let Uj, 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 U of the filters Uj, j ∈ J, inside F(Refl(Z)), as the finite intersections of binary relations R1 ∩ … ∩ Rn (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 U is a quasi-uniformity: then U will be the desired supremum of the family (Uj)j ∈ J in the poset of quasi-uniformities on Z. In order to show this, let R ≝ R1 ∩ … ∩ Rn be any element of U. R1 is an element of some Uj, and therefore has a splitter ½R1 in Uj. We do the same with R2, …, Rn, and we let R’ be (½R1) ∩ … ∩ (½Rn). Since ½R1, …, ½Rn are all in some Uj (not necessarily the same one), R’ is in U. Moreover, it is clear that R’ o R’ is included in R. Hence U is a quasi-uniformity, as promised.

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 fi uniformly continuous. (This is a set, even when those maps form a proper class.) Let U be the supremum of F in the complete lattice of quasi-uniformities on Z. We claim that U is again in F, so that U will indeed be the largest quasi-uniformity that makes all the maps fi uniformly continuous. To this end, let R ≝ R1 ∩ … ∩ Rn be any element of U, where each Rj is in some quasi-uniformity that occurs as an element of F. Let us also fix an arbitrary i ∈ I. We must show that (fi×fi)–1 (R) is an entourage of Yi. We realize that (fi×fi)–1 (R) is equal to (fi×fi)–1 (R1) ∩ … ∩ (fi×fi)–1 (Rn). Now R1 is in some quasi-uniformity Uj that occurs as an element of F. By definition of F, fi is uniformly continuous from Yi to Z with the quasi-uniformity Uj: so (fi×fi)–1 (R1) is an entourage of Yi. We do the same with R2, …, Rn. Therefore (fi×fi)–1 (R) is a finite intersection of entourages of Yi, and is therefore itself an entourage of Yi. It follows that fi is uniformly continuous from Yi to 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,U) uniformly continuous. I have no concrete description of that quasi-uniformity, though. But we now have a quasi-uniform space S(X,U), and a uniformly continuous map η : X → S(X,U), which is injective if X is T0.

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.

  1. Is there any concrete description of the quasi-uniformity U+ on S(X,U)?
  2. Is S(X,U) is isomorphic to the Smyth-completion of X [4, Section V]?
  3. 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?
  4. With that notion of completeness, is S(X,U) complete? Remember that the formal ball completion of a hemi-metric case is not just (Yoneda-)complete, but even algebraic complete.
  5. 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.
  1. Jean Goubault-Larrecq and Kok Min Ng. A few notes on formal balls. Logical Methods in Computer Science 13(4), nov. 28, 2017.
  2. Steven Vickers. Localic Completion of Generalized Metric Spaces I. Theory and Application of Categories 14(15), pages 328-356, 2005.
  3. 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.
  4. 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
jgl-2011

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