Bounded-complete domains (bc-domains) are an incredibly useful form of continuous dcpos. I have just again mentioned them in a recent talk at LICS 2019, and Prakash Panangaden aptly, and wittily, described them as “bloody convenient domains”. In 1997, Yuri Ershov showed that every C-space can be embedded into a (weakly) universal bc-domain, which he called its bc-hull [1]. The construction is rather elaborate, but I claim that it can be made considerably simpler if we consider coherent continuous dcpos instead of general C-spaces. I will also briefly show why the case of algebraic, not necessarily coherent, dcpos, is simple as well, and I will say a word on the general continuous case, without delving into details.
Bc-hulls and Clat-hulls
Let me recall that a bc-domain (see Section 5.7 in the book) is a pointed, continuous dcpo in which every pair of elements with an upper bound has a least upper bound; or equivalently, a continuous dcpo in which every family of elements with an upper bound has a least upper bound; or equivalently, a non-empty continuous dcpo in which every non-empty family has a greatest lower bound. Every bc-domain is stably compact in its Scott topology. And the category of bc-domains is Cartesian-closed. And the bc-domains are exactly the densely injective topological spaces. That is all very nice.
I will also mention their close cousins: continuous complete lattices. (Allow me to call them continuous lattices, for short.) Every continuous lattice is a bc-domain, and conversely, every bc-domain with a top element is a continuous lattice. Continuous lattices also form a Cartesian-closed category, and they are exactly the injective topological spaces.
Not all continuous dcpos are bc-domains. For example, build a dcpo whose elements are the negative integers –n with their usual ordering (so that 0 is above –1, which is above –2, etc.), all above two incomparable elements a and b, and the latter two being above a bottom element ⊥:
This is a continuous (even algebraic) dcpo, a and b have an upper bound, but no least upper bound.
A natural question is then: given a continuous dcpo X, can we embed X into a bc-domain bc(X)? (respect., a continuous lattice clat(X)?) This is of course true, and in fact one can embed any T0 topological space X into a continuous lattice: just take the powerset of OX with the inclusion ordering, and take the map that sends every point x of X to its set of open neighborhoods. (That construction is originally due to Dana S. Scott.)
But can we ask for more? For example, is there a free bc-domain (resp., continuous lattice) on any given continuous dcpo?
That is too much to ask, as we will see below. In 1997, Yuri Ershov [1] came up with the following funny, intermediate notion: a bc-hull of a continuous dcpo X is a bc-domain bc(X) with an embedding η : X → bc(X) such that:
- for every continuous map f : X → Y where Y is a bc-domain, one can find an extension f* : bc(X) → Y, where by extension I mean that f* o η = f — but note that we do not require the extension to be unique;
- the following weak universality property holds: the only continuous map g : bc(X) → bc(X) such that g o η = η is the identity map.
For example, the bc-hull of the algebraic dcpo we have above as an example of one that is not a bc-domain is the following dcpo, where we have just added a fresh least upper bound to a and b. (This can be checked by using the forthcoming construction.)
We will see later that bc(X) cannot be a free bc-domain on X, for general X, precisely because extensions f* cannot be required to be unique. However, we can salvage a few things. For one, weak universality implies that η* is the identity map on bc(X). It also implies that the bc-hull of a continuous dcpo is unique up to isomorphism (if it exists)—a property that we are accustomed to see satisfied with free objects, but freeness is not required for that.
Indeed, imagine we had two bc-hulls bc(X) and bc'(X) of X, with respective embeddings η and η’. The map η’ extends to a map η’* : bc(X) → bc'(X), i.e., η’* o η = η’, and symmetrically η extends to η† : bc'(X) → bc(X) (I am using † instead of * to avoid any confusion), meaning that η† o η’ = η. This implies that η’* o η† o η’ = η’ and η† o η’* o η = η, so by weak universality η’* o η† and η† o η’* are identity maps, showing that η† and η’* form an isomorphism.
Ershov has shown [1] that the bc-hull of a continuous dcpo, and more generally of a C-space, always exists. I’ll say a word on his proof later, but the final construction is complicated. My goal is to show that bc(X) can be constructed in a fairly simple manner, provided X is a coherent continuous dcpo.
I will also show that the continuous lattice hull clat(X) of X always exists, too, where clat(X) is defined exactly as bc(X), replacing “bc-domain” by “continuous lattice” everywhere. Of course, if a continuous lattice hull exists, it is unique by weak universality again.
Building bc(X) and clat(X)
Let us fix a coherent, continuous dcpo X. By coherent, I mean that the intersection of two compact saturated sets is compact saturated.
Note that since X is a continuous dcpo, it is sober, hence well-filtered. Since the intersection of a non-empty family of compact saturated subsets of X can be written as a filtered intersection of non-empty finite intersections, and since the latter are compact saturated by coherence, every non-empty intersection of compact saturated sets is compact saturated. Indeed, recall that in a well-filtered space, every filtered intersection of compact saturated sets is compact saturated (Proposition 8.3.6 of the book).
We define clat(X) as the set of all intersections of principal filters ↑x, where x ranges over arbitrary subsets E of X. The idea is that we want to add the least upper bounds of every subset E to X. If the least upper bound of E already exists, then it is a point y such that ↑y is equal to the intersection of all ↑x, x in E. Otherwise, that intersection will serve to represent the supremum of E that we must add to X.
Every principal filter is compact saturated, and every non-empty intersection of compact saturated subsets is again compact saturated, so all the elements of clat(X) are compact saturated, except possibly for the intersection of the empty family, namely X itself.
We order clat(X) by reverse inclusion. Every intersection of a family of elements of clat(X) is obviously in clat(X), and coincides with the supremum of the family. It follows that clat(X) is a complete lattice.
We also define bc(X) as the subset of clat(X) obtained by removing the empty set. Every family that is bounded from above in bc(X), say by Q, consists of elements of bc(X) which all contain Q, hence their intersection also contains Q, and is in particular non-empty. Therefore, in bc(X), every upper bounded family has a least upper bound: bc(X) is bounded-complete.
bc(X) and clat(X) are dcpos
It is also true that bc(X) is a dcpo, with directed suprema computed as filtered intersections. (clat(X) is vacuously a dcpo, since it is a complete lattice.) For that, we use the following observation:
(*) For every filtered family (Qi)i ∈ I in clat(X) (resp., in bc(X)), for every open subset U of X that contains the intersection ∩i ∈ I Qi, some Qi is included in U.
We have already seen that this holds if every Qi is compact saturated. (Recall that every Qi is compact saturated or equal to the whole of X.) If some Qi is different from X, then removing X from the family (Qi)i ∈ I still yields a directed family, with the same intersection, and this allows us to conclude. Otherwise, every Qi is equal to X, so U=X, and the claim is clear.
Using (*) with the empty set for U, we observe that the intersection of a filtered family of non-empty compact saturated sets must be non-empty, so that filtered intersections of elements of bc(X) are again in bc(X). It follows that those filtered intersections are exactly the required directed suprema.
bc(X) and clat(X) are continuous
In order to show that bc(X) is a bc-domain and that clat(X) is a continuous lattice, it remains to show that clat(X) and bc(X) are continuous.
Let me use the following abbreviation: for every subset E of X, let E↑ denote the set of all upper bounds of E. Equivalent, E↑ is the intersection of the sets ↑x, x ∈ E, and is therefore an element of clat(X) (and of bc(X) if non-empty).
I will need the following auxiliary lemma:
(**) For every E↑ in clat(X), for every open subset U of X, if E↑ ⊆ U then there are finitely many pairs of elements y1≪x1, …, yn≪xn such that x1, …, xn are in E, and {y1, …, yn}↑ is included in U.
This is proved as follows. First, we apply (*) to the family of subsets {x1, …, xn}↑ with x1, …, xn in E (the intersection of that family is E↑, which is included in U). Therefore {x1, …, xn}↑ is included in U for some finite family of elements x1, …, xn of E. Since X is a continuous dcpo, we can write each xi as a directed supremum sup ↡xi. Then ↑xi=∩ {↑y | y≪xi}, and hence {x1, …, xn}↑ = ∩i=1n ↑xi = ∩ {{y1, …, yn}↑ | y1≪x1, …, yn≪xn}. The latter intersection is again directed (note that n is fixed), as one easily checks. By (*) again, it follows that {y1, …, yn}↑ is included in U for some y1≪x1, …, yn≪xn.
Now that we have proved (**), we also observe the following:
(***) Every set E↑ in clat(X) is the filtered intersection of the sets {y1, …, yn}↑, where y1≪x1, …, yn≪xn and x1, …, xn are in E.
For a proof, first, I will let you check that the family of those sets {y1, …, yn}↑, is indeed filtered. We then prove the double inclusion between E↑ and the filtered intersection given in (***). In one direction, E↑ is certainly included in any set {y1, …, yn}↑ as given in (***), because every element of E↑ is above every element of E, hence above every xi, hence above every yi. In the converse direction, for every open neighborhood U of E↑, we use (*) and obtain finitely many pairs of elements y1≪x1, …, yn≪xn such that x1, …, xn are in E, and such that {y1, …, yn}↑ is included in U. This shows that U also contains the intersection of the sets {y1, …, yn}↑ as given in (***). Since E↑ is saturated, it is the intersection of its open neighborhoods U, and therefore E↑ itself contains the intersection of the sets {y1, …, yn}↑ as given in (***).
With (*), (**), and (***), we can now show that, in clat(X) or in bc(X), Q ≪ Q’ if and only if one can find finitely many pairs of elements y1≪x1, …, yn≪xn such that Q contains {y1, …, yn}↑ and {x1, …, xn}↑ contains Q’.
- If. Q‘ is included in {x1, …, xn}↑ = ∩j=1n ↑xj ⊆ ∩j=1n ↟yj , and the latter is an open subset of X. For every directed family (Qi)i ∈ I in clat(X) (or bc(X)) whose supremum ∩i ∈ I Qi is above (included in) Q’, we must have ∩i ∈ I Qi ⊆ ∩j=1n ↟yj. By (*), in particular, Qi ⊆ ∩j=1n ↟yj for some i in I. Then Qi is also included in ∩j=1n ↑yj = {y1, …, yn}↑ ⊆ Q. Therefore Q ≪ Q’.
- Only if. We assume Q ≪ Q’. We can write Q’ as E↑ for some set E. By (***), Q’ is the filtered intersection (=directed supremum) of the sets {y1, …, yn}↑, where y1≪x1, …, yn≪xn and x1, …, xn are in E. Hence one of them is contained in Q, and {x1, …, xn}↑ contains Q’ because every xi is in E.
Finally, we use (***) once again: every set E↑ in clat(X) is the filtered intersection (=directed supremum) of the sets {y1, …, yn}↑, where y1≪x1, …, yn≪xn and x1, …, xn are in E. In particular, each such {y1, …, yn}↑ is way-below E↑ (take Q={y1, …, yn}↑.)
This shows that clat(X) is continuous, and the case of bc(X) is similar.
Summarizing: clat(X) is a continuous, complete lattice, and bc(X) is a continuous, bounded-complete dcpo, namely, a bc-domain.
The upper Vietoris topology
Let us open a quick parenthesis.
Since bc(X) and clat(X) are sub-posets of the Smyth powerdomain Q(X) (which consists of all compact saturated subsets of X, including the empty set, contrarily to the convention I took in Proposition 8.3.25 of the book), and there is another natural topology on Q(X) called the upper Vietoris topology, we may inquire whether the Scott topology coincides with the (subspace topology of) the upper Vietoris topology on bc(X) and clat(X). The answer is positive:
Fact. For every coherent continuous dcpo, the Scott topology on bc(X) and clat(X) coincides with the upper Vietoris topology, namely the topology with a base of open subsets of the form ☐U, U open in X, and where ☐U denotes the set of elements Q of bc(X) (resp., clat(X)) that are included in U.
Proof. ☐U is always Scott-open, using (*). In the converse direction, let W be a Scott-open subset of bc(X) (resp., clat(X)), and Q be an element of W. We will show that there is an open subset U of X such that Q ∈ ☐U ⊆ W. Using (***), and writing Q as E↑, Q is the filtered intersection of the sets {y1, …, yn}↑, where y1≪x1, …, yn≪xn and x1, …, xn are in E. Since W is Scott-open, one of them is in W. We let U be ∩i=1n ↟yi. Every element x of Q is above every element of E, in particular above every xi, in particular in every ↟yi, hence in U, so Q ∈ ☐U. Next, consider any element Q’ of ☐U. Then Q’ ⊆ ∩i=1n ↟yi ⊆ {y1, …, yn}↑, and since {y1, …, yn}↑ is in W, so is Q’. It follows that ☐U ⊆ W. ☐
One should note, however, that Q(X) is usually much bigger than bc(X) and clat(X) (when X is compact, otherwise note that X is in bc(X) and in clat(X), but not in Q(X)). If you define X as the set of natural numbers plus an element ⊥, with ≤ defined so that ⊥ is below all natural numbers and all natural numbers are pairwise incomparable, then X is already a bc-domain, so bc(X) is isomorphic to X. (clat(X) is isomorphic to X plus one fresh top element.) But Q(X) consists of a bottom element X, plus all finite subsets of the natural numbers.
Extensions
Let now f be a Scott-continuous map from the coherent continuous dcpo X to some bc-domain Y.
We define its extension f* as mapping every Q in bc(X) to:
inf {f(x) | x ∈ Q}.
Note that this is the infimum of a non-empty family, so that exists, since Y is a bc-domain. The same construction works in order to define the extension f* on clat(X) instead of bc(X), and where Y is a continuous lattice instead of a bc-domain: in that case, we need to agree that inf ∅ is the top element of Y instead.
We claim that the map f* is Scott-continuous. It is monotonic, and it remains to show that for every directed family (Qi)i ∈ I in clat(X), f*(∩i ∈ I Qi ) ≤ supi ∈ I f*(Qi). (The converse inequality follows immediately from monotonicity.) In order to do so, let y be any element way-below f*(∩i ∈ I Qi ) in Y. Let us abbreviate ∩i ∈ I Qi as Q, too. For every element x of Q, y≪f*(Q)≤f(x), so x is in the open set f-1(↟y). Therefore Q ⊆ f-1(↟y). By (*), some Qi is included in f-1(↟y). Then, for every element x of Qi, y≪f(x), in particular y≤f(x). Since x is an arbitrary element of Qi, it follows that y≤f*(Qi). Hence y≤supi ∈ I f*(Qi). Taking suprema over all y finally yields the desired inequality f*(∩i ∈ I Qi ) = sup {y | y≪f*(Q)≤f(x)} ≤ supi ∈ I f*(Qi).
This is reminiscent of Exercise 9.3.12 in the book, where it is asked to show that the bc-domains are exactly the densely injective topological spaces, and where a similar inf formula is used.
And indeed, one can use that result to give an alternate proof that f has an extension f*. For that, we need to show that X is dense in bc(X), or rather, that the image η[X] is dense in bc(X). Consider any non-empty open subset of bc(X). Since the Scott topology coincides with the upper Vietoris topology, that open subset contains a non-empty open subset of the form ☐U, U open in X. It is easy to see that ☐∅ is empty (in bc(X), not in clat(X)!), so U cannot be empty. Let x be any point in U. Then η(x) is in ☐U, so ☐U indeed intersects η[X].
We can now apply Exercise 9.3.12. Equating X with η[X], we have that Y is densely injective, so every continuous map f from X to Y extends to a continuous map from any space that contains X as a dense subspace—in particular, bc(X)—to Y.
Weak universality
We now need to show that the only continuous map g : bc(X) → bc(X) such that g o η = η is the identity map. (Similarly for maps from clat(X) to clat(X).)
Suppose that we are given such a map g. Certainly, g(↑x)=↑x for every x in X. We claim that g({x1, …, xn}↑)={x1, …, xn}↑ (where x1, …, xn are arbitrary in the case of clat(X), or are taken so that {x1, …, xn}↑ is non-empty in the case of bc(X)). Note that g is not required to preserve finite intersections, so this is not how we will proceed.
Since g is monotonic, and {x1, …, xn}↑ is included in ↑xi for every i, g({x1, …, xn}↑) must be included in g(↑xi)=↑xi for every i, hence in their intersection, which is {x1, …, xn}↑.
In the converse direction, for every x in {x1, …, xn}↑, {x1, …, xn}↑ contains ↑x, so by monotonicity again, g({x1, …, xn}↑) contains g(↑x)=↑x. This means that g({x1, …, xn}↑) contains every element x of {x1, …, xn}↑, hence it contains {x1, …, xn}↑ itself. This shows that g({x1, …, xn}↑)={x1, …, xn}↑.
In (***), we have seen that every element Q of bc(X) is the supremum of a directed family of sets of the form {x1, …, xn}↑, so the latter plus the fact that g is Scott-continuous implies that g(Q)=Q.
We are done! bc(X) is the bc-hull of X, and clat(X) is the clat-hull of X—provided X is a coherent, continuous dcpo.
There is no free bc-domain
I said earlier that there is no free bc-domain on X in general. The argument is again due to Ershov [1, Example 12]. We consider the following dcpo X:
This is a finite dcpo, hence it is in particular algebraic, and therefore continuous. It is also coherent, because every upwards-closed subset is finite hence compact.
Let us build bc(X). That contains ↑a, ↑b, ↑c, and ↑d, which we equate with a, b, c, and d respectively. The (other) non-empty pairwise intersections also include ↑c ∩ ↑d (={a,b}), which we write as c ∨ d below; and there is also the intersection of the empty family, which is the whole of X, and which we write as ⊥. We can check that those exhaust all the elements of bc(X), which therefore looks as follows:
(In addition, clat(X) has a top element above all those.)
Now let us consider the map f : X → S, where S is Sierpiński space ({0,1}, with 0<1) defined by f(a)=f(b)=1, f(c)=f(d)=0. This is the characteristic map of the Scott-open set {a,b}, hence it is Scott-continuous.
The extension f* that we have defined maps c ∨ d to inf (f(a), f(b))=1, and ⊥ to 0.
However, f has another Scott-continuous extension f’, which maps c ∨ d (and ⊥) to 0. This shows that continuous extensions are not unique. (Exercise: show that f* is the largest Scott-continuous extension of f—for every coherent continuous dcpo X.)
It follows that there is no free bc-domain on X (and no free continuous lattice on X either). Any such free bc-domain would have to satisfy the extension and weak universality properties of bc-hulls, so, up to isomorphism, the only possible candidate for a free bc-domain on X is bc(X). We have just seen that some maps had non-unique extensions. However, extensions have to be unique for any free object. Therefore bc(X) is not free, and similarly for clat(X).
What if we do not assume coherence?
Ershov actually constructed the bc-hull of any C-space. (In fact, of every c-space, which he calls α-spaces. However, since c-spaces may fail to be T0, I don’t see how you can embed them in a bc-domain. I assume he meant C-space, that is, T0 c-space.)
A C-space is almost the same thing as a continuous dcpo, in the sense that the sober C-spaces are exactly the continuous dcpos, and the most important thing is that Ershov does not require coherence.
Dealing with the non-coherent case is more complicated. Let me simplify slightly what can be. Given a C-space X, its sobrification S(X) is a continuous dcpo, and any bc-hull of S(X) must be a bc-hull of X, as I will argue right away. So we only have to consider the case of continuous dcpos.
Let me describe the argument that any bc-hull Y of S(X) must be a bc-hull of X in more detail. By definition of bc-hulls, S(X) embeds into Y through some embedding η. The mapping η0 : X → S(X) that sends x to ↓x is an embedding, since X is T0. Hence we obtain an embedding η o η0 of X into Y. Every continuous map f from X to a bc-domain Z extends to a unique continuous map f’ from S(X) to Z, because Z is sober and S(X) is the free sober space over X. Then f’ extends to some continuous map f’* from Y to Z, in the sense that f’* o (η o η0) = f. Additionally, every continuous map g from Y to Y such that g o (η o η0) = η o η0 must be such that g o η = η, because extensions of maps from X to a sober space [through η0] to the whole of S(X) are determined uniquely; and then g must be the identity by weak universality.
So we only have to deal with the case where X is a continuous dcpo; but this is difficult without coherence. A simpler case is when X is an algebraic dcpo. Then X has a basis Fin(X) consisting of its finite elements, and X is isomorphic to the ideal completion I(Fin(X)) of Fin(X). For every poset K, let bc0(K) be the set of those finite intersections of sets ↑x, x in K, that are non-empty, ordered by reverse inclusion. (This is similar to our previous construction of bc(X), except we only take finite intersections.) Ershov builds the bc-hull of X as the ideal completion I(bc0(Fin(X))) of bc0(Fin(X)).
Let us check that I(bc0(Fin(X))) is a bc-hull of X (assuming X algebraic, but not necessarily coherent). It is an algebraic dcpo, and it has all non-empty infima, computed as intersections (left as an exercise; this depends on the fact that bc0(Fin(X)) has binary suprema, computed as binary intersections), so it is a Scott domain, namely, an algebraic bc-domain. Given any Scott-continuous map f from X to a bc-domain Y, f restricts to a Scott-continuous, hence monotonic map, from Fin(X) to Y. That restriction of f extends to a monotonic map f’ from bc0(Fin(X)) to Y, defined by f’(Q)=inf {f(x) | x ∈ Q}, in the sense that f’(↑x)=f(x) for every x in Fin(X). (This is the same formula as before.) Then f’ extends to a Scott-continuous map f* from I(bc0(Fin(X))) to Y by the Scott formula f*(I) = sup {f’(Q) | Q ∈ I}. The embedding η : X → I(bc0(Fin(X))) maps every x in X to the ideal of all Q in bc0(Fin(X)) such that Q ⊇ ↑y for some finite element y below x. I will let you check that η is Scott-continuous and that f*(η(x))=x for every x in X. Additionally, you are invited to check that weak universality holds: given any Scott-continuous map g : I(bc0(Fin(X))) → I(bc0(Fin(X))) such that g o η = η, g must be the identity map. (The argument uses the Scott formula again, and the same trick as what we used to show that f* is weakly universal in the coherent case.)
The real difficulty is to deal with the case where X is a continuous, not necessarily coherent, dcpo. In that case, X is a retract of an algebraic dcpo Y (Theorem 5.1.48 in the book). Call the retraction r : Y → X and the section s : X → Y. Y is in fact I(X), and s(x)=↡x. One may build bc(X) as a retract of the bc-hull I(bc0(Fin(Y))) of Y, but how? As a hint, Fin(Y)≅X, so one may consider I(bc0(X)), and try to find a suitable retract. One may paraphrase what Ershov does as follows. We first build I(bc0(X)). This is a bc-domain, X embeds into it by η : X → I(bc0(X)) defined by η(x)={Q ∈ bc0(X) | x ∈ int(Q)}, and every Scott-continuous map f from X to a bc-domain Z extends to I(bc0(X)) by the formula f*(I)=supQ ∈ I infx ∈ Q f(x) (in the sense that f* o η=f), but this has no reason to satisfy weak universality. Ershov notices that η[X] is a smooth subdcpo of I(bc0(X)), in the sense that the way-below relation on the former is the restriction of the way-below relation on the latter. With that, he then shows that one can extract a sub-bc-domain Y’ of Y that contains η[X] and in which η[X] is ⋁-dense, meaning that every element of Y’ is a non-empty supremum of elements of η[X] [1, Proposition 15]. That Y’ may still be too big, but ⋁-density gives you that any continuous map g : Y’ → Y’ such that g o η=η is larger than or equal to the identity map. Hence any such g is inflationary. Let F denote the family of those maps g such that g o η=η. As in Escardó’s extension of Pataraia’s fixed point theorem, (this is really what Ershov does in the proof of [1, Theorem 16]) F is a dcpo, and is directed. (Ershov seems to have missed that F is directed, and then goes on to use Zorn’s Lemma, but that is useless. This is directed because given any two maps g and g’ in F, g o g’ is in F and above both g and g’.) Hence F has a unique largest element g. It so turns out that the maximality of g implies that g2=g, so that g is a retraction of Y’ onto its image. Any retract of a bc-domain is a bc-domain, so g[Y’] is a bc-domain, and that is the desired bc-hull, as a few further lines of verification show. Phew.
The Dedekind-MacNeille completion
Oh, one final word, still: clat(X), as we constructed it in the coherent case, is merely the Dedekind-MacNeille completion DM(X) of X (up to order-isomorphism, if we want to be picky).
Recall that E↑ denotes the set of all upper bounds of E, for any subset E of X. Dually, let E↓ denote the set of all lower bounds of E. The Dedekind-MacNeille completion DM(X) of X is the set of all the subsets E of X such that E=E↑↓, ordered by inclusion.
However, it is also (up to order-isomorphism) the set DM‘(X) of all subsets E of X such that E=E↓↑ (note the swapping of ↑ and ↓), ordered by reverse inclusion. Let us check that right away.
It is clear that, for any two subsets A and B of X, A ⊆ B↑ if and only if B ⊆ A↓. Also, the operations E ↦ E↑ and E ↦ E↓ are antitone. It follows that those two operations form a Galois connection (Definition 8.4.17 in the book), hence in particular it is always true that E ⊆ E↑↓. It follows that E↑↓↑ ⊆ E↑ (by applying the antitonic operation E ↦ E↑ to each side of the latter inclusion) and that E↑ ⊆ E↑↓↑ (by using the same inclusion with E replaced by E↑), hence E↑ = E↑↓↑, for every subset E of X. Similarly, E↓ = E↓↑↓ for every subset E of X.
The function E ↦ E↑ maps DM(X) to DM‘(X): that just means that if E=E↑↓ then E↑=E↑↓↑, and that is obvious. Since that map is antitone (with respect to inclusion orderings), but DM‘(X) is ordered by reverse inclusion, it defines a monotonic map from DM(X) to DM‘(X). Similarly, the function E ↦ E↓ is monotonic from DM‘(X) to DM(X), and the definitions of DM(X) and DM‘(X) show that these two functions are mutual inverses. Therefore DM(X) and DM‘(X) are order-isomorphic.
The classical embedding of X into its Dedekind-MacNeille completion DM(X) maps every point x of X to ↓x. That is an element of the Dedekind-MacNeille completion because ↓x = {x}↓ = {x}↓↑↓ = (↓x)↑↓. Up to the above order-isomorphism, we can embed X into DM‘(X) by mapping x to ↑x.
Hence we obtain the following alternate form of our construction:
Theorem. For every coherent continuous dcpo X, the unique clat-hull of X up to isomorphism is its Dedekind-MacNeille completion DM‘(X), with the embedding x ↦ ↑x. Its unique bc-hull is DM‘(X), minus the empty set if present (i.e., if ∅=∅↓↑, or equivalently if X does not have a top element). The Scott topology and the upper Vietoris topology coincide on both.
Note (added by JGL, July 28th, 2019): Zhenchao Lyu told me that the completion process we have applied is exactly the same as the one we used in the construction of Isbell’s non-sober complete lattice.
- Yuri Leonidovich Ershov (Юрий Леонидович Ершов). The bounded-complete hull of an α-space. Theoretical Computer Science 175, 1997, pages 3-13.
— Jean Goubault-Larrecq (July 20th, 2019)