Let us start with the following problem. Let X be a dcpo, and ≡ be an equivalence relation on X. What is the quotient dcpo X/≡? One may think that it is built in the usual way, taking the equivalence classes [x] of elements x of X with respect to ≡, and ordering them in a suitable way. This approach fails miserably. In order to understand why, we should first understand what a quotient is.
What dcpo quotients should be
We should really think categorically. Although the following lacks some of the abstract beauty of category theory, the quotient dcpo X/≡ should be defined by a universal property: it should be a dcpo, there should be a continuous map q : X → X/≡ (intuitively, mapping x to its equivalence class) that is compatible with ≡ (namely, for all x, x’ such that x≡x’, q(x)=q(x’)), and the universal property is that, for every dcpo Y, for every continuous map f : X → Y that is compatible with ≡, there should be a unique continuous map f’ : X/≡ → Y such that f’ o q = f.
Now this is a clean property, but it is not clear that X/≡ exists.
The fact that dcpo quotients (and, more generally, colimits, see below) exist has been proved a number of times. Jose Meseguer [1] proved it for ω-dcpos in only a few lines, using extremal epi-mono factorizations and well-poweredness. A. Fiech [2] proved it by elementary arguments, and also considers the case of algebraic dcpos. He also says that A. Jung also had a proof. However that proof is referenced as “Jung, A. (1992) Private notes communicated by Michael Huth in April 1992”, which makes it harder to obtain. Let me venture that the way I am going to build them in this post is what A. Jung had in mind. The last proof I know is as a brief corollary of general constructions in [3], a paper I will talk more about below.
How not to build dcpo quotients
Let me explain the obvious, but wrong way, of constructing X/≡.
We first build the quotient of X by ≡ in Pos, the category of posets. In general, that quotient exists for every poset X. The map q sends every element x to its equivalence class [x], and the ordering on the quotient is the coarsest ordering ⊑ such that x≤x’ implies [x]⊑[x’], for all x, x’ in X. Explicitly, [x]⊑[x’] if and only if there are finitely many elements xi and x’i such that x≡x0≤x‘0≡x1≤x‘1≡…≡xn≤x’n≡x’.
Oops… that is not an ordering in general! only a preordering, so we have to take a further quotient. I will not say more, except to say that even if we do so, the result will in general fail to be a dcpo, so something more has to be done again. (Consider the dcpo obtained as the disjoint sum of countably many copies of Sierpiński space S = {0 < 1}, and take the equivalence relation which equates the element 1 of one copy of S with the element 0 of the next copy. Up to isomorphism, you will obtain N with its usual ordering, and you should at least add an element at infinity to turn it into a dcpo.)
Building dcpo quotients: the first step
Here is now an elementary way of building X/≡, inspired by A. Jung, M.A. Moshier, and S. Vickers [3]. They solve a much more general problem, and they consider dcpo quotients in Section 6.1, although somewhat cursorily. I will briefly say something about this paper at the end of this post.
Hence let X be a poset. While we are interested in dcpos, it is equally easy, and useful, to build a dcpo quotient out of a poset. We will see the advantage of doing so near the end of this post.
Let also ≡ be an equivalence relation on X. Let me recall that we wish to find a dcpo X/≡, with:
- a Scott-continuous map q : X → X/≡,
- that is compatible with ≡,
- and satisfying the universal property that, for every dcpo Y, for every Scott-continuous map f : X → Y that is compatible with ≡, there is a unique continuous map f’ : X/≡ → Y such that f’ o q = f.
Let us call a subset C of X saturated if and only if for every x in C, for every x’≡x, x’ is also in C. We define H≡(X) as the set of all saturated Scott-closed subsets of X. Let us order it by inclusion. This is a variant of the Hoare powerdomain. It is easy to see that the intersection of any family of saturated Scott-closed sets is again saturated and Scott-closed. It follows that H≡(X) is a complete lattice, in which infima are computed as intersections.
Suprema are more complicated to describe explicitly. Intuitively, one would compute the union, then take the closure, then add all the elements equivalent to elements in the latter set, then take the closure again, then again add all equivalent elements, …, and continue this way into the transfinite.
A simpler, but equivalent, description is to realize that every subset A of X has a saturated closure cl≡(A): this is the smallest saturated closed subset of X that contains A, and it is obtained by taking the intersection of all the saturated closed sets that contain A. This is what we were trying to build by taking the closure, then adding all equivalent elements, and repeating the process transfinitely. Then the supremum of a family of elements of H≡(X) is the saturated closure of the union of the elements of the family.
There is a map q : X → H≡(X), defined by q(x) = cl≡({x}). Good. It is monotonic: if x≤x’, then x is in cl≡({x‘}), so the whole of cl≡({x}) is included in cl≡({x‘}). By the same sort of argument, if x≡x’, then q(x)≤q(x’) as well, hence q(x)=q(x’), by symmetry: so q is compatible with ≡. Very good.
We claim that q is Scott-continuous. We consider a directed family (xi)i ∈ I in X, with some element x as a supremum. Since q is monotonic, supi ∈ I q(xi) ⊆ q(x). In the reverse direction, we note that every xi is in q(xi), hence in supi ∈ I q(xi), and because the latter is Scott-closed, it must therefore contain x as well. It follows that supi ∈ I q(xi) is a saturated closed subset of X that contains x, so q(x) = cl≡({x}) is included in it, being the smallest saturated closed subset of X that contains x. We conclude that q(x) ⊆ supi ∈ I q(xi).
So far so good… but H≡(X) is not the quotient dcpo we are looking for. It is way too big. For example, if you start from X=N, with equality as ordering, and with equality for ≡, then we expect the dcpo quotient to be N itself, but H≡(X) is the whole powerset of X, which is not even countable.
Building dcpo quotients: the second step
But we can extract the required dcpo from H≡(X).
In every dcpo Z, for every subset A of Z, there is a smallest subdcpo of Z containing A. This is obtained as the intersection of all subdcpos of Z that contain A, and is sometimes called the inductive closure of A in Z. I will call it the d-closure of A, for reasons that appear in the appendix to this post.
Again, we could try to build the d-closure of A in Z by taking all the elements of A, then adding all suprema of directed families of elements of A, then adding all suprema of directed families of elements that we have built until now, and continuing transfinitely. (In general, that process does not stop after any finite number of steps, in fact not even after any fixed ordinal-valued number of steps.) That construction is more intuitive, perhaps, more constructive even, but less elementary.
We are now in a position to build the dcpo quotient X/≡:
We define X/≡ as the d-closure of the image Im q of q in H≡(X).
The proof
Let us check that X/≡ and q satisfy all the required properties.
X/≡ is a dcpo… vacuously. The map q : X → H≡(X) takes its values in X/≡… vacuously again. We can then consider q as a map from X to X/≡. It is Scott-continuous, and compatible with ≡. It only remains to check the universal property.
Let f : X → Y be a Scott-continuous map that is compatible with ≡, where Y is a dcpo.
We can build a map g : H≡(X) → H(Y), where H(Y) is the complete lattice of Scott-closed subsets of Y ordered by inclusion, by g(C) = cl(f[C]) (the Scott-closure of the image of C by f).
We claim that the map g is Scott-continuous. Monotonicity is clear. Preservation of directed suprema is harder, but proceeds along standard lines—up to a small twist. Let (Ci)i ∈ I be a directed family in H≡(X), and let C = cl≡(∪i ∈ I Ci) be its supremum in H≡(X). Given that g is monotonic, we only have to show that g(C) ⊆ supi ∈ I g(Ci) (= cl (∪i ∈ I g(Ci))). The easiest way to do this is to consider any closed subset D of Y that contains cl (∪i ∈ I g(Ci)), and to show that it contains g(C). Any such D must contain every g(Ci), hence every image f[Ci]. Hence every Ci is included in f-1(D), so ∪i ∈ I Ci is also included in f-1(D). Now f-1(D) is closed (since f is continuous) and saturated (since f is compatible—this is the twist, compared to the standard argument), so it must also contain cl≡(∪i ∈ I Ci), namely, C. It follows that f[C] is included in D, and therefore, that cl(f[C]) = g(C) is included in D.
Let A be the collection of elements C of H≡(X) such that g(C) is the downward closure of a single point in Y. If that is the case, we call that point f’(C). It is determined uniquely, because ↓y=↓y’ in Y implies y=y’. (Yes, f’ will be the function we are looking for.)
We first observe that A contains Im q. In other words, we claim that for every x in X, g(q(x)) is equal to the downward closure of some point of Y. In fact, we claim that g(q(x))=↓f(x). Let C = q(x) (= cl≡({x})). The point f(x) is in f[C], hence in cl(f[C]) = g(C). Hence ↓f(x) is included in g(q(x)). In order to show the reverse inclusion, it is enough to show that f[C] is included in ↓f(x), since the latter is closed; equivalently, we need to show that cl≡({x}) is included in f-1(↓f(x)), and that is clear since the latter contains x, is closed (since f is continuous), and is saturated (since f is compatible).
Next, we observe that A is a subdcpo of H≡(X). Imagine that we are given a directed family (Ci)i ∈ I in A, and let C = cl≡(∪i ∈ I Ci) be its supremum in H≡(X). For every i in I, g(Ci)=↓f’(Ci), and since g is Scott-continuous, g(C) = cl(∪i ∈ I g(Ci)) = cl(∪i ∈ I ↓f’(Ci)), and we can check that this is the downward closure of supi ∈ I f’(Ci).
Since A is a subdcpo of H≡(X) and A contains Im g, A must contain its d-closure X/≡. Since f’ is defined as a map from A to Y, by restriction we obtain a map (still written f’) from X/≡ to Y.
We claim that f’ is continuous. It is clearly monotonic. Given any directed family (Ci)i ∈ I in A, with supremum C = cl≡(∪i ∈ I Ci) (in A), g(C) = ↓f’(C) is also equal to cl(∪i ∈ I g(Ci)) = cl(∪i ∈ I ↓f’(Ci)) = ↓supi ∈ I f’(Ci), since g is Scott-continuous, and that show that f’ indeed preserves directed suprema.
Finally, f’(q(x)) = f(x) for every x in X: this is how we showed that A contains Im q a few lines ago.
In order to conclude, it only remains to show that f’ is unique. Hence we imagine that we have another continuous map f” : X/≡ → Y such that f” o q = f. Let B be the subset of elements C of H≡(X) such that f”(C)=f’(C). B clearly contains Im q, and is a subdcpo of H≡(X). Hence B contains X/≡.
We are done! X/≡ is the dcpo quotient of X by ≡.
Coequalizers in Dcpo
Let us consider two Scott-continuous maps f, g : X → Y between dcpos. There is a coarsest equivalence relation ≡ on Y such that, for every x in X, f(x)≡g(x). Explicitly, y≡y’ if and only if y=y’ or there are finitely many elements xi such that y=f(x0), g(x0)=f(x1), …, g(xn-1)=f(xn), and g(xn)=y’.
We have just build a dcpo Y/≡ and a Scott-continuous map q : Y → Y/≡, satisfying a certain universal property. Given any Scott-continuous map h : Y → Z such that h o f=h o g, where Z is a dcpo, it is easy to see that h is compatible, so there is a unique Scott-continuous map h’ : Y/≡ → Z such that h = h’ o q. It follows that q : Y → Y/≡ is the coequalizer of the pair of maps f, g. (See Section 4.12.3 in the book for coequalizers, and compare this construction with Example 4.12.11 there.)
In particular, coequalizers exist in the category Dcpo of dcpos.
Colimits in Dcpo
Let F be a diagram in the category Dcpo of dcpos. Let me recall that this is just a functor from a small category I to Dcpo. The colimit of F, if it exists, is the universal cocone over F (see Section 4.12.3 in the book). A coequalizer is a particular form of colimit, and conversely, every colimit arises as a coequalizer of a (generally infinite) coproduct, provided all those coproducts exist.
Coproducts in Dcpo do indeed exist, and contrarily to quotients, they are very simple: they are just disjoint unions, and only elements in the same summand can be compared.
Hence all colimits exist in Dcpo.
Explicitly, given a diagram F : I → Dcpo as above, we take the coproduct X of all the dcpos F(A), where A ranges over the objects of I. This is the set of pairs (A, x), where A ranges over the objets of I, and x in F(A), ordered by (A, x) ≤ (B, y) iff A=B and x≤y. We define an equivalence relation ≡ on X as the coarsest one such that, for every morphism j : A → B in I, for every x in F(A), (A, x) ≡ (B, F(j) (x)). And voilà, the colimit of F in Dcpo is our dcpo quotient X/≡.
D-completions
Remember that we have built our dcpo quotient X/≡ from a general poset X, not a dcpo. In the apparently trivial case where ≡ is the equality relation =, we have therefore built a dcpo X/= (yes, the notation is a bit silly) with:
- a Scott-continuous map q : X → X/=,
- satisfying the universal property that, for every dcpo Y, for every Scott-continuous map f : X → Y, there is a unique continuous map f’ : X/= → Y such that f’ o q = f.
(We have omitted the compatibility conditions, since they are vacuously true here.)
Such a dcpo X/= is called a dcpo completion, or d-completion, of the poset X. That d-completions always exist (and are unique up to isomorphism) was first shown by D. Zhao and T. Fan [5], and the construction was analyzed and put in context by K. Keimel and J. Lawson [4]. (The Zhao-Fan result seems to predate [4], although the publication dates tend to indicate the contrary, as can be seen by the fact that Keimel and Lawson cite [5] as a preprint.)
I will not say that we have obtained the d-completion for free: we have sweated a bit to obtain dcpo quotients in the first place! But there was nothing more to be done than to assume X to be a poset instead of a dcpo in order to obtain d-completions as a byproduct of dcpo quotients.
If you read [5], you will probably realize that our strategy to produce dcpo quotients is the same as Keimel and Lawson’s approach to building the d-completion, too. The appendix on d-closures at the end of this post is taken from [5], too.
Dcpo presentations
Near the beginning of this post, I had said that my way of building dcpo quotients is inspired by A. Jung, M. A. Moshier, and S. Vickers [3]. Their setting is rather more general.
They start with so-called dcpo presentations. A dcpo presentation is a preordered set P together with a set of so-called covers, which are pairs x ⊲ D of a point x in P and of a directed family in P. One should think of such a cover as a specification that we would like to make x be below the supremum of D. The free dcpo on a dcpo presentation is a pair of a dcpo Y and of a monotonic map q : P → Y such that:
- q preserves covers, namely for every cover x ⊲ D, q(x) ≤ sup q[D],
- and q is universal with this property: for every monotonic map f : P → Z to a dcpo Z that preserves covers, there is a unique Scott-continuous map f’ : Y → Z such that f = f’ o q.
The main point of [3] is to show that such a free dcpo always exists. (I may talk about it another time, but I think you already have an idea how this can be built.) Section 6.1 of this paper argues that we obtain dcpo colimits from that construction. I will argue for dcpo quotients: X/≡ is obtained by taking P=X, with covers all pairs x ⊲ D such that sup D exists and is equivalent to x. They build the dcpo Y as a least subdcpo of a complete lattice of so-called C-ideals, and one can check that their C-ideals in that case are exactly the saturated Scott-closed subset. Hence what we have done is really a special case of their construction.
Appendix: the d-topology
Here is a purely topological description of the d-closure. Let me remind you that the d-closure of a subset A of a dcpo Z is the smallest subdcpo of Z that contains A.
First note that the d-closure is not the Scott-closure of A, because we are not requiring it to be downwards closed. Instead, we define the d-topology as the topology whose closed sets are exactly the subsets that are closed under the formation of directed suprema—in other words, the subdcpos. This was introduced by K. Keimel and J. Lawson [4].
Then the d-closure is simply the closure in the d-topology. Oh yes, sure, that is a tautology… But the d-topology is a useful notion! (By the way, the authors of [3] say in a footnote that the d-topology appears to have first been considered by Oswald Wyler in 1981. Having just reread that paper, I do not think so.)
In order to appreciate how far from the Scott topology the d-topology is, one should realize that the d-topology is always Hausdorff. Indeed, every Scott-open set is open in the d-topology, and also every downwards-closed subset (for rather trivial reasons…); if x≰y, then we can separate x from y by taking ↓x as open neighborhood of x, and its complement as open neighborhood of y. In general, the d-topology is finer than the Skula topology obtained from the Scott topology, and the Skula topology of a T0 space is already always Hausdorff.
- Jose Meseguer. On order-complete universal algebra and enriched functorial semantics. Proceedings of the 1977 International FCT-Conference, Poznan-Kornik, Poland, September 1977, pages 294–301.
- Adrian Fiech. Colimits in the category DCPO. Mathematical Structures in Computer Science, 6(5), October 1995, pages 455-468.
- Achim Jung, M. Andrew Moshier, and Steve Vickers. Presenting dcpos and dcpo algebras. Proceedings of the 24th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIV), May 2008, Philadelphia, PA, USA. Edited by A. Bauer and M. Mislove. Electronic Notes in Theoretical Computer Science 218, pages 209-229.
- Klaus Keimel and Jimmie D. Lawson. D-completions and the d-topology. Annals of Pure and Applied Logic 159(3), June 2009, pages 292-306.
- Dongsheng Zhao and Taihe Fan. Dcpo-completion of posets. Theoretical Computer Science 411(22-24), May 2010, pages 2167-2173.
— Jean Goubault-Larrecq (November 20th, 2019)