Coherence of Dcpos

The nice thing about colleagues is that they sometimes give you a primer on their latest discovery.  The irritating thing about colleagues is that they may prefer you not to announce it before this has been published.  This is what happened to me with a very nice result due to Jia, Jung and Li [1] a while ago.  I guess enough time has passed now.


The question is one of coherence.  See Section 5.2.2 in the book: a space is coherent if and only if the intersection of any two compact saturated subsets is again compact (and saturated, necessarily).  Every T2 space is coherent, but that is no longer the case outside the realm of T2 space, in particular in dcpos.

A typical counter-example is built as follows. Take N, the set of natural numbers, and order them by equality: i.e., let them all be incomparable.  Add two incomparable elements a and b below all elements of N.  Then ↑a is compact saturated, ↑b is compact saturated too, since the upward closure of any finite collection of points is.  But their intersection is N, which is not compact: indeed it is covered by the union of the one-point subsets {n}, nN, which are all Scott-open; and certainly that has no finite subcover.

Call that counter-example Na,b.

How do you prove that a dcpo X is not coherent?  Of course you have to consider any two compact saturated subsets, and show that their intersection is compact.  Among the compact saturated subsets, we have the finitary compacts, and in particular the upward closures of single points ↑x.

Therefore, certainly, if X is coherent, then for any two points x and y, ↑x ∩ ↑y should be compact.  That provides an easy test.  If that fails, as in the case of Na,b, then you know X is not coherent.  But what if the test succeeds?

There is a particularly simple answer to that question in continuous dcpos: a continuous dcpo is coherent if and only if ↑x ∩ ↑y is compact for any two points x and y (Proposition 5.2.34 in the book).

But what about other dcpos?  For example, what about complete lattices?  In that case ↑x ∩ ↑y = ↑(xy) is trivially compact, but it was unknown until recently whether there were any non-coherent complete lattices in their Scott topology.  (I have got some inside information about that… but I cannot speak about that yet.  Update [Jan. 10th, 2021]: all complete lattices are coherent in their Scott topology, by a result of Xi and Lawson.)

The main result

Jia, Jung and Li’s main result is the following:

Thm [1, Lemma 3.1]. Let X be a well-filtered dcpo. X is coherent if and only if ↑x ∩ ↑y is compact for any two points x and y.

This is a vast generalization of our previous result on continuous dcpos: recall that every continuous dcpo is sober, and that every sober space is well-filtered (Propositions 8.2.12 and 8.3.5 in the book).

The proof of that theorem is particularly nifty.

We start with the Smyth powerdomain Q(X) of X.  See Proposition 8.3.25 in the book: this is the poset of all non-empty compact saturated subsets of X under reverse inclusion.  This is a dcpo since X is well-filtered, and directed suprema are filtered intersections.

We take a variant of that construction.  We keep the same set Q(X), but we change the topology.  Equip Q(X) with the upper Vietoris topology, whose basic open sets are of the form ☐U, U open in X.  Here ☐U denotes the set of all non-empty saturated subsets Q that are included in U.  In Proposition 8.3.26 of the book, you will find that those sets form a base of the Scott topology, so it may look like the upper Vietoris topology is just another name for the Scott topology of Q(X) under reverse inclusion… but that is only the case if X is well-filtered and locally compact, an assumption which we shall not make.

Q(X) has a rich theory, much like H(X), the Hoare powerspace with the lower Vietoris topology.  This was explored in previous posts.  This is called the Smyth powerspace monad. Oh yes, this was shown to be a monad by Andrea Schalk again [2].  In fact, Q(X) with the upper Vietoris topology is the free unital deflationary sober semi-lattice on X.  (Oops, that sentence is not true.  It looks like it should be that way, but Schalk even has two sections as to why this fails.  Still, Q is a monad, and that is the only think we will need.  Thanks to Matthew de Brecht and Weng Kin Ho for pointing out this problem—corrected on June 26th, 2018.)
In particular, the Q monad has a unit, and that is the map that sends x to ↑x.  But we shall not need that, except to give a hint as what we are going to do.

Jia, Jung and Li start by showing that a parameterized version of the unit is also continuous.  For every compact saturated subset Q of X, let iQ be the map xQ ∩ ↑x.

When Q is of the form ↑y, we know that iQ maps every point x to an element of Q(X). In general, let C be the subset of Q(X) consisting of those non-empty compact saturated subsets Q such that Q ∩ ↑x is compact for every point x in X.  The map iQ is well-defined, as a map from X to Q(X), exactly when Q is in C.

Lemma 1.  For every Q in C, iQ is (well-defined and) continuous.

Proof. We compute the inverse image A of ☐U, where U is open in X, and we show that A is Scott-open.  A is upwards-closed, being the inverse image of an upwards-closed subset by a monotonic map (recall that when x grows, ↑x becomes smaller under inclusion, hence larger in the specialization ordering of Q(X), which is reverse inclusion).

To show that A is Scott-open, we consider a directed family (xi)i ∈ I of points of X, and realize that iQ(supi ∈ I xi)=Q ∩ ↑(supi ∈ I xi) = ∩i ∈ I (Q ∩ ↑xi), because the upward closure of supi ∈ I xi is the collection of upper bounds of (xi)i ∈ I, and that is the intersection of all the upward closures of each xi.  However, ∩i ∈ I (Q ∩ ↑xi)= ∩i ∈ I iQ(xi), and the latter is the supremum of the elements iQ(xi): recall that directed suprema in Q(X) are exactly filtered intersections, when X is well-filtered.  ☐

Lemma 2.  For every Q in C, for every compact saturated set Q’ of X, QQ’ is compact in X.

Proof. We use what is essentially the multiplication of the Q monad.  By Lemma 1, and the fact that the images of compact sets by continuous maps are compact (Proposition 4.4.13 in the book), for every Q in C, the image iQ[Q’] of any given compact saturated subset Q’ of X by iQ is compact in Q(X). (It is compact in a space of compact sets!)

Let Q” be the union of all the elements of iQ[Q’].  We have:

  • Q” is equal to the union of all intersections Q ∩ ↑x, when x ranges over Q’, hence is equal to Q Q’.
  • Q” is itself compact in X.  Indeed, let (Ui)i ∈ I be a directed open cover of Q” (in X).  For every x in Q’, iQ(x) is included in Q”, hence in the union ∪i ∈ I Ui, hence in some Ui.  Recall indeed that compactness is characterized by the fact that one can extract a single element cover from any directed open cover (Proposition 4.4.7 in the book).  This means that for every x in Q’iQ(Q’) is in some ☐Ui.  We have found a directed open cover of iQ[Q’], consisting of the (basic) open sets ☐Ui, i I.  Hence iQ[Q’] is included in some ☐Ui.  In turn, this implies that Q” is included in that Ui.  This terminates our argument that Q” is compact.
    Together with Q” = Q Q’, this concludes our proof.  ☐

We are almost through.  For every point y of X, ↑y is in C: that is our assumption, i.e., its intersection with every set of the form ↑x is compact.  Apply Lemma 2 to Q=↑y: for every compact saturated set Q’, Q’ ∩ ↑y is compact.  That just means that every compact saturated set Q’ is in C! The statement of Lemma 2 then simplifies to: For every compact saturated set Q (necessarily in C), for every compact saturated set Q’ of X, Q Q’ is compact in X.  Hence X is coherent.  ☐

Jia, Jung and Li then go on and derive a few consequences.  For example, every well-filtered complete lattice is coherent.  That should be obvious, now, right?

Jean Goubault-Larrecq(April 2nd, 2017)jgl-2011

  1. Xiaodong Jia, Achim Jung, and Qingguo Li.  A note on the coherence of dcpos.
    Topology and its Applications, Volume 209, 15 August 2016, Pages 235–238.
  2. Andrea Schalk. Algebras for Generalized Power Constructions. PhD Thesis, TU Darmstadt, 1993.