A closed graph theorem in dcpo’s

Today I will add one closed graph type theorem to the list made by Terence Tao in his post Closed graph theorem in various categories.

I first recall a few basic notions of domain theory. If X is a poset or partially ordered set, a subset D of X is directed if it is nonempty and for all d, d' \in D there is some d'' \in D such that d \leq d'' and d' \leq d''. The poset X is a dcpo (a directed-complete poset) if every directed subset has a supremum, written \bigvee D. A subset U of X is d-open if \bigvee D \in U \implies D \cap U \neq \emptyset for every directed subset D of X. The collection of d-open subsets forms a topology called the d-topology.

Then a map f : X \rightarrow Y is called d-continuous if it is continuous when X and Y are equipped with their respective d-topologies. It happens that a map f : X \rightarrow Y is order-preserving and d-continuous if and only if f(\bigvee D) = \bigvee f(D) for every directed subset D of X (which is a characterization of Scott continuity). For a proof of this latter assertion and for more on the d-topology of a poset I refer the reader to the paper D-completions and the d-topology by Klaus Keimel and Jimmie Lawson.

Theorem (Closed graph theorem (dcpo theory)). Let X, Y be dcpo’s. Then an order-preserving map f : X \rightarrow Y is d-continuous if and only if the graph \Sigma := \{ (x, f(x)) : x \in X \} is d-closed (in the poset X \times Y equipped with the product topology).

Before giving a proof to this theorem, it is important to recall that the d-topology on the poset X \times Y does not coincide in general with the product of the d-topologies on X and Y.

Proof. Suppose that \Sigma is d-closed, and let D be a directed subset of X. We define \Delta := \{ (d, f(d)) : d \in D \}, which is a subset of \Sigma, and a directed subset of the poset X \times Y since f is order-preserving. It is easily seen that \Delta has a supremum in X \times Y equal to (\bigvee D, \bigvee f(D)); since \Sigma is d-closed, this supremum is in \Sigma, hence f(\bigvee D) = \bigvee f(D). \Box

Question. Do we have a closed graph theorem in (continuous?) dcpo’s equipped with the Lawson topology?