Theory and Applications of Categories, Vol. 14, No. 15, 2005, pp. 328–356.

LOCALIC COMPLETION OF GENERALIZED METRIC SPACES I

STEVEN VICKERS

Abstract. Following Lawvere, a generalized metric space (gms) is a set X equipped with a metric map from X^{2} to the interval of upper reals (approximated from above but not from below) from 0 to ∞ inclusive, and satisfying the zero self-distance law and the triangle inequality.

We describe a completion of gms’s by Cauchy filters of formal balls. In terms of Lawvere’s approach using categories enriched over [0, ∞], the Cauchy filters are equivalent to flat left modules.

The completion generalizes the usual one for metric spaces. For quasimetrics it is equivalent to the Yoneda completion in its netwise form due to Künzi and Schellekens and thereby gives a new and explicit characterization of the points of the Yoneda completion.

Non-expansive functions between gms’s lift to continuous maps between the completions.

Various examples and constructions are given, including finite products.

The completion is easily adapted to produce a locale, and that part of the work is constructively valid. The exposition illustrates the use of geometric logic to enable point-based reasoning for locales.

1. Introduction

1.1. Quasimetric completion. This paper arose out of work aimed at providing a constructive, localic account of the completion of quasimetric spaces, that is to say the generalization of metric spaces that drops the symmetry axiom d(x, y) = d(y, x). For each such space we give a locale (a space in the approach of point-free topology) whose points make up the completion. In its constructive aspects the paper is an application of logic, and in particular the ability of geometric logic to allow constructive localic arguments that ostensibly rely on points but without assuming spatiality [Vic99], [Vic04]. However, the techniques developed seem to have some interest even from the point of view of mainstream topology and so we have tried to make them accessible to a more general mathematical readership. An earlier version of this paper appeared as [Vic98].

In its early stages this work was conducted with the support of the Engineering and Physical Sciences Research Council through the project Foundational Structures in Computer Science at the Department of Computing, Imperial College. The author also acknowledges with thanks the time spent by anonymous referees on successive drafts of this paper. Their insistence on making the work accessible to a wider mathematical readership has led to profound changes since the early report [Vic98].

Received by the editors 2004-03-15 and, in revised form, 2005-07-15. Transmitted by Ieke Moerdijk. Published on 2005-09-28. 2000 Mathematics Subject Classification: primary 54E50; secondary 26E40, 06D22, 18D20, 03G30. Key words and phrases: topology, locale, geometric logic, metric, quasimetric, completion, enriched

category.

\begin{matrix}c \\ ◯ \end{matrix} Steven Vickers, 2005. Permission to copy for private use granted.

Dropping symmetry has a big effect on the mathematics. Theories of quasimetric completion by Cauchy sequences and nets have been worked out and a summary can be seen in [Smy91] and [KS02]. One simple approach is to symmetrize the metric in an obvious way and use the symmetric theory. However, this loses information. Accounts that respect the asymmetry have substantial differences from the usual symmetric theory. The definitions of Cauchy sequence, of limit and of distance between Cauchy sequences bifurcate into left and right versions, making the theory more intricate, and, unlike the symmetric case, the completion topologies are not in general Hausdorff or even T_{1}.

This means that order enters into the topology in an essential way. Recall that the specialization order ⊑ on points is defined by x ⊑ y if every neighbourhood of x also contains y. (For a topological space in general this is a preorder, not necessarily antisymmetric, but for a T_{0} space, as also for a locale, it is a partial order. A space is T_{1} iff the specialization order is discrete, which is why in the symmetric completion, which is always Hausdorff, specialization is not noticed.) The specialization can also be extended pointwise to maps. (Maps in this paper will always be continuous.) If f, g : X → Y are maps, then f ⊑ g iff for every open V of Y, we have f^{∗}(V) ⊆ g^{∗}(V). (f^{∗} and g^{∗} denote the inverse image functions. For locales, ⊆ would be replaced by the frame order ≤.)

Thus the quasimetric completion gives access to non-T_{1} situations. This is exploited in a companion paper [Vic03], which investigates powerlocales. These include non-T_{1} analogues of the Vietoris hyperspace.

In addition to dropping symmetry, we shall also take the opportunity to generalize in two other ways of less consequence. We allow the metric to take the value +∞, and we also drop the antisymmetry axiom that if d(x, y) = d(y, x) = 0 then x = y. Following Lawvere’s definition [Law73], together with his notation for the metric, a generalized metric space (or gms) is a set X equipped with a function X(−, −) : X^{2} → [0, ∞] such that

X(x, x) = 0,  (zero self-distance)
X(x, z) ≤ X(x, y) + X(y, z).  (triangle inequality)

(We define this with slightly more constructive care in Definition 3.4.)

The construction of completion points as equivalence classes of Cauchy sequences has its drawbacks from the localic point of view, for there is no generally good way of forming “quotient locales” by factoring out equivalence relations. Instead we look for a direct canonical description of points of the completion. We shall in fact develop two approaches, and prove them equivalent. The first, and more intuitive, uses Cauchy filters of ball neighbourhoods. The second “flat completion” is more technical. It uses the ideas of [Law73], which treats a gms as a category enriched over [0, ∞], and is included because it allows us to relate our completion to the “Yoneda completion” of [BvBR98].

The basic ideas of the completion can be seen simply in the symmetric case. Let X be an ordinary metric space, and let i : X → \overline{X} be its completion (by Cauchy sequences). A base of opens of \overline{X} is provided by the open balls

B_{δ}(x) = \{ξ ∈ \overline{X} | \overline{X}(i(x), ξ) < δ\}

where δ > 0 is rational and x ∈ X. The completion is sober, and so each point can be characterized by the set of its basic open neighbourhoods, which will form a Cauchy filter. The Cauchy filters of formal balls can be used as the canonical representatives of the points of \overline{X} (Theorem 6.3). For a localic account it is therefore natural to present the corresponding frame by generators and relations, using formal symbols B_{δ}(x) as generators. In fact the relations come out very naturally from the properties characterizing a Cauchy filter.

For each point ξ of \overline{X} we can define a function \overline{X}(i(−), ξ) : X → [0, ∞), and it is not hard to show that if two points ξ and η give the same function, then ξ = η. Moreover, the functions that arise in this way are precisely those functions M : X → [0, ∞) for which

M(x) ≤ X(x, y) + M(y)  (1)
X(x, y) ≤ M(x) + M(y)  (2)
inf_{x} M(x) = 0  (3)

It follows that these functions too can be used as canonical representations of the points of \overline{X}, which can therefore be constructed as the set of such functions. These functions are the flat modules of Section 7.1. The distance on \overline{X} is then defined by \overline{X}(M, N) = inf_{x}(M(x) + N(x)), and the map i is defined by i(x) = X(−, x).

Without symmetry this becomes substantially more complicated, the major difficulty being condition (2). If M is obtained in the same way, as \overline{X}(i(−), ξ), then we consider the inequality X(x, y) ≤ \overline{X}(i(x), ξ) + \overline{X}(i(y), ξ). With symmetry (and assuming i is to be an isometry) it becomes an instance of the triangle inequality; but otherwise this breaks down.

2. Note on locales and constructivism

For basic facts about locales, see [Joh82] or [Vic89].

The present paper is presented in a single narrative line, in terms of “spaces”. The overt meaning of this is, of course, as ordinary topological spaces, and mainstream mathematicians should be able to read it as such.

However, there is also a covert meaning for locale theorists, and it is important to understand that the overt and covert are not mathematically equivalent. We do not prove any spatiality results for the locales, and anyway such results wouldn’t be constructively true. (Even the localic real line, the completion of the rationals, is not constructively spatial.) From a constructive point of view it is the covert meaning that is more important, since the locales have better properties than the topological spaces. (For example, the Heine-Borel theorem holds constructively for the localic reals – see [Vic03] for more on this.)

Locale theorists therefore need to be able to understand our descriptions of “spaces” as providing descriptions of locales – think of “space” here as being meant somewhat in the sense of [JT84]. (However, unlike [JT84], we use the word “locale” itself in the sense of [Joh82]. When working concretely with the lattice of opens we shall always call it a frame, never a locale.)

A typical double entendre will be a phrase of the form “the space whose points are XYZ, with a subbase of opens provided by sets of the form OPQ”. The topological meaning of this is clear. What is less obvious is how this can be a definition of a locale, since in general a locale may have insufficient points. However, a locale theorist familiar with the technology of frame presentations by generators and relations (see especially [Vic89]) will find that all these definitions naturally give rise to such presentations. The subbasic opens OPQ are used as the generators, and then relations translate the properties characterizing the points XYZ. The points of the locale, homomorphisms from the frame presented to the frame Ω of truth values, can be easily calculated from the presentation and should match the description XYZ.

So also with maps. A map between “spaces” is described by how it transforms points, and a topologist will have no problem checking continuity. But a locale theorist too will have no problem calculating the inverse image functions, using the generators and relations to describe frame homomorphisms.

Secretly, there is a deeper logical issue. In each case in the present paper, the description XYZ amounts to giving a geometric theory whose models are those points. It is a characteristic of these geometric theories that they can be transformed into frame presentations. What happens here is that the frame presentation makes it easy to describe homomorphisms out of the frame presented, in other words locale maps into the corresponding locale, and these “generalized points” correspond to models of the theory in toposes of sheaves over other locales. The description XYX thus describes not only the usual “global” points of the locale, of which there may be insufficient, but also the generalized points and of these there are enough. For fuller details see [Vic99], [Vic04]. Since these generalized points may live in non-classical toposes, reasoning about them has to be constructive. Moreover, there is a requirement for the reasoning to transport properly from one topos to another (along inverse image functors of geometric morphisms), which means the constructivism has to be of a more stringent geometric nature. But if one accepts these constructivist constraints then it is permissible to reason about locales in a space-like way as though they had sufficient points, and that is what is really happening in this paper.

The use of generators and relations is compatible with the practice in formal topology [Sam87], in particular as inductively generated formal topologies [CSSV03]. The geometric constructions used here are predicative. Hence the work here can also be used to give an account of completion in formal topology in predicative type theory.

As an example, consider the localic real line ℝ [Joh82]. We can describe it as the space whose points are Dedekind sections of the rationals. To be precise, a Dedekind section is a pair (L, R) of subsets of the rationals ℚ such that:

1. L is rounded lower (q ∈ L iff there is q′ ∈ L with q < q′) and inhabited.

2. R is rounded upper and inhabited.

3. If q ∈ L and r ∈ R then q < r.

4. If q < r are rationals, then either q ∈ L or r ∈ R.

(In practice, we shall not use the notation of L and R. If S is the section, then we shall write q < S for q ∈ L and S < r for r ∈ R.) In addition, we say that a subbase is given by the sets (q, ∞) = {(L, R) | q ∈ L} and (−∞, q) = {(L, R) | q ∈ R}. (Actually, with a little imagination the subbase can be extracted from the definition of Dedekind section.)

The definition can be converted into a frame presentation by taking two ℚ-indexed families of generators (q, ∞) and (−∞, q) (q ∈ ℚ) together with relations to translate the properties of a Dedekind section.

• 1 ≤ ⋁_{q∈ℚ}(q, ∞) (This says L is inhabited.)

• (q′, ∞) ≤ (q, ∞) for q < q′ (This says L is lower.)

• (q, ∞) ≤ ⋁_{q<q′}(q′, ∞) (This says L is rounded.)

• Three similar relations for R.

• (q, ∞) ∧ (−∞, r) ≤ ⋁{1 | q < r} for q, r ∈ ℚ (This expresses the third axiom.)

• 1 ≤ (q, ∞) ∨ (−∞, r) for q < r (This expresses the fourth axiom.)

It is a simple matter to check that the points are the Dedekind sections. The topology generated by the subbasis is clearly the Euclidean topology. However, note that we do not know from this that the locale presented is spatial and hence equivalent to the spatial real line – constructively, in fact, it isn’t in general.

By routine manipulation of presentations, it is also straightforward to show that the frame presented is isomorphic to that described in [Joh82, IV.1.1].

2.1. Remark. The only slight point of difficulty is Johnstone’s relation corresponding to our fourth axiom. He requires (in effect) that if ε > 0 is rational, then 1 ≤ ⋁{(q, ∞) ∧ (∞, r) | q < r and r − q < ε}. This can be deduced from our fourth axiom. In terms of Dedekind sections, if q ∈ L and r ∈ R then by subdividing the interval (q, r) in four we can find a subinterval (q′, r′) of half the length with q′ ∈ L and r′ ∈ R. Then iterate until the length is less than ε.

3. Generalized metric spaces

When we define generalized metric spaces, the distances will take their values in the range 0 to ∞. However, for the sake of the constructive development we shall be careful how we define the space of reals used for the distance. Let us write Q_{+} for the set of positive rationals.

3.1. Definition. We write \overleftarrow{[0, ∞]} for the space whose points are rounded upper subsets of Q_{+} ( rounded means that the subset has no least element), with a subbase of opens given by the sets [0, q) = {S | q ∈ S} (q ∈ Q_{+}). We call its points upper reals.

Classically, this is a well-known alternative completion of rationals to get reals. For every such rounded upper subset of Q_{+} (except for the empty set, which corresponds to ∞) there is a corresponding rounded lower subset of ℚ, showing a bijection between the finite (meaning non-empty here) upper reals and the Dedekind reals in the range [0, ∞). For most classical purposes it suffices to think of \overleftarrow{[0, ∞]} as [0, ∞]. However, the topology on \overleftarrow{[0, ∞]} is different, being the Scott topology on ([0, ∞], ≥). Occasionally this matters. The specialization order ⊑ on \overleftarrow{[0, ∞]} is reverse numerical order ≥ (0 is top, ∞ is bottom), and the arrow on \overleftarrow{[0, ∞]} is intended to indicated this.

3.2. Remark. Locale theorists should be able to translate the definition into a frame presentation by generators and relations, the relations arising directly out of the property of being rounded upper.

Ω\overleftarrow{[0, ∞]} = Fr⟨[0, q) (q∈Q_{+}) | [0, q) = ⋁_{q′<q}[0, q′) (q∈Q_{+})⟩.

It is also worth noting that \overleftarrow{[0, ∞]} is (in localic form) a continuous dcpo (dcpo = directed complete poset). Using the techniques of [Vic93], it can be got as the ideal completion of (Q_{+}, >).

3.3. Remark. For constructivist reasons, we restrict ourselves in the arithmetic we use on \overleftarrow{[0, ∞]}. Addition, multiplication, max and min are no problem, but subtraction is inadmissible because it is not continuous (with respect to the Scott topology – it would have to be antitone in its second argument, while continuous maps are always monotone with respect to the specialization order). Arbitrary infs (unions of the rounded upper subsets) are OK, but arbitrary sups are not.

3.4. Definition. A generalized metric space (or gms) is a set X equipped with a distance map X(−, −) : X^{2} → \overleftarrow{[0, ∞]} satisfying

X(x, x) = 0  (zero self-distance)
X(x, z) ≤ X(x, y) + X(y, z)  (triangle inequality)

From the definition of upper real, we see that the metric is equivalent to a ternary relation on X × X × Q_{+}, comprising those triples (x, y, q) for which X(x, y) < q.

The opposite, or conjugate, of a gms X is the gms X^{op} with the same carrier set, and distance X^{op}(x, y) = X(y, x).

3.5. Example. Let X be a gms. Then its upper powerspace F_{U}X is carried by the finite powerset FX, with distance

F_{U}X(S, T) = max_{t∈T} min_{s∈S} X(s, t).

F_{U}X is a gms, and together with two other powerspaces it is examined at length in [Vic03]. It is shown there that the points of its completion are roughly (i.e. modulo some localic provisos) equivalent to compact saturated subspaces of the completion of X, the specialization order being reverse inclusion. In fact, it is an asymmetric half of the Vietoris hyperspace, though we shall not dwell here on the technicalities of that. However, even if X is an ordinary metric space such as the rationals ℚ with the usual metric, we see that the powerspace F_{U}ℚ is not symmetric. This corresponds to the non-discrete specialization order on its completion. Moreover, in the case where S is empty and T is not, we see that the infinite distance F_{U}X(∅, T) = ∞ arises naturally.

If X is an asymmetric gms that has X(x, y) = 0 ≠ X(y, x), then we get F_{U}X({x}, {x, y}) = 0 = F_{U}X({x, y}, {x}). Hence failure of antisymmetry also can arise naturally in the powerspace.

3.6. Example. [MP91] defines a seminormed space to be a rational vector space B together with a function N : Q_{+} → Ω^{B} satisfying the following conditions whenever a, a′ ∈ B and q, q′ ∈ Q_{+}:

1. a ∈ N(q) ↔ ∃q′ < q. a ∈ N(q′);

2. ∃q. a ∈ N(q);

3. a ∈ N(q) ∧ a′ ∈ N(q′) → a + a′ ∈ N(q + q′);

4. a ∈ N(q′) → qa ∈ N(qq′);

5. a ∈ N(q) → −a ∈ N(q);

6. 0 ∈ N(q).

Condition (1) is equivalent to saying we can define a map || − || : B → \overleftarrow{[0, ∞]} by ||a|| < q iff a ∈ N(q). After that, conditions (2) and (3) say that ||a|| < ∞ and ||a+a′|| ≤ ||a|| + ||a′||, and conditions (4)-(6) say that for any rational r, ||ra|| = |r|.||a||. A metric can then be defined in the usual way by B(a, a′) = ||a − a′||, and N(q) is the open ball of radius q round 0 ∈ B.

The values ||a|| have to be in \overleftarrow{[0, ∞]}, not [0, ∞]. Constructively, the structure of the seminormed space does not tell us when ||a|| > q.

3.7. Definition. Let X and Y be generalized metric spaces. Then a homomorphism from X to Y is a non-expansive function, i.e. a function f : X → Y such that for all x_{1}, x_{2} ∈ X,

Y (f(x_{1}), f(x_{2})) ≤ X(x_{1}, x_{2})

In fact, this is a special case of the much more general definition of homomorphism between models of a geometric theory: for there is a geometric theory of generalized metric spaces.

We can specialize the definition in various ways.

3.8. Definition. A gms is –

• symmetric if it satisfies the symmetry axiom X(x, y) = X(y, x);

• finitary if X(x, y) is finite for every x, y;

• Dedekind if the distance map factors via [0, ∞] → \overleftarrow{[0, ∞]}, where [0, ∞] is the locale whose points are Dedekind sections in the range 0 to ∞.

(Classically, every gms is Dedekind. Constructively the Dedekind property corresponds to an additional ternary relation to say when X(x, y) > q.)

3.9. Definition. A Dedekind gms is –

• antisymmetric if for all x, y we have x = y or X(x, y) > 0 or X(y, x) > 0;

• a pseudometric space if it is finitary and symmetric;

• a quasimetric space if it is finitary and antisymmetric;

• a metric space if it is finitary, symmetric and antisymmetric.

The terms “pseudometric” and “quasimetric” are standard and arise out of dropping axioms from metric spaces. However, as a system of nomenclature this becomes cumbersome when we have four almost independent properties that can be dropped. We shall generally eschew it.

4. Completion by Cauchy filters of formal balls

In the classical completion \overline{X} of a metric space X, we see that a basis for the topology is provided by the open balls

B_{δ}(x) = \{ξ ∈ \overline{X} | d(x, ξ) < δ\}

for x ∈ X, δ ∈ Q_{+}. It follows that the neighbourhood filter of a point is determined by a filter of those balls. Moreover, that filter is Cauchy, containing balls of arbitrarily small radius. We present a “localic completion” in which the points are the Cauchy filters of formal open balls.

4.1. Definition. If X is a generalized metric space then we introduce the symbol “B_{δ}(x)”, a “formal open ball”, as alternative notation for the pair (x, δ) (x ∈ X, δ ∈ Q_{+}). We write

B_{ε}(y) ⊂ B_{δ}(x) if X(x, y) + ε < δ

(more properly, if ε < δ and X(x, y) < δ − ε) and say in that case that B_{ε}(y) refines B_{δ}(x).

This formal relation is intended to represent the notion that {ξ | X(y, ξ) < ε} is contained in {ξ | X(x, ξ) < δ}, with a bit to spare:

[figure: x; δ; y; ϵ]

Note an asymmetry here. Knowing when a point ξ of \overline{X} is in a ball B_{δ}(x) tells us about a distance from x to ξ, but not the other way round. The inclusion is also tacitly expecting that the distance from x (qua element of X) to y (qua point of \overline{X}) should be equal to X(x, y).

4.2. Definition. Let X be a generalized metric space.

1. A subset F of X × Q_{+} is a filter (with respect to ⊂) if

(a) it is upper – if B_{δ}(x) ∈ F and B_{δ}(x) ⊂ B_{ε}(y) then B_{ε}(y) ∈ F;

(b) it is inhabited; and

(c) any two elements of F have a common refinement in F.

2. A filter F of X ×Q_{+} is Cauchy if it contains arbitrarily small balls. In other words, for every δ ∈ Q_{+} there is some x such that B_{δ}(x) ∈ F.

3. We define \overline{X} to be the space whose points are the Cauchy filters of X × Q_{+}. For each formal ball B_{δ}(x) there is a subbasic open {F | B_{δ}(x) ∈ F }.

Note that the Cauchy property implies inhabitedness.

By taking two equal elements in the filter property 1(c), we see that a filter F is also rounded with respect to ⊂ – any element of F has a refinement in F.

Also by the filter property,

B_{δ}(x) ∩ B_{δ′}(x′) = ⋃{B_{ε}(y) | B_{ε}(y) ⊂ B_{δ}(x) and B_{ε}(y) ⊂ B_{δ′}(x′)}.

(We abuse notation here by writing B_{δ}(x) also for the corresponding subbasic.) It follows that the subbasic opens form a base of opens.

4.3. Remark. For locale theorists, the definition leads to a frame presentation

Ω\overline{X} = Fr⟨B_{δ}(x) (x ∈ X, δ ∈ Q_{+}) |
B_{δ}(x) ∧ B_{δ′}(x′) = ⋁{B_{ε}(y) | B_{ε}(y) ⊂ B_{δ}(x) and B_{ε}(y) ⊂ B_{δ′}(x′)}
(x, x′ ∈ X, δ, δ′ ∈ Q_{+})
1 = ⋁_{x∈X} B_{δ}(x) (δ ∈ Q_{+})⟩.

The ≤ direction of the first relation corresponds to the filter property 1(c), while the ≥ direction corresponds to 1(a). The second relation corresponds to the Cauchy property, which, as we have remarked, implies inhabitedness.

4.4. Definition. The map Y : X → \overline{X} is defined by

Y(z) = {B_{ε}(y) | X(y, z) < ε}.

(As will be explained in Section 7.1, Y stands for Yoneda.)

4.5. Proposition. If z ∈ X then Y(z) is indeed a point of \overline{X}.

Proof. First, if X(y, z) < ε and X(x, y) + ε < δ then X(x, z) ≤ X(x, y) + X(y, z) < δ. Hence Y(z) is upper with respect to ⊂.

To show the Cauchy property, we have X(z, z) = 0 < δ and so B_{δ}(z) ∈ Y(z) for all z. To show Y(z) is a filter, suppose X(x_{i}, z) < δ_{i} for i = 1, 2. We can find δ′_{i} < δ_{i} with

X(x_{i}, z) < δ′_{i}. Let ε = min(δ_{1} − δ′_{1}, δ_{2} − δ′_{2}). Then B_{ε}(z) refines both balls B_{δ_{i}}(x_{i}), and is in Y(z).

4.6. Lemma. Writing, as usual, ⊑ for the specialization order, we find Y(x) ⊑ Y(y) iff X(x, y) = 0.

Proof. Y(x) ⊑ Y(y) means that every B_{ε}(z) in Y(x), i.e. for which X(z, x) < ε, is also in Y(y). Taking z = x we see this implies X(x, y) = 0. For the converse, if X(z, x) < ε then X(z, y) ≤ X(z, x) + X(x, y) < ε.

4.7. Proposition. The map Y : X → \overline{X} is dense.

Proof. Considering the inverse image of a basic open, we find Y^{∗}(B_{δ}(x)) is the set {y ∈ X : X(x, y) < δ}. This contains x, and so is inhabited. It follows for any open U of \overline{X} that if Y^{∗}(U) is empty then so is U.

4.8. Remark. Constructively, the proof is easily adapted to show that Y is strongly dense [Joh89], in other words that if p is any truth value and Y^{∗}(U) ≤!^{∗}(p) then U ≤!^{∗}(p). (!^{∗} denotes the unique frame homomorphism from the initial frame Ω to another frame.) Classically, strongly dense is equivalent to dense. Of the two possible values for p, false is covered by denseness and true is trivial.

4.9. Theorem. Let ϕ : X → Y be a homomorphism between gms’s. Then ϕ lifts to a map \overline{ϕ} : \overline{X} → \overline{Y},

B_{ε}(y) ∈ \overline{ϕ}(F) iff ∃B_{δ}(x) ∈ F. B_{ε}(y) ⊃ B_{δ}(ϕ(x)).

The assignment ϕ ⟼ \overline{ϕ} is functorial.

Proof. It is clear that if F is a Cauchy filter, then so is \overline{ϕ}(F). The main point to note is that if B_{α}(x) ⊂ B_{α′}(x′), then monotonicity tells us that B_{α}(ϕ(x)) ⊂ B_{α′}(ϕ(x′)). To check continuity, note that

\overline{ϕ}^{∗}(B_{ε}(y)) = ⋃\{B_{δ}(x) | B_{ε}(y) ⊃ B_{δ}(ϕ(x))\}.

For functoriality, first \overline{Id} = Id is an immediate consequence of the fact that filters are rounded upper. Now suppose ϕ : X → Y and ψ : Y → Z.

B_{γ}(z) ∈ \overline{ψ} ∘ \overline{ϕ}(F) ⇔ ∃B_{ε}(y) ∈ \overline{ϕ}(F). B_{γ}(z) ⊃ B_{ε}(ψ(y))

⇔ ∃B_{ε}(y). ∃B_{δ}(x) ∈ F. (B_{γ}(z) ⊃ B_{ε}(ψ(y)) and B_{ε}(y) ⊃ B_{δ}(ϕ(x))

⇔ ∃B_{δ}(x) ∈ F. (B_{γ}(z) ⊃ B_{δ}(ψ ∘ ϕ(x))
⇔ B_{γ}(z) ∈ \overline{ψ ∘ ϕ}(F).

The only non-obvious step is this. Suppose we have B_{δ}(x) ∈ F such that B_{γ}(z) ⊃ B_{δ}(ψ ∘ ϕ(x)). Then there is some δ′ > δ such that B_{γ}(z) ⊃ B_{δ′}(ψ ∘ ϕ(x)). To get to the previous line, we can take B_{ε}(y) = B_{δ′}(ϕ(x)).

4.10. Remark. For locales, it is routine to check, using the generators and relations, that the formula given for the inverse image \overline{ϕ}^{∗} does indeed give a frame homomorphism. There is also a deeper logical reason, relying on the fact that only geometric constructions are used in constructing \overline{ϕ}(F) from F. This is part of the secret story that geometric reasoning allows one to deal with locales through their points.

Localically we can characterize \overline{ϕ} as the least (with respect to the specialization order ⊑) map f : \overline{X} → \overline{Y} such that for every point F, if B_{δ}(x) ∈ F then B_{δ}(ϕ(x)) ∈ f(F). Clearly \overline{ϕ} does satisfy this condition for f. To show that it is the least such, we have to take care to understand the quantification “for every point F ” in a suitably localic way. If we just quantified over the global points (maps 1 → \overline{X}) then we should need a spatiality result for the locale \overline{X}. But really, a point F here is taken to mean a generalized point, i.e. a map with \overline{X} as codomain. Given a ball B_{δ}(x), take F to be the open inclusion of B_{δ}(x) into \overline{X}. This satisfies B_{δ}(x) ∈ F – in the most generic possible way –, and we deduce, as B_{δ}(ϕ(x)) ∈ f(F), that B_{δ}(x) ≤ f^{∗}(B_{δ}(ϕ(x))). To show that \overline{ϕ} ⊑ f we require that, for every B_{ε}(y), \overline{ϕ}^{∗}(B_{ε}(y)) ≤ f^{∗}(B_{ε}(y)). But by definition \overline{ϕ}^{∗}(B_{ε}(y)) = ⋁\{B_{δ}(x) | B_{δ}(ϕ(x)) ⊂ B_{ε}(y)} and if B_{δ}(ϕ(x)) ⊂ B_{ε}(y) then B_{δ}(x) ≤ f^{∗}(B_{δ}(ϕ(x))) ≤ f^{∗}(B_{ε}(y)).

5. Examples

5.1. Products. As is well known, a product of ordinary metric spaces can be given a metric in various ways. We show here that one of them (the max-metric) provides a product in the category of generalized metric spaces and homomorphisms, and that completion preserves products: if p : X × Y → X and q : X × Y → Y are the projection homomorphisms then ⟨\overline{p}, \overline{q}⟩ : \overline{X × Y} → \overline{X} × \overline{Y} is a homeomorphism.

5.2. Theorem. The category gms of generalized metric spaces and homomorphisms has finite products.

Proof. The terminal gms 1 is the essentially unique gms with only one element. For binary products, let X and Y be two gms’s. Then we can define a distance map on their set-theoretic product by

(X × Y)((x, y), (x′, y′)) = max(X(x, x′), Y (y, y′))

The proof that this satisfies the axioms is routine. The projections p : X × Y → X and q : X × Y → Y are then homomorphisms, and so too is the pairing ⟨f, g⟩ if f : Z → X and g : Z → Y are homomorphisms.

We now show that completion preserves finite products. The nullary case is simple.

5.3. Proposition. Let 1 be the final gms. Then \overline{1} is homeomorphic to the singleton space.

Proof. The unique Cauchy filter has B_{α}(∗) for every α, where ∗ is the unique element of 1.

5.4. Theorem. Let X and Y be two gms’s. Then \overline{X × Y} is homeomorphic to \overline{X} × \overline{Y}.

Proof. Note that B_{α}(x, y) ⊂ B_{β}(x′, y′) in X × Y iff B_{α}(x) ⊂ B_{β}(x′) in X and B_{α}(y) ⊂ B_{β}(y′) in Y.

Let p : X × Y → X and q : X × Y → Y be the projections, giving a map ⟨\overline{p}, \overline{q}⟩ : \overline{X × Y} → \overline{X} × \overline{Y}.

We also have f : \overline{X} × \overline{Y} → \overline{X × Y} defined by

f(F, G) = {B_{α}(x, y) | B_{α}(x) ∈ F and B_{α}(y) ∈ G}.

To show that this is indeed a filter, suppose f(F, G) contains both B_{α}(u, v) and B_{β}(x, y). In F, B_{α}(u) and B_{β}(x) have a common refinement B_{γ}(w), and in G, B_{α}(v) and B_{β}(y) have a common refinement B_{δ}(z). Now for some ε less than both γ and δ we can find B_{ε}(w′) ⊂ B_{γ}(w) in F and B_{ε}(z′) ⊂ B_{δ}(z) in G. Then B_{ε}(w′, z′) is a common refinement for B_{α}(u, v) and B_{β}(x, y) in f(F, G).

It is routine to check that f(\overline{p}(L), \overline{q}(L)) = L, \overline{p}(f(F, G)) = G and \overline{q}(f(F, G)) = G.

5.5. Some dcpos. Our next two examples show generalized metric completion capturing continuous dcpos with their Scott topology. In general [Vic93] these can be obtained as ideal completions of transitive, interpolative orders. If (P, <) is such, then its ideal completion Idl(P) is the space whose points are ideals of P. (Ideals are dual to filters – inhabited downsets I such that any two elements of I are bounded above by an element of I.) A subbase for the topology is given by the set ↑ x = {I | x ∈ I} for x in P. (The topology is in fact the Scott topology.)

The first example shows that generalized metric completion subsumes ideal completion of preorders, in other words algebraic dcpos. Note that in this example, the gms is neither finitary nor symmetric, and the completion is not T_{1}. Moreover, the completion is in some sense not even complete, since Idl is not idempotent.

5.6. Proposition. Let (P, ≤) be a preorder, and define a distance function on it by

P (x, y) = inf{0 | x ≤ y}

(If x ≤ y then P (x, y) = 0; if x ≰ y then P (x, y) = ∞.)

Then \overline{P} is homeomorphic to Idl(P).

Proof. First note that B_{δ}(y) ⊂ B_{ε}(x) iff ε < δ and x ≤ y. This is because if P (x, y) < ε − δ then there is some element (necessarily 0) of {0 | x ≤ y} such that 0 < ε − δ, and so x ≤ y.

Now suppose F is a Cauchy filter over P. If B_{α}(x) ∈ F, then B_{ε}(x) ∈ F for all ε. For we can find some B_{ε}(y) ∈ F, and then some common refinement B_{δ}(z) ∈ F for B_{α}(x) and B_{ε}(y). Then x ≤ z and δ < ε, so B_{δ}(z) ⊂ B_{ε}(x) and B_{ε}(x) ∈ F.

If we define I(F) = {x ∈ P | B_{1}(x) ∈ F }, then we find I(F) is an ideal in P and F = {B_{ε}(x) | x ∈ I(F)}.

Conversely, if I is an ideal and we define F (I) = {B_{ε}(x) | x ∈ I}, then F (I) is a Cauchy filter of balls and I = I(F (I)).

The next example shows an example of a non-algebraic continuous dcpo.

5.7. Proposition. Let \overrightarrow{ℚ} be the rationals equipped with a distance map \overrightarrow{ℚ}(x, y) = x ˙−y = max(0, x − y) (truncated minus). Then its completion is homeomorphic to the ideal completion of (ℚ, <), which we may write as \overrightarrow{(−∞, ∞]}.

Proof. Note that B_{ε}(y) ⊂ B_{δ}(x) iff ε < δ and x − δ < y − ε.

If I is an ideal of (ℚ, <), define F (I) = {B_{δ}(x) | x − δ ∈ I}. This is a Cauchy filter for \overrightarrow{ℚ}. The other way round, if F is a Cauchy filter, define I(F) = \{x − δ | B_{δ}(x) ∈ F \}, an ideal. Clearly if I is an ideal then I = I(F (I)). If F is a Cauchy filter, we must show F (I(F)) ⊆ F. Suppose x − α = y − β where B_{β}(y) ∈ F. Find B_{ε}(z) ∈ F with B_{ε}(z) ⊂ B_{β}(y) and ε < α. Then B_{ε}(z) ⊂ B_{α}(x) so B_{α}(x) ∈ F.

5.8. Dedekind sections. In this section we show the equivalence between two different completions of the rationals: by Dedekind sections (as in Section 2), and by Cauchy filters. The metric on the rationals ℚ is given by ℚ(q, r) = |q − r|, and we show \overline{ℚ} ≅ ℝ.

Notice how our approach circumvents a certain logical oddity of the usual account. Since the reals are the metric completion of the rationals, it might seem that this is one way to define the reals. But the theory of metric completion relies on having the reals already available as the metric values. So the usual classical story appears to have redundancy: first complete in the special case of the rationals, then define the notion of metric space, then define metric completion in general. Constructively, however, we are alert to a distinction between the Dedekind reals and the upper reals. It is the upper reals that are needed for the theory of metric completion and we then could define the Dedekind reals as the completion of the rationals.

5.9. Theorem. ℝ, the space of Dedekind sections of ℚ, is homeomorphic to the completion of ℚ as metric space.

Proof. Note that B_{α}(x) ⊂ B_{β}(y) iff y − β < x − α and x + α < y + β.

If F is a Cauchy filter, define a Dedekind section S(F) by q < S(F) if q = x − α for some B_{α}(x) ∈ F, and S(F) < r if r = x+α for some B_{α}(x) ∈ F. To show it is a Dedekind section, suppose q = x − α < S(F) < r = y + β, with B_{α}(x), B_{β}(y) ∈ F. Choosing B_{ε}(z) a common refinement in F for B_{α}(x) and B_{β}(y), we see that

q = x − α < z − ε < z + ε < y + β = r.

Now suppose we have arbitrary q < r in ℚ. Choose B_{δ}(x) ∈ F with δ < (r − q)/2. If q ≤ x − δ then q < S(F), while if x − δ ≤ q (recall that the order on ℚ is decidable) then x + δ < q + (r − q) = r and S(F) < r.

Now if S is a Dedekind section, define the Cauchy filter F (S) = {B_{δ}(x) | x − δ < S < x + δ}. Note that if q < S < r, then by taking x = (r + q)/2 and δ = (r − q)/2 we can find B_{δ}(x) ∈ F (S) with q = x − δ and r = x + δ. It follows that S = S(F (S)). It also follows that F (S) is a filter, since if B_{δ}(x), B_{ε}(y) ∈ F (S) then we can find q < S < r with max(x − δ, y − ε) < q and r < min(x + δ, y + ε). The Cauchy property follows from Remark 2.1.

Finally we must show that if F is a Cauchy filter then F (S(F)) ⊆ F. Suppose B_{α}(x) ∈ F (S(F)) with x − α = y_{1} − β_{1}, x + α = y_{2} + β_{2}, and each B_{β_{i}}(y_{i}) in F. If B_{δ}(z) is a common refinement in F for the B_{β_{i}}(y_{i})’s then B_{δ}(z) ⊂ B_{α}(x) so B_{α}(x) ∈ F.

6. Completion in symmetric case

For this section, we take X to be a symmetric gms, for example a pseudometric. In this case, we can weaken the characterization of filter somewhat and at the same time relate it to Condition (2) in the Introduction.

Note that if a set F of formal balls is rounded upper, and B_{δ}(x) ∈ F, then we can find B_{δ′}(x) ∈ F for some δ′ < δ. For if B_{ε}(y) ⊂ B_{δ}(x) then B_{ε}(y) ⊂ B_{δ′}(x) for some δ′ < δ.

6.1. Lemma. Let F be a Cauchy rounded upper set of formal balls over X. Then the following are equivalent.

1. F is a filter.

2. If B_{α}(x), B_{β}(y) ∈ F then X(x, y) < α + β.

3. Any two balls in F with the same radius have a common refinement in F.

Proof. The proof is unexpectedly intricate, but we have avoided using the rearranged triangle inequality

X(x, y) ≥ |X(x, z) − X(y, z)|,

which is not constructively valid except in the case of a Dedekind gms. It is not hard to prove (1)⇔(2) directly; the hard part is the diversion via (3).

(1)⇒(3) a fortiori.

(2)⇒(1): Suppose B_{α_{i}}(x_{i}) ∈ F (i = 1, 2). Find δ such that B_{α_{i}−δ}(x_{i}) ∈ F and z such that B_{δ/2}(z) ∈ F. Then

X(x_{i}, z) + δ/2 < α_{i} − δ + δ/2 + δ/2 = α_{i}

so B_{δ/2}(z) ⊂ B_{α_{i}}(x_{i}).

For (3)⇒(2) we proceed by a sequence of claims.

First, by symmetry note that if B_{α}(x) ⊂ B_{β}(y) then B_{α}(y) ⊂ B_{β}(x).

Second, if F contains both B_{α}(x) and B_{β}(x), then it also contains B_{(α+β)/2}(x).

Third, suppose F contains balls B_{α_{i}}(x_{i}) (i = 1, 2) and let α = max(α_{1}, α_{2}). Then the balls B_{α}(x_{i}) have a common refinement B_{β}(y) in F with β ≤ (α_{1} + α_{2})/2. To see this, use condition (3) to find a common refinement B_{β′}(y) in F for B_{α}(x_{1}) and B_{α}(x_{2}). Without loss of generality we can assume α_{2} ≤ α_{1} = α. Now B_{β′}(y) ⊂ B_{α_{1}}(x_{2}), so B_{β′}(x_{2}) ⊂ B_{α_{1}}(y) and B_{α_{2}}(x_{2}) ⊂ B_{α_{1}−β′+α_{2}}(y). Now both B_{β′}(y) and B_{α_{1}−β′+α_{2}}(y) are in F, so B_{β}(y) ∈ F where β = (α_{1} + α_{2})/2.

Fourth, if F contains B_{α}(x) and B_{β}(y), then X(x, y) < α + 2β. Let γ = max(α, β), and let B_{δ}(z) be a common refinement in F for B_{γ}(x) and B_{γ}(y), with δ ≤ (α + β)/2. We have

X(x, y) ≤ X(x, z) + X(z, y) < 2γ.

Now we consider various cases. If α ≤ β, then 2γ = 2β < α + 2β. If β ≤ α ≤ 2β, then 2γ = 2α ≤ α+2β. The last case is 2β < α. Since δ ≤ (α+β)/2, we have δ−β ≤ (α−β)/2. By induction on the number of halvings needed to get this difference less than β, we can assume X(z, y) < δ + 2β, and then

X(x, y) ≤ X(x, z) + X(z, y) < γ − δ + δ + 2β = α + 2β.

To complete the proof of the theorem, suppose B_{α}(x), B_{β}(y) ∈ F. Find ε such that B_{α−2ε}(x), B_{β−2ε}(y) ∈ F, and then z such that B_{ε}(z) ∈ F. By the fourth claim we have

X(x, y) ≤ X(x, z) + X(y, z) < α − 2ε + 2ε + β − 2ε + 2ε = α + β.

6.2. Example. Condition (3) in Theorem 6.1 is in asymmetric generality weaker than the usual filter condition. This can be seen in Example 5.7, where any Cauchy rounded upper set F of balls over \overrightarrow{ℚ} has the condition. For suppose B_{α}(x), B_{α}(y) ∈ F. Without loss of generality we can suppose x ≤ y. By roundedness there is some ε such that B_{α−ε}(y) ∈ F, and then B_{α−ε}(y) is a common refinement for B_{α}(x) and B_{α}(y). Now consider the Cauchy rounded upper set

F = {B_{δ}(x) | ∃n ∈ ℕ. (n ≥ 1, δ > 1/n and x − δ < −n)}.

It contains B_{1.1}(0) and B_{0.6}(−1.5). If B_{δ}(x) is a common refinement for those two then δ < 0.6 and x − δ > −1.1. Hence if x − δ < −n for some 1 ≤ n ∈ ℕ we must have n = 1. But then δ > 1/n gives a contradiction.

We can now show classically that for a metric space X the points of our completion are the same as for the usual completion (which we shall write i : X → X′) by Cauchy sequences. If ξ = (x_{n}) and η = (y_{n}) are two Cauchy sequences, then as is well known their distance X′(ξ, η) is lim_{n→∞} X(x_{n}, y_{n}).

6.3. Theorem. (Classically) Let X be a symmetric gms and let X′ be its Cauchy completion.

1. For every Cauchy sequence ξ, the set F_{ξ} = {B_{δ}(x) | X′(i(x), ξ) < δ} is a Cauchy filter.

2. Let ξ = (x_{n}) and η = (y_{n}) be two Cauchy sequences. Then the sequences are equivalent iff F_{ξ} = F_{η}.

3. If F is a Cauchy filter, then there is a Cauchy sequence ξ = (x_{n}) such that F = F_{ξ}.

4. The points of X′ are in bijective correspondence with the Cauchy filters F.

Proof. (1) It is straightforward to show that F_{ξ} is a Cauchy rounded upper set. Then condition (2) in Lemma 6.1 is an instance of the triangle inequality in X′.

(2) Clearly F_{ξ} = F_{η} iff for all x ∈ X we have X′(i(x), ξ) = X′(i(x), η).

⇒: If ξ and η are equal in the usual completion, in other words X′(ξ, η) = 0, then for all x, X′(i(x), ξ) = X′(i(x), η).

⇐: X′(ξ, η) = lim_{n→∞} X′(i(x_{n}), η) = lim_{n→∞} X′(i(x_{n}), ξ) = 0, so the sequences are equivalent.

(3) We can find a sequence ξ = (x_{n}) such that B_{2^{−n}}(x_{n}) ∈ F. Then by condition (2) in Lemma 6.1, if k ≥ 0 then

X(x_{n}, x_{n+k}) < 2^{−n} + 2^{−n−k} ≤ 2^{−n+1}

and it follows that (x_{n}) is Cauchy. We must show that B_{δ}(x) ∈ F iff X′(i(x), ξ) < δ. If B_{δ}(x) ∈ F, there is some δ′ < δ with B_{δ′}(x) ∈ F. Choose n with 2^{−n+1} < δ − δ′. Then

X′(i(x), ξ) ≤ X(x, x_{n}) + X′(i(x_{n}), ξ) < δ′ + 2^{−n} + 2^{−n} < δ.

Conversely, suppose X′(i(x), ξ) < δ. Choose δ′ < δ such that X′(i(x), ξ) < δ′, and then find m such that for every n ≥ m we have X(x, x_{n}) < δ′. Choose n ≥ m such that 2^{−n} < δ − δ′. Then B_{2^{−n}}(x_{n}) ⊂ B_{δ}(x), so B_{δ}(x) ∈ F.

(4) now follows.

Symmetry allows us to define a continuous metric on the localic completion.

6.4. Definition. Let X be a symmetric gms. Then the map \overline{X}(−, −) : \overline{X}×\overline{X} → \overleftarrow{[0, ∞]} is defined by

\overline{X}(F, G) = inf\{α_{1} + α_{2} | ∃x ∈ X. (B_{α_{1}}(x) ∈ F and B_{α_{2}}(x) ∈ G)\}.

6.5. Remark. As in previous examples, this definition of the action on points can easily be made localic by converting into a frame homomorphism for the inverse image. (Or, logically, one can use the geometricity of the construction.)

6.6. Proposition.

1. The map \overline{X} satisfies the axioms for a symmetric gms.

2. If x ∈ X then \overline{X}(Y(x), F) = inf\{δ | B_{δ}(x) ∈ F \}.

3. The Yoneda map Y : X → \overline{X} is an isometry.

4. If X is Dedekind (as is always the case classically), then the (continuous) map \overline{X}(−, −) factors via [0, ∞].

Proof. (1) Symmetry and zero self-distance are obvious. For the triangle inequality, suppose we have \overline{X}(F, G) < α_{1} + α_{2} arising from B_{α_{1}}(x) ∈ F and B_{α_{2}}(x) ∈ G, and \overline{X}(G, H) < β_{1} + β_{2} arising from B_{β_{1}}(y) ∈ G and B_{β_{2}}(y) ∈ H. By Lemma 6.1 (2) we have X(x, y) < α_{2} + β_{1}, and it follows that B_{α_{1}}(x) ⊂ B_{α_{1}+α_{2}+β_{1}}(y) hence \overline{X}(F, H) < α_{1} + α_{2} + β_{1} + β_{2}.

(2) (This also appears in a different form as Proposition 7.8.) If B_{α_{1}}(y) ∈ Y(x) and B_{α_{2}}(y) ∈ F then B_{α_{2}}(y) ⊂ B_{α_{1}+α_{2}}(x) so B_{α_{1}+α_{2}}(x) ∈ F. The other way round, if B_{δ}(x) ∈ F, then B_{δ′}(x) ∈ F for some δ′ < δ. Then B_{δ−δ′}(x) ∈ Y(x), so δ = δ−δ′+δ′ ∈ \overline{X}(Y(x), F).

(3) follows easily from (2).

(4) We must describe a Dedekind section for \overline{X}(F, G). The right half (which may be empty, to allow for ∞) follows immediately from the definition:

\overline{X}(F, G) < r if ∃B_{α_{1}}(x) ∈ F, B_{α_{2}}(x) ∈ G. α_{1} + α_{2} ≤ r.

For the left half, which allows us to calculate the inverse image of (q, ∞], we define

\overline{X}(F, G) > q if ∃B_{ε}(y) ∈ F, B_{ε}(z) ∈ G. X(y, z) > q + 2ε.

Suppose q < \overline{X}(F, G) < r, with balls B_{α_{1}}(x), B_{α_{2}}(x), B_{ε}(y) and B_{ε}(z) as in the definition. Then

q + 2ε < X(y, z) ≤ X(y, x) + X(x, z) < ε + α_{1} + α_{2} + ε ≤ r + 2ε

LOCALIC COMPLETION OF GENERALIZED METRIC SPACES I  345

so q < r.

Now suppose q, r are elements of Q_{+} with q < r and let ε = (r − q)/5. Choose B_{ε}(y) in F and B_{ε}(z) in G. We have q + 2ε < r − 2ε, so either X(y, z) > q + 2ε, in which case \overline{X}(F, G) > q, or X(y, z) < r − 2ε. In this latter case B_{ε}(y) ⊂ B_{r−ε}(z), so B_{r−ε}(z) ∈ F and we find \overline{X}(F, G) < r.

Note that Lemma 6.1 (2) states an instance of the triangle inequality,

\overline{X}(Y(x), Y(y)) = X(x, y) ≤ \overline{X}(Y(x), F) + \overline{X}(F, Y(y)).

We cannot expect to get a generalized metric like this, in the form of a continuous map \overline{X} × \overline{X} → \overleftarrow{[0, ∞]}, in the asymmetric case. For suppose we do have such a map, with Y an isometry. Suppose X(x, x′) = 0 so that, by Lemma 4.6, Y(x) ⊑ Y(x′). By the monotonicity (with respect to ⊑) of continuous maps, we find that for all y we have X(x, y) = \overline{X}(Y(x), Y(y)) ≥ \overline{X}(Y(x′), Y(y)) = X(x′, y) and it follows that X(x′, x) = 0. But we have already seen examples (e.g. the algebraic dcpos) where this does not happen.

We end this section with a result for constructive mathematicians. It is well known in classical metric space theory that Cauchy completion is idempotent: i : X′ → X′′ is a homeomorphism (where, as in Theorem 6.3, we write X′ for the Cauchy completion of X). This relies on symmetry – it is not the case in general for the Yoneda completion of quasimetrics. Now Theorem 6.3 shows that in the symmetric case our completion is equivalent to Cauchy completion, so ours too is idempotent. However, Theorem 6.3 uses classical reasoning principles. The next result shows this idempotence constructively.

6.7. Proposition. Let X be a symmetric gms, and let X′ be the set of points of the locale \overline{X} (the construction of X′ is not geometric, but it is topos-valid), equipped with the symmetric generalized metric arising from the map \overline{X}(−, −) . Since X is discrete, the map Y : X → \overline{X} factors via an isometry 𝔜 : X → X′. Then \overline{𝔜} : \overline{X} → \overline{X′} is a homeomorphism.

Proof. (The \overline{𝔜} referred to here is definitely intended as a map of locales. However, we shall continue our policy of giving a geometric, point-based argument, and leaving it to the reader either to believe the tricks of geometric reasoning or to work out the frame homomorphisms.) By definition B_{α}(G) ∈ \overline{𝔜}(F) iff there is some B_{β}(x) ∈ F with B_{β}(𝔜(x)) ⊂ B_{α}(G), i.e. B_{α−β}(x) ∈ G.

For an inverse, we define j : \overline{X′} → \overline{X} by j(K) = \{B_{δ}(x) | B_{δ}(𝔜(x)) ∈ K\}. It is routine to show j(\overline{𝔜}(F)) = F. We must show that if K is a Cauchy filter over X′ then \overline{𝔜}(j(K)) = K. B_{α}(F) is in \overline{𝔜}(j(K)) iff it is refined by some B_{β}(𝔜(x)) in K, so clearly \overline{𝔜}(j(K)) ⊆ K. For the opposite inclusion, suppose B_{α}(F) ∈ K. Find ε such that B_{α−2ε}(F) ∈ K, and x such that B_{ε}(x) ∈ F. Then \overline{X}(𝔜(x), F) < ε, so B_{α−2ε}(F) ⊂ B_{α−ε}(𝔜(x)) ⊂ B_{α}(F).

We have not yet shown that j(K) is a filter. If B_{α_{i}}(𝔜(x_{i})) ∈ K (i = 1, 2) then they have a common refinement B_{β}(F) ∈ K, and that is refined by some B_{γ}(𝔜(y)) in K. Then B_{γ}(y) is a common refinement for the B_{α_{i}}(x_{i})s in j(K).

7. Yoneda completion

In this Section we move to material that is more technical. One established approach to quasimetric completion is the Yoneda completion, which has appeared in sequential form in [BvBR98] and in netwise form in [KS02]. This is inspired by the observation [Law73] that quasimetric spaces can be understood as an application of enriched category theory, the enrichment being over [0, ∞] (as poset under ≥), with the triangle inequality corresponding to composition and the zero self-distance law being identity morphisms. We now show that our completion gives a new and direct characterization of the points of the netwise version of the Yoneda completion.

In Section 1.1, it was mentioned that each point of the completion of a symmetric X could be represented by the function showing the distance from every element of X. Three conditions were given characterizing such functions, but condition (2) was clearly problematic for asymmetric completion. The observation from enriched category theory is that, considering a gms as a category enriched over [0, ∞], a function satisfying condition (1) alone is a module over the gms. We write X̂ for the space of such modules, and there is a “Yoneda embedding” of X in X̂. Our completion and the Yoneda completion are then both identified as subspaces of X̂ containing the image of X. The Yoneda completion is defined as the smallest subspace that contains that image and is complete in the sense of being closed under taking limits – of Cauchy sequences in one version, or of Cauchy nets in another (giving a different completion). In [BvBR98] there are two techniques used for constructing this subspace: from above, as intersection of complete subspaces containing the image of X, and from below, as the subspace of all points of X̂ that are limits of Cauchy sequences of points in the image of X. In [KS02] the subspace is constructed as a quotient of the class of all Cauchy nets in X. By contrast our approach deriving from the Cauchy filter property characterizes the points of the subspace directly and turns out to be a “flatness” property of the modules in the same sense as a flat functor or a flat module over a ring (see, e.g., [MLM92, p. 381]).

The present Section falls into two halves. Subsection 7.1 shows the relationship of our Cauchy filters with the basic notions of [Law73], and proves the flatness condition. This part has constructive localic content in the same way as most of the rest of this paper. Subsection 7.12 sets out the comparison with the Yoneda completion. Its results are ones of topological spaces, and make essential use of classical reasoning principles.

7.1. Completion by flat modules. The presentation in [Law73] has been so influential in the Yoneda completion that it would be unnatural not to show here how the Cauchy filter ideas fit in with the enriched category theory. In fact our work was originally formulated in terms of the flat modules, and the Cauchy filters came later. However, those readers who are less eager to swim in the abstraction of enriched categories might want some stepping stones for crossing this subsection to the next one without getting their feet too wet. The main points to note are these.

1. Modules (or more specifically left modules) over a gms correspond to a generalization of Cauchy filter that (in terms of Definition 4.2 and the remarks following it) is upper and rounded – the other filter properties and the Cauchy property are omitted. See Proposition 7.3.

2. Under this correspondence, flat left modules correspond to Cauchy filters.

3. There is also a technical transformation. In the module language, rounded upper sets F of formal balls are represented by maps M : X → \overleftarrow{[0, ∞]}, with M(x) < δ iff B_{δ}(x) ∈ F. This is not deep, but makes a difference to the appearance of the arguments in Section 7.12.

The general enriched theory is for enrichment over a monoidal category (V, ⊗, I). An enriched category X comprises a set (also denoted X) of objects, together with, for each x, y ∈ X a “hom-set” X(x, y), actually an object of V. Then composition and identities are expressed by V-morphisms from X(x, y) ⊗ X(y, z) to X(x, z) and from I to X(x, x). These must satisfy additional conditions corresponding to associativity and the unit laws, but they are trivial if V is a poset, and this is the case in our particular example where V is (\overleftarrow{[0, ∞]}, ≥) and the monoidal structure is given by + and 0. Then composition becomes the triangle inequality X(x, y)+X(y, z) ≥ X(x, z) and the identities are zero self-distance 0 ≥ X(x, x).

If X is enriched over V, then a left module over X is a function M : X → ob V with, for every x, y ∈ X an action α_{xy} : X(x, y) ⊗ M(y) → M(x), a morphism in V, satisfying various conditions that are trivially satisfied if V is a poset.

Fuller details are in [Law73]. We have replaced [0, ∞] by \overleftarrow{[0, ∞]}. That makes no difference classically, but one constructive effect is that our V is not monoidal closed, since the internal hom corresponds to subtraction, which is not continuous on \overleftarrow{[0, ∞]}.

There are two paradigm enrichments, which influence the language used. If V is Set, then enriched categories are just ordinary categories, and left modules are presheaves. Then the map Y of Definition 4.4, treated as a map from X to the space X̂ of left modules, corresponds to the Yoneda embedding. Our \overline{X} corresponds to the category of flat presheaves, which is equivalent to the ind-completion of a category. On the other hand, the word module itself comes from the situation where V is the category Ab of Abelian groups. A ring is an enriched category over Ab of a simple kind, having only one object, and then modules are just as in ring theory.

For the rest of this section we shall take X to be a fixed gms.

7.2. Definition.

1. A left module over X is a map M : X → \overleftarrow{[0, ∞]} such that X(x, y) + M(y) ≥ M(x).

2. A right module over X is a left module over the opposite gms X^{op}, in other words a map M : X → \overleftarrow{[0, ∞]} such that M(x) + X(x, y) ≥ M(y).

The whole theory of modules is self-dual, by replacing X by X^{op}. We shall normally state our results for left modules.

7.3. Proposition. A left module over X is equivalent to a rounded upper set (under ⊂) of formal balls over X.

Proof. A map M : X → \overleftarrow{[0, ∞]} is described by the set F (M) of formal balls B_{α}(x) such that M(x) < α, and a set F of formal balls arises in this way iff it satisfies the condition that B_{α}(x) ∈ F ⟺ ∃α′ < α. B_{α′}(x) ∈ F. The module condition now corresponds to saying that if X(x, y) < δ and B_{β}(y) ∈ F then B_{δ+β}(x) ∈ F, in other words (writing α for δ + β) F is upper under ⊂. Suppose F is also rounded under ⊂. Then as already noted F satisfies the slightly stronger condition that B_{α}(x) ∈ F ⇒ ∃α′ < α. B_{α′}(x) ∈ F, and this is needed in defining the map M.

We write X-Mod or X̂ for the space whose points are the left modules over X (and Mod-X for the space of right modules). Each formal ball B_{α}(x) gives rise to a subbasic open {M | M(x) < α}, but they do not form a base. The fact that they do for the subspace \overline{X} uses the filter property. The specialization order on X̂, given by inclusion of rounded upper sets of balls, corresponds to the pointwise reverse numerical order on maps X → \overleftarrow{[0, ∞]}.

7.4. Proposition. X̂ is a distributive lattice with respect to the specialization order.

Proof. For rounded upsets of balls, meet and join are given by intersection and union. For maps to \overleftarrow{[0, ∞]} they are given by pointwise numerical max and min (respectively).

Since we write ⊑ for the specialization order, we shall write ⊓ and ⊔ for meet and join with respect to it. These operations are in fact continuous (and localically, X̂ is a distributive lattice object in the category of locales).

7.5. Proposition. If y ∈ X then Y(y) is defined as a left module by Y(y)(x) = X(x, y). We shall also often denote Y(y) by X(−, y).

From this we see that Y is indeed the analogue of the Yoneda embedding. (However, it is not an embedding in the topological sense.)

7.6. Definition. A left module of the form Y(y) (i.e. X(−, y)) is called representable.

A representable right module is one of the form X(x, −), defined by X(x, −)(y) = X(x, y).

If M is a right module, then so is λ ⊗_{1} M for any point λ of \overleftarrow{[0, ∞]}, defined by (λ ⊗_{1} M)(x) = λ + M(x). (As we shall see shortly, the notation is justified by treating M as a left module over the one-element gms 1.) This gives a map ⊗_{1} : \overleftarrow{[0, ∞]}× Mod-X → Mod-X. Similarly if M is a left module, then we write M ⊗_{1} λ, giving a map from X-Mod ×\overleftarrow{[0, ∞]} to X-Mod.

7.7. Definition.

1. Let M and N be right and left modules respectively over a gms X. Then their tensor product M ⊗_{X} N is inf_{x}(M(x) + N(x)), giving a map ⊗_{X} : Mod-X × X-Mod → \overleftarrow{[0, ∞]}.

2. A left X-module M is flat iff the map − ⊗_{X} M : Mod-X → \overleftarrow{[0, ∞]} preserves finite meets.

In the case where X is symmetric, Mod-X = X-Mod and so ⊗_{X} : X̂ × X̂ → \overleftarrow{[0, ∞]}. The restriction of this to \overline{X} is the metric of Definition 6.4.

Note that − ⊗_{X} M preserves the nullary meet iff 0 ⊗_{X} M = 0, i.e. inf_{z} M(z) = 0. If X is finitary (no infinite distances), then this condition in itself is enough to show that M too is finitary: for if we choose z so that M(z) < 1, then for any x we have M(x) ≤ X(x, z) + M(z) ≤ X(x, z) + 1, which is finite.

7.8. Proposition. M ⊗_{X} X(−, y) = M(y), and X(x, −) ⊗_{X} N = N(x).

Proof. M ⊗_{X} X(−, y) = inf_{x}(M(x) + X(x, y)). By the module law this is ≥ M(y), but by choosing x = y we can attain that lower bound.

From this it is plain that representable modules are flat.

7.9. Proposition. Let M be a left module. Then the following conditions are equivalent.

1. − ⊗_{X} M preserves binary meets.

2. If x_{i} ∈ X and λ_{i} is an upper real (i = 1, 2), then inf_{z}(max_{i}(λ_{i} +X(x_{i}, z))+M(z)) ≤ max_{i}(λ_{i} + M(x_{i})).

3. The same as (2), but with the λ_{i}s restricted to be in Q_{+}.

4. If M(x_{i}) < δ_{i} (i = 1, 2) then there is some y for which X(x_{i}, y) + M(y) < δ_{i}.

5. If M(x_{i}) < δ_{i} (i = 1, 2) then there are y ∈ X and ε ∈ Q_{+} for which M(y) < ε and X(x_{i}, y) + ε < δ_{i}.

Proof. (1)⇒(2): (2) is equivalent to saying that − ⊗_{X} M preserves binary meets of right modules of the form λ ⊗_{1} Y(x).

(2)⇒(1):Let N_{1} and N_{2} be right X-modules, so we want to show that (N_{1}⊓N_{2})⊗_{X}M = (N_{1} ⊗_{X} M) ⊓ (N_{2} ⊗_{X} M), i.e.

inf_{z}(max(N_{1}(z), N_{2}(z)) + M(z)) = max(inf_{z}(N_{1}(z) + M(z)), inf_{z}(N_{2}(z) + M(z)))

The ≥ direction is obvious. For ≤, we see that the right hand side is

inf_{x_{1}x_{2}}(max(N_{1}(x_{1}) + M(x_{1}), N_{2}(x_{2}) + M(x_{2})))

so we must show that for every x_{1} and x_{2} we have

inf_{z}(max(N_{1}(z), N_{2}(z)) + M(z)) ≤ max(N_{1}(x_{1}) + M(x_{1}), N_{2}(x_{2}) + M(x_{2}))

But

max(N_{1}(z), N_{2}(z)) + M(z) ≤ max(N_{1}(x_{1}) + X(x_{1}, z), N_{2}(x_{2}) + X(x_{2}, z)) + M(z)

so we can apply condition (2) with λ_{i} = N_{i}(x_{i}).

(2)⇔(3): ⇒ is a fortiori. For ⇐, use the fact that any upper real is the inf of the rationals greater than it.

(3)⇒(4): If M(x_{i}) < δ_{i} then max(δ_{2} + M(x_{1}), δ_{1} + M(x_{2})) < δ_{1} + δ_{2}, so there is some z with δ_{2} + X(x_{1}, z) + M(z) < δ_{1} + δ_{2}, δ_{1} + X(x_{2}, z) + M(z) < δ_{1} + δ_{2}.

(5)⇒(3): If max_{i}(λ_{i} + M(x_{i})) < q then M(x_{i}) < q − λ_{i} = δ_{i} (say). Find y, ε with M(y) < ε and X(x_{i}, y) + ε < δ_{i}; then

LHS ≤ max_{i}(λ_{i} + X(x_{i}, y)) + M(y) < max_{i}(λ_{i} + δ_{i}) = q.

(4)⇒(5): Take y as in (4). Then we can find α_{i}, β_{i} ∈ Q_{+} such that X(x_{i}, y) < α_{i}, M(y) < β_{i}, α_{i} +β_{i} ≤ δ_{i}. Let ε = min(β_{1}, β_{2}). Then M(y) < ε, X(x_{i}, y)+ε < α_{i} +ε ≤ δ_{i}.

7.10. Theorem. As a subspace of X̂, the completion \overline{X} is the space of flat left modules.

Proof. The Cauchy property says inf_{x} M(x) = 0, which (as has been noted) is preservation of nullary meets. The filter property is condition (5) of Proposition 7.9, equivalent to preservation of binary meets.

7.11. Remark. Localically, \overline{X} is a sublocale of X̂. This is most easily understood through the fact that its frame Ω\overline{X}, a quotient of ΩX̂, is presented using extra relations that correspond to the flatness conditions on points.

In terms of modules, condition (3) in Theorem 6.1 can be rephrased as

∀x, y ∈ X. inf_{z}(max(X(x, z), X(y, z)) + M(z)) = max(M(x), M(y)),

in other words that − ⊗_{X} M preserves binary meets of representable modules. Thus Theorem 6.1 shows that this is sufficient for flatness in the symmetric case. For the general case (Proposition 7.9 (2)) − ⊗_{X} M must preserve binary meets of modules of the form λ ⊗_{1} X(x, −).

7.12. Classical correspondence with the Yoneda completion. In this subsection we shall show how the our completion relates to the Yoneda completion. As explained in [KS02], there are two different Yoneda completions: the sequential Yoneda completion of [BvBR98], and the netwise version of [KS02]. Our completion corresponds to the netwise Yoneda. A typical illustration of the difference is Example 5.6, in which our completion and netwise Yoneda give the ideal completion of a poset but the sequential Yoneda gives the ω-chain completion. However, we shall find it convenient to adapt the sequential account of [BvBR98] rather than use the somewhat different construction in [KS02].

Throughout this subsection we have to use classical reasoning principles. For instance, we assume arbitrary infs and sups of real numbers.

7.13. Definition. Let X be a gms. A net (x_{i})_{i∈I} of points (i.e. a family of points indexed by a directed set I) is Cauchy iff for every ε > 0 there is some l such that for all n ≥ m ≥ l we have X(x_{m}, x_{n}) ≤ ε. (More precisely, this is forward Cauchy. A net is backward Cauchy in X iff it is forward Cauchy in X^{op}.)

The point x is a (forward) limit of (x_{i}) iff for every point y in X we have

X(x, y) = inf_{n∈I} sup_{k≥n} X(x_{k}, y)

X is complete iff every Cauchy net in X has a limit. A subset V ⊆ X is complete in X iff every Cauchy net in V has a limit in V. (Note that the definition of limit still uses “for all y in X”, not “for all y in V ”.)

7.14. Proposition. (Classically) Let X be a gms.

1. If (x_{i})_{i∈I} is a Cauchy net in X for which x and x′ are both limits, then X(x, x′) = X(x′, x) = 0.

2. X̂ is a gms by X̂(M, N) = sup_{x∈X}(N(x) ˙−M(x)).

3. X̂ is complete: if (M_{i})_{i∈I} is a Cauchy net of left modules then its limit M is unique and given by M(x) = lim_{n} M_{n}(x).

Proof. These results are essentially already in [BvBR98], but with sequences instead of nets.

1. For all y we have X(x, y) = inf_{n∈I} sup_{k≥n} X(x_{k}, y) = X(x′, y), so X(x, x′) = X(x′, x′) = 0 and X(x′, x) = X(x, x) = 0.

2. Proved in [BvBR98].

3. Uniqueness follows from (1), using the fact that if X̂(M, N) = 0 then for all x we have N(x) ≤ M(x). For existence, let (M_{i})_{i∈I} be a Cauchy net of left modules: so for every ε > 0 we can find l such that for all n ≥ m ≥ l and all x we have M_{n}(x) ˙−M_{m}(x) ≤ ε, i.e. M_{n}(x) ≤ M_{m}(x) + ε. We first show that for each x, the net (M_{n}(x)) is Cauchy with respect to the usual metric on [0, ∞], and hence convergent (so its limsup and liminf are equal). Given ε > 0, choose k such that for all n ≥ m ≥ k and for all y we have M_{n}(y) ≤ M_{m}(y)+ε/2. Let u = inf_{n≥k} M_{n}(x) and choose l ≥ k such that M_{l}(x) < u+ε/2. Then for all n ≥ l we have u ≤ M_{n}(x) ≤ M_{l}(x) + ε/2 < u + ε. It follows that for all m, n ≥ l we have |M_{m}(x) − M_{n}(x)| ≤ ε.

Let us define M as stated. It is clearly a left module; we must show that it is the limit of the net (M_{i}). Let N be another left module: we require X̂(M, N) = inf_{n∈I} sup_{k≥n} X̂(M_{k}, N). Notice that while the Cauchy property (with respect to the distance function) for the net (M_{i}) is uniform over x, that for the net (M_{i}(x)) is not: we have

∀ε.∃k.∀x.∀n ≥ m ≥ k. M_{n}(x) ≤ M_{m}(x) + ε
∀x.∀ε.∃k.∀n, m ≥ k. |M_{n}(x) − M_{m}(x)| ≤ ε

From the first of these we deduce

∀ε.∃n.∀k ≥ n.∀x. M(x) ≤ M_{k}(x) + ε
∀ε.∃n.∀k ≥ n.∀x. N(x) ≤ M_{k}(x) + N(x) − M(x) + ε
∀ε.∃n.∀k ≥ n.∀x. N(x) ˙−M_{k}(x) ≤ X̂(M, N) + ε
∀ε. inf_{n∈I} sup_{k≥n} X̂(M_{k}, N) ≤ X̂(M, N) + ε

From the second, and using the directedness of I,

∀n.∀x.∀ε.∃k ≥ n. M_{k}(x) ≤ M(x) + ε
∀n.∀x.∀ε.∃k ≥ n. N(x) ≤ M(x) + N(x) − M_{k}(x) + ε
∀n.∀x.∀ε. N(x) ˙−M(x) ≤ sup_{k≥n} X̂(M_{k}, N) + ε
∀n.∀x. N(x) ˙−M(x) ≤ sup_{k≥n} X̂(M_{k}, N)

X̂(M, N) ≤ inf_{n∈I} sup_{k≥n} X̂(M_{k}, N)

7.15. Theorem. (Classically) Let X be a gms. Then the set of points of \overline{X} is the least subset of X̂ that contains all the representables and is complete in X̂.

Proof. First we show that every flat left module M is the limit of a Cauchy net of representables. Let I be the set of formal balls in M, in other words I = {B_{ε}(x) ∈ X×Q_{+} | M(x) < ε}. This is directed by the partial order B_{δ}(x) ≤ B_{ε}(y) iff X(x, y) + ε ≤ δ, a non-strict version of ⊃, and gives a net (x_{i})_{i∈I} for which if i = B_{δ}(x) then x_{i} = x. We show that M = lim_{i} X(−, x_{i}), in other words for every left module N, and using a result from [BvBR98],

X̂(M, N) = lim_{i} X̂(X(−, x_{i}), N) = lim_{i} N(x_{i})

To show ≥, suppose ε > 0 and choose y such that M(y) < ε so B_{ε}(y) ∈ I. If B_{ε}(y) ≤ B_{δ}(x) ∈ I then

N(x) ≤ N(x) − M(x) + δ ≤ X̂(M, N) + ε

and so

lim_{i} N(x_{i}) ≤ sup{N(x_{i}) | B_{ε}(y) ≤ i ∈ I} ≤ X̂(M, N) + ε

For ≤, suppose M(x) < α and M(y) < β, and let B_{δ}(z) be an upper bound for B_{α}(x) and B_{β}(y) in I. Then

N(x) ≤ X(x, z) + N(z) ≤ α + sup{N(x_{i}) | B_{β}(y) ≤ i ∈ I}

It follows that

∀x ∈ X.∀j ∈ I. N(x) ≤ M(x) + sup_{i≥j} N(x_{i})

and hence X̂(M, N) ≤ lim_{i} N(x_{i}).

Next we show that if (M_{i})_{i∈I} is any net of flat left modules then its limit M is also flat.

If ε > 0, then we can find n such that for all x we have M(x) ≤ M_{n}(x) + ε/2. Using flatness to choose y such that M_{n}(y) < ε/2 we get M(y) < ε and so inf_{x} M(x) = 0.

Now suppose M(x_{λ}) < α_{λ} (λ = 1, 2), and choose α′_{λ} such that M(x_{λ}) < α′_{λ} < α_{λ}. Let ε = min_{λ}(α_{λ} − α′_{λ}). We can find n such that for all m ≥ n and for all x we have M(x) ≤ M_{m}(x)+ε/2; and in addition for all m ≥ n and for λ = 1, 2, M_{m}(x_{λ}) < α′_{λ} +ε/2. Choose z such that X(x_{λ}, z) + M_{n}(z) < α_{λ} + ε/2. Then X(x_{λ}, z) + M(z) ≤ X(x_{λ}, z) + M_{n}(z) + ε/2 < α_{λ}. It follows that M is flat.

The following definition is simply a net version of the corresponding sequential definition in [BvBR98].

7.16. Definition. Let X be a gms. A subset U of X is generalized Scott open (gS-open) iff for every Cauchy net (x_{i})_{i∈I} in X with limit x in U we have some n and some ε > 0 such that for every m ≥ n and for every y with X(x_{m}, y) < ε we have y ∈ U.

We next show that our topology on \overline{X} is the netwise generalized Scott topology.

7.17. Proposition. Let X be a gms and U a subset of \overline{X}. Then U is gS-open for \overline{X} iff it is a union of open balls B_{δ}(x) (x ∈ X).

Proof. ⇐: It suffices to show the open balls are gS-open. Suppose M ∈ B_{δ}(x), i.e. M(x) < δ, and let (M_{i})_{i∈I} be a Cauchy net converging on M. We can find δ′ such that M(x) < δ′ < δ, and then n such that for all m ≥ n we have M_{m}(x) < δ′. Let ε = δ − δ′. If \overline{X}(M_{m}, N) < ε then N(x) < M_{m}(x) + ε < δ, so N ∈ B_{δ}(x).

⇒: Suppose U is gS-open and M ∈ U. As in Theorem 7.15, M is a limit of a Cauchy net of representables X(−, x_{i}) for i ∈ I = {(δ, x) | M(x) < δ}. There is some n ∈ I and some ε > 0 such that for every m ≥ n and for every N with N(x_{m}) = \overline{X}(X(−, x_{m}), N) < ε we have N ∈ U: in other words, for m ≥ n the open ball B_{ε}(x_{m}) is a subset of U. Choosing m = (δ, x) ∈ I such that δ < ε, we have M ∈ B_{ε}(x_{m}).

8. Conclusions

Given a gms X, we have constructed a completion \overline{X} whose points are Cauchy filters of formal balls. Even for ordinary metric spaces this has the virtue of providing canonical representations for the points, instead of using sequences modulo an equivalence. For quasimetric spaces our completion provides a direct characterization of the points of the netwise Yoneda completion.

We have tried to present the main narrative line in terms that can be understood by mainstream mathematicians, but that naive understanding converts readily to a constructive localic account and one might see that as a bonus for those readers who are interested in such things. Historically, however, that view is back to front.

The work arose out of efforts to describe completion within the constraints of geometric reasoning [Vic99], [Vic04]. These constraints are very severe, and in practice lead to reasoning that is both choice-free and predicative. Many set constructions that one normally takes for granted (such as function sets and powersets) are not available geometrically as sets, and have to be constructed as locales; and even so, the corresponding frames have to be presented using sets (in the geometrically restricted sense) of generators and or relations. From this point of view it is an achievement to find any account of completion at all, and a miracle for it to be a reasonably simple one in ordinary mathematics. In the asymmetric case, the construction by Cauchy filters stands up well in comparison with the constructions by Cauchy sequences or nets. We might take this as a vindication of the geometric approach.

These constructive localic aspects are still unfinished in that so far we have not been able to characterize the completion as a “complete gms”. This is because of the different natures of the original space and the localic completion. The original space is considered to have its discrete topology and to try to construct its gms topology would not be geometric (stable under change of base). On the other hand the topologized structure, the completion \overline{X}, does not in the asymmetric case have its own distance function, at least not in the obvious sense of a map from \overline{X} × \overline{X} to a space of reals.

The situation is analogous to that of ideal completion of a poset. The poset is carried by a discrete locale (the underlying set of the poset), but its ideal completion is an algebraic dcpo, a non-discrete locale. Without a notion of “partially ordered locales” it is not possible to say that ideal completion has taken an incomplete partially ordered locale (but a discrete locale) and constructed a complete one.

Nonetheless, we propose the locale \overline{X} (rather than its set of points) as a fruitful localic notion of completion of a gms. The difference is seen most clearly in non-classical mathematics, even in the paradigm example of ℝ as completion of ℚ. Constructively, the localic form of ℝ as we defined it is not spatial but is often better behaved than its spatialization. For example, the Heine-Borel Theorem is true for the localic ℝ but not for its spatialization. This is discussed in [Vic03], where we use the point-based techniques to give a constructive proof of the Heine-Borel theorem. Of course, this relies crucially on the idea that “point” means generalized point.

Thus the paper has constituted another case study in the use of geometric reasoning – locales as “topology-free spaces”. This has made it possible to treat locales in an entirely spatial way that often conceals not only the frame (the lattice of opens) but even any explicit consideration of the topology.

We have used Lawvere’s approach to generalized metric spaces using enriched category theory. However, we have enriched over a locale \overleftarrow{[0, ∞]} instead of a poset ([0, ∞], ≥). A curious problem that in the end seemed not to matter is that there is no obvious way localically to say that \overleftarrow{[0, ∞]} is monoidal closed – the internal hom (truncated minus) is not continuous.

Many questions are left unanswered here. Some that perhaps merit further work are:

• Can gms completions be given distance functions of their own in any sense? (The obvious sense – of a continuous map from \overline{X}^{2} to \overleftarrow{[0, ∞]} – is plainly not possible in general, for it would have to be contravariant in one argument with respect to the specialization order.) One approach that looks promising is to define a distance function on a locale X by using a map from X to P_{L}(X × \overleftarrow{[0, ∞]}), conceptually mapping y to {(x, δ) : X(x, y) ≤ δ}. This has the right variances.

• What special properties are enjoyed by Dedekind gms’s, for which the metric factors via [0, ∞] (on its way to \overleftarrow{[0, ∞]})?

• How does the theory appear when restricted to generalized ultrametrics? These can also be treated as enriched categories in a different way, enriched over \overleftarrow{[0, ∞]} with max for its monoidal product instead of addition. Are the points of the completion still flat modules in the new setting?

• How can arbitrary maps between gms completions be expressed in terms of the original gms’s?

• Can one give criteria on the gms’s for their completions to have various properties – for instance, Hausdorff, stably locally compact, locally compact?

References

[BvBR98] M.M. Bonsangue, F. van Breugel, and J.J.M.M. Rutten, Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding, Theoret. Comput. Sci. 193 (1998), 1–51.

[CSSV03] T. Coquand, G. Sambin, J. Smith, and S. Valentini, Inductively generated formal topologies, Annals of Pure and Applied Logic 124 (2003), 71–106.

[Joh82] P.T. Johnstone, Stone spaces, Cambridge Studies in Advanced Mathematics, no. 3, Cambridge University Press, 1982.

[Joh89] P.T. Johnstone, A constructive ‘closed subgroup’ theorem for localic groups and groupoids, Cahiers Topologie Géom. Differentielle Catégoriques 30 (1989), 3– 23.

[JT84] A. Joyal and M. Tierney, An extension of the Galois theory of Grothendieck, Memoirs of the American Mathematical Society 309 (1984).

[KS02] H.P. Künzi and M.P. Schellekens, On the Yoneda completion of a quasi-metric space, Theoretical Computer Science 278 (2002), 159–194.

[Law73] F.W. Lawvere, Metric spaces, generalised logic, and closed categories, Rend. del Sem. Mat. e Fis. di Milano 43 (1973), reissued as [Law02].

[Law02] F.W. Lawvere, Metric spaces, generalised logic, and closed categories, Reprints in Theory and Applications of Categories 1 (2002), 1–37, originally published as [Law73].

[MLM92] S. Mac Lane and I. Moerdijk, Sheaves in geometry and logic, Springer-Verlag, 1992.

[MP91] C.J. Mulvey and J. Wick-Pelletier, A globalization of the Hahn-Banach theorem, Advances in Mathematics 89 (1991), 1–59.

[Sam87] G. Sambin, Intuitionistic formal spaces – a first communication, Mathematical Logic and its Applications (Dimiter G. Skordev, ed.), Plenum, 1987, pp. 187– 204.

[Smy91] M. Smyth, Totally bounded spaces and compact ordered spaces as domains of computation, Topology and Category Theory in Computer Science (G.M. Reed, A.W. Roscoe, and R.F. Wachter, eds.), Oxford University Press, 1991, pp. 207– 229.

[Vic89] S. Vickers, Topology via logic, Cambridge University Press, 1989.

[Vic93] S. Vickers, Information systems for continuous posets, Theoretical Computer Science 114 (1993), 201–229.

[Vic98] S. Vickers, Localic completion of quasimetric spaces, Tech. Report DoC 97/2, Department of Computing, Imperial College, London, 1998.

[Vic99] S. Vickers, Topical categories of domains, Mathematical Structures in Computer Science 9 (1999), 569–616.

[Vic03] S. Vickers, Localic completion of generalized metric spaces II: Powerlocales,

         draft available on web at http://www.cs.bham.ac.uk/~sjv, 2003.

[Vic04] S. Vickers, The double powerlocale and exponentiation: A case study in geometric reasoning, Theory and Applications of Categories 12 (2004), 372–422.

School of Computer Science, University of Birmingham, Birmingham, B15 2TT, UK.

Email: s.j.vickers@cs.bham.ac.uk

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/14/15/14-15.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX 2ε is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@mathstat.uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca