A few months ago, Keye Martin drew my attention to his results on so-called ideal models of spaces [1]. Ideal domains are incredibly specific dcpos: they are defined as dcpos where each non-finite element is maximal. Despite this, Keye Martin was able to show that: (1) every space that has an ω-continuous model has an ideal model, that is, a model that is an ideal domain; (2) the metrizable spaces that have an ideal model are exactly the completely metrizable spaces.

I will try to expose a few of his ideas here. I will probably betray him a lot. For example, I will not talk about measurements (one of Keye’s inventions), and I will not stress the role of Choquet-completeness to go beyond “Lawson at the top” domains, or the role of *G*_{δ} subsets so much. I have also tried to extend whatever I can to the case of quasi-metric, not just metric, spaces… unfortunately, I failed to achieve this.

## A basic example

The prime example of an ideal domain is the infinite binary tree. Take finite and infinite words over the two-letter alphabet {0, 1}, and order them by prefix. So the empty word is the least element, and is below, say, 0, which is below 01, which is below 011, and so on. In that dcpo, the finite elements are the finite words, and the maximal elements are the infinite words. This is an ideal domain.

## Ideal ⟹ algebraic

In general, ideal domains have plenty of properties.

For one, they are all *algebraic dcpos*.

For that, we show that every element *x* is the supremum of a directed family of finite elements. If *x* is itself finite, this is clear. Otherwise, by the definition of “finite”, and since *x* is not finite, there must be a directed family (*x _{i}*)

_{i}_{ in }

*of elements whose supremum is above*

_{I}*x*, and such that no

*x*is above

_{i}*x*. Since we are in an ideal domain,

*x*is maximal, so the supremum is equal to

*x*. Since no

*x*is equal to

_{i}*x*, none is maximal, so they are all finite, and we are done.

## Ideal ⟹ first-countable

An ideal domain is not just algebraic: every element is the supremum of a *countable chain* of finite elements.

Consider any point *x* in the chosen ideal domain. If *x* is finite, then we can take the constant chain whose elements are all equal to *x*.

Otherwise, let *D* be a directed family of finite elements whose supremum is *x*. Pick one element *x*_{1} from *D*. Since *x*_{1} is finite and *x* is not, there is a strictly larger element in *D*, call it *x*_{2} in *D*, and then an even strictly larger element *x*_{3}, etc. The sequence of elements *x _{n}*,

*n*∈

**N**, has a supremum

*x*‘, and

*x*‘ cannot be finite, since otherwise

*x*‘ would be below some

*x*, contradicting the fact that the sequence is strictly increasing. Hence

_{n}*x*‘ is maximal, and since it is clearly below

*x*, it coincides with it.

It follows that an ideal domain is *first-countable*: every point has a countable basis of open neighborhoods. Indeed, for every point *x*, write *x* as the supremum of a countable chain *x _{n}*,

*n*∈

**N**: the open subsets ↑

*x*form the desired basis of open neighborhoods of

_{n}*x*.

In this post, I will not make use of first-countability. But remember that for next time!

## Constructing an ideal domain of formal balls

First note that if *X*, *d* is a metric space, then its space of formal balls **B**(*X*) is not an ideal domain, and in fact is not even algebraic (unless *X* is empty): if (*x*, *r*) were finite in **B**(*X*), since it is the supremum of the chain of formal balls (*x*, *r*+ε), ε>0, it would be equal to one of them, which is absurd.

Keye Martin has a general construction for building an ideal domain from *G*_{δ} subsets of a continuous dcpo. I said I would betray him, and I will now. Instead of showing you the general construction, let me show you how he would build an ideal domain for a complete metric space *X*, by changing the ordering on its space of formal balls **B**(*X*).

Every complete metric space is in particular Smyth-complete, in particular continuous Yoneda-complete. What that means is that its dcpo of formal balls **B**(*X*) is a continuous dcpo (Definition 7.4.72). In that case, let **B*** _{D}*(

*X*) be just the set of formal balls on

*X*again, except with a modified ordering: (

*x*,

*r*) ⊑ (

*y*,

*s*) if and only if:

- either (
*x*,*r*) ≪ (*y*,*s*) and*r*≥ 2*s*, - or (
*x*,*r*) = (*y*,*s*).

That is, to go up, we really have to jump high (go way-above, and divide the radius by at least 2), or to stay put.

**Lemma.** For every complete metric space *X*, **B*** _{D}*(

*X*) is a dcpo, and in fact one in which directed suprema are computed exactly as in

**B**(

*X*).

*Proof.* First note that (*x*, *r*) ⊑ (*y*, *s*) implies (*x*, *r*) ≤ (*y*, *s*) (in short, we shall say that ⊑ implies ≤). In particular, every directed family in **B*** _{D}*(

*X*) is also directed in

**B**(

*X*).

Take a family (*x _{i}*,

*r*)

_{i}*in*

_{i ∈ I}**B**

*(*

_{D}*X*) that is directed with respect to ⊑, and let (

*x*,

*r*) = (

*d*-lim

*x*, inf

_{i}*r*) be its supremum in

_{i}**B**(

*X*).

If (*x _{i}*,

*r*) is the largest element of the family with respect to ⊑ (there may not even be any such largest element, but in case that happens), then it is the supremum with respect to ⊑. It is also the supremum of the family with respect to ≤, since ⊑ implies ≤, so it coincides with (

_{i}*x*,

*r*).

Otherwise, that is, if the family contains no single ⊑-largest element, we use the following trick: (*) for every element (*x _{i}*,

*r*) of the family, there is another element of the family that is not ⊑ it, and since the family is directed, there is one, (

_{i}*x*,

_{j}*r*) above those two elements; in particular, (

_{j}*x*,

_{i}*r*) ⊑ (

_{i}*x*,

_{j}*r*) and (

_{j}*x*,

_{i}*r*) ≠ (

_{i}*x*,

_{j}*r*); then, by definition, (

_{j}*x*,

_{i}*r*) ≪ (

_{i}*x*,

_{j}*r*) and

_{j}*r*≥ ½

_{i}*r*.

_{j}We use this trick to show that (*x*, *r*) is an upper bound of (*x _{i}*,

*r*)

_{i}*in*

_{i ∈ I}**B**

*(*

_{D}*X*). For every

*i ∈ I*, use (*) to find (

*x*,

_{j}*r*) such that (

_{j}*x*,

_{i}*r*) ≪ (

_{i}*x*,

_{j}*r*) and

_{j}*r*≥ ½

_{i}*r*. Since (

_{j}*x*,

_{j}*r*) ≤ (

_{j}*x*,

*r*) (in particular,

*r*≥

_{j}*r*), (

*x*,

_{i}*r*) ≪ (

_{i}*x*,

*r*) and

*r*≥ ½

_{i}*r*, whence (

*x*,

_{i}*r*) ⊑ (

_{i}*x*,

*r*).

Now consider any other upper bound (*y*, *s*) of the family with respect to ⊑. Since ⊑ implies ≤, it is also an upper bound with respect to ≤, so (*x*, *r*) ≤ (*y*, *s*). We cannot conclude much from that, except by iterating trick (*). We find (*x _{i}*,

*r*) ⊑ (

_{i}*x*,

_{j}*r*) ⊑ (

_{j}*x*,

_{k}*r*) ⊑ …, all those formal balls being different. In particular,

_{k}*r*≥ 2

_{i}*r*,

_{j}*r*≥ 2

_{j}*r*, …, and all these radii are larger than or equal to

_{k}*r*. That implies

*r*=0. From (

*x*,

*r*) ≤ (

*y*,

*s*), we can now conclude that

*d*(

*x*,

*y*) ≤

*r*–

*s*= 0. Since

*X*is metric,

*x*=

*y*. We conclude that (

*x*,

*r*)=(

*y*,

*s*), therefore (

*x*,

*r*) ⊑ (

*y*,

*s*). ☐

The only place where we use the fact that *X* is metric is in the last line. I once thought that we could prove the above lemma for all continuous Yoneda-complete *quasi-metric* spaces, but that seems to fail.

**Lemma.** For every complete metric space *X*, every formal ball (*x*, *r*) with non-zero radius *r* is finite in **B*** _{D}*(

*X*).

*Proof.* Assume a ⊑-directed family (*x _{i}*,

*r*)

_{i}*whose supremum is above (*

_{i ∈ I}*x*,

*r*) in the sense of ⊑. If the supremum is attained, say at index

*i*, then (

*x*,

*r*) ≤ (

*x*,

_{i}*r*). Otherwise, we iterate trick (*) (see previous lemma) to conclude that there is a chain of elements in the family that are strictly ordered by ⊑. Each further element in the chain has a radius twice as small or even smaller than the previous one. It follows that inf

_{i}*r*=0. Because (

_{i}*x*,

*r*) is ⊑-below the supremum of (

*x*,

_{i}*r*)

_{i}*, because*

_{i ∈ I}*r≠*0 and inf

*r*=0, some

_{i}*r*is below

_{i}*r*, and even below

*r/2*. Also, since inf

*r*=0 and

_{i}*r≠*0, (

*x*,

*r*) is strictly ⊑-below, hence way-below the supremum of (

*x*,

_{i}*r*)

_{i}*. Hence (*

_{i ∈ I}*x*,

*r*) ≪ (

*x*,

_{i}*r*) for some

_{i}*i*, and we can take the same

*i*by directedness. It follows that (

*x*,

*r*) ⊑ (

*x*,

_{i}*r*). ☐

_{i}**Lemma.** For every complete metric space *X*, no formal ball with zero radius is finite in **B*** _{D}*(

*X*).

*Proof.* We first note: (**) if a formal ball is way-below another, then they cannot have the same radius. Indeed, if (*x*, *r*) ≪ (*y*, *r*), since (*y*, *r*) is the supremum of the directed chain (*y*, *r*+ε), ε>0, we must have (*x*, *r*) ≤ (*y*, *r*+ε) for some ε>0. In particular, *r* ≥ *r*+ε, which is impossible.

Now imagine that (*x*, 0) is finite in **B*** _{D}*(

*X*). It is the sup of a directed family

*D*of formal balls way-below it, since

*X*is complete metric, hence continuous Yoneda-complete. By (**) none of those formal balls can have zero radius. We shall build a new family of formal balls (

*x*,

_{I}*r*), where

_{I}*I*ranges over the finite subsets of

*D*. Each will be an element of

*D*, and will be above every element of

*I*in the ⊑ ordering. It will also be above (

*x*,

_{J}*r*) in the ⊑ ordering, for every proper subset

_{J}*J*of

*I*, ensuring that the family of formal balls (

*x*,

_{I}*r*) is directed with respect to ⊑. Clearly, its supremum will be (

_{I}*x*, 0), and if the latter is finite, then (

*x*, 0) ⊑ (

*x*,

_{I}*r*) for some finite set

_{I}*I*. But that is impossible, since

*r*≠0.

_{I}Let us construct (*x _{I}*,

*r*), by induction on the cardinality of

_{I}*I*. This is a classical construction. When

*I*is empty, we pick any element of

*D*for (

*x*,

_{I}*r*). Otherwise, we consider the (finite) intersection

_{I}*U*of the sets ↟(

*y*,

*s*) for (

*y*,

*s*) in

*I*, and of ↟(

*x*,

_{J}*r*), for all proper subsets

_{J}*J*of

*I*. This is a Scott-open neighborhood of (

*x*, 0), since

*X*is continuous Yoneda-complete.

*U*therefore contains an element (

*z*,

*t*) in

*D*; the infimum of the radii of the elements of

*D*is equal to 0, so there is also an element of

*D*with radius less than or equal to

*s*/2 for all (

*y*,

*s*) in

*I*and less than or equal to

*r*for every proper subset

_{J}*J*of

*I*. By directedness, we can assume that (

*z*,

*t*) has all those properties: it follows that (

*z*,

*t*) is an element of

*D*above every element of

*I*and above every (

*x*,

_{J}*r*) with respect to ⊑, as we had announced. ☐

_{J}When *X* is a metric space, the formal balls of radius 0 are maximal in **B**(*X*), hence also in **B*** _{D}*(

*X*). We have therefore obtained:

**Proposition.** For every complete metric space *X*, **B*** _{D}*(

*X*) is an ideal domain whose subset of maximal elements coincides with the set of formal balls of radius 0.

The latter formal balls are in bijection with *X* itself.

## Ideal models of complete metric spaces.

If we equate *X* with the set of formal balls of radius 0, then the subspace topology on *X*, induced by the Scott topology on **B**(*X*), is called the *d*-Scott topology (Definition 7.4.43 in the book). For a metric space, this coincides with the open ball topology. We do not need that to show:

**Theorem.** Let *X*, *d* be a complete metric space. Then *X*, with the *d*-Scott topology, is homeomorphic to the subspace of limit elements of the ideal domain **B*** _{D}*(

*X*).

*Proof.* We have already established the bijection with the subset of limit elements. We equate the latter, namely formal balls with radius 0, with their centers in *X*. Therefore *X* is included in both **B**(*X*) and **B*** _{D}*(

*X*). Let us call, temporarily, the

*D*-Scott topology the topology induced by the latter inclusion.

An open subset *U* of *X* in the *d*-Scott topology is the intersection of *X* with a Scott-open subset *V* of **B**(*X*). Since ⊑ implies ≤, and since directed suprema are computed in **B*** _{D}*(

*X*) as in

**B**(

*X*),

*V*is Scott-open in

**B**

*(*

_{D}*X*), hence

*U*is

*D*-Scott open.

Conversely, let *U* be a *D*-Scott open subset of *X*. For every *x* in *U*, there is a formal ball (*y*, *r*) ⊑ (*x*, 0) with *r*≠0 such that every formal ball (*z*, *0*) such that (*y*, *r*) ⊑ (*z*, 0) is in *U*. Since *r*≠0, (*y*, *r*) ≪ (*x*, 0). For every element *e* such that (*y*, *r*) ≪ (*z*, 0), we plainly observe that (*y*, *r*) ⊑ (*z*, 0), so (*z*, 0) is in *U*. It follows that the intersection of *X* with ↟(*y*, *r*) contains (*x*, 0) and is included in *U*, showing that *U* is *d*-Scott-open. ☐

In particular, we obtain one of Keye Martin’s theorems:

**Theorem (Martin [1]).** When *X*, *d* is a complete metric space, **B*** _{D}*(

*X*) is an ideal model of

*X*, namely an ideal domain whose subspace of maximal elements is homeomorphic to

*X*with its open ball topology.

Indeed, recall that the latter coincides with the *d*-Scott topology when *X* is metric—Proposition 7.4.46—, or when it is Smyth-complete—Proposition 7.4.47. ☐

Next time, we shall study ideal domains. Keye has a complicated (but clever) argument that the subset *X* of maximal elements of an ideal domain *Y* is a *G*_{δ} subset of *Y*. I’ve just found an alternate, simpler argument of a weaker result that there is another ideal domain *Y*‘ whose subset of maximal elements is again *X*, and such that *X* is a *G*_{δ} subset of *Y*‘. I hope that argument is correct. With all that, we shall be able to obtain one of Keye’s results:

**Theorem (Martin [1]).** The metrizable spaces that have an ideal model are exactly the completely metrizable spaces.

Proof. We have already seen how to build an ideal model of a completely metrizable space. Conversely, if *X* is metrizable, and embeds as the space of maximal elements of an ideal domain *Y*, then (changing the latter if necessary, although Keye shows that it is not necessary), *X* is a *G*_{δ} subset of *Y*. Since *Y* is in particular a continuous dcpo, its subspace of maximal elements *X* is also Choquet-complete (see Proposition 7.7.19 in the book; that is due to Keye Martin as well). But a Choquet-complete metrizable space is completely metrizable (Corollary 7.6.16 in the book). ☐

I love those arguments that mix Choquet game theory with domain theory. Keye Martin was the person who imagined such arguments, and put them to good use. They are truly fantastic.

— Jean Goubault-Larrecq (October 25th, 2015)

- Keye Martin. Ideal models of spaces. Theoretical Computer Science, Volume 305, Issues 1–3, 18 August 2003, Pages 277–297.