{"id":2102,"date":"2019-11-20T11:11:41","date_gmt":"2019-11-20T10:11:41","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=2102"},"modified":"2022-05-17T10:35:15","modified_gmt":"2022-05-17T08:35:15","slug":"quotients-colimits-of-dcpos-and-related-matters","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=2102","title":{"rendered":"Quotients, colimits of dcpos, and related matters"},"content":{"rendered":"\n

Let us start with the following problem. Let X<\/em> be a dcpo, and \u2261 be an equivalence relation on X<\/em>. What is the quotient dcpo X<\/em>\/\u2261? One may think that it is built in the usual way, taking the equivalence classes [x<\/em>] of elements x<\/em> of X<\/em> with respect to \u2261, and ordering them in a suitable way. This approach fails miserably. In order to understand why, we should first understand what a quotient is.<\/p>\n\n\n\n

What dcpo quotients should be<\/h2>\n\n\n\n

We should really think categorically. Although the following lacks some of the abstract beauty of category theory, the quotient dcpo X<\/em>\/\u2261 should be defined by a universal property<\/em>: it should be a dcpo, there should be a continuous map q<\/em> : X<\/em> \u2192 X<\/em>\/\u2261 (intuitively, mapping x<\/em> to its equivalence class) that is compatible with \u2261 (namely, for all x<\/em>, x’<\/em> such that x<\/em>\u2261x’<\/em>, q<\/em>(x<\/em>)=q(x’<\/em>)), and the universal property is that, for every dcpo Y<\/em>, for every continuous map f<\/em> : X<\/em> \u2192 Y<\/em> that is compatible with \u2261, there should be a unique continuous map f’<\/em> : X<\/em>\/\u2261 \u2192 Y<\/em> such that f’<\/em> o q<\/em> = f<\/em>.<\/p>\n\n\n\n

Now this is a clean property, but it is not clear that X<\/em>\/\u2261 exists.<\/p>\n\n\n\n

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 \u03c9-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.<\/p>\n\n\n\n

How not to build dcpo quotients<\/h2>\n\n\n\n

Let me explain the obvious, but wrong way, of constructing X<\/em>\/\u2261.<\/p>\n\n\n\n

We first build the quotient of X<\/em> by \u2261 in Pos<\/strong>, the category of posets. In general, that quotient exists for every poset X<\/em>. The map q<\/em> sends every element x<\/em> to its equivalence class [x<\/em>], and the ordering on the quotient is the coarsest ordering \u2291 such that x<\/em>\u2264x’<\/em> implies [x<\/em>]\u2291[x’<\/em>], for all x<\/em>, x’<\/em> in X<\/em>. Explicitly, [x<\/em>]\u2291[x’<\/em>] if and only if there are finitely many elements xi<\/sub><\/em> and x’i<\/sub><\/em> such that x<\/em>\u2261x<\/em>0<\/sub>\u2264x<\/em>‘0<\/sub>\u2261x<\/em>1<\/sub>\u2264x<\/em>‘1<\/sub>\u2261…\u2261xn<\/sub><\/em>\u2264x’n<\/sub><\/em>\u2261x’<\/em>.<\/p>\n\n\n\n

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\u0144ski space S<\/strong> = {0 < 1}, and take the equivalence relation which equates the element 1 of one copy of S<\/strong> with the element 0 of the next copy. Up to isomorphism, you will obtain N<\/strong> with its usual ordering, and you should at least add an element at infinity to turn it into a dcpo.)<\/p>\n\n\n\n

Building dcpo quotients: the first step<\/h2>\n\n\n\n

Here is now an elementary way of building X<\/em>\/\u2261, 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.<\/p>\n\n\n\n

Hence let X<\/em> 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.<\/p>\n\n\n\n

Let also \u2261 be an equivalence relation on X<\/em>. Let me recall that we wish to find a dcpo X<\/em>\/\u2261, with:<\/p>\n\n\n\n