Apartness, sharp elements, and the Scott topology of domains

TL;DR

This paper introduces the concepts of intrinsic apartness and sharp elements in continuous dcpos, showing their topological and order-theoretic properties, and illustrating these ideas with classical domain examples.

Contribution

It defines intrinsic apartness and sharp elements, proves their properties, and relates them to existing topologies and maximal elements in continuous dcpos.

Findings

The Scott topology and the apartness topology coincide for a large class of continuous dcpos.

Intrinsic apartness is tight and cotransitive on sharp elements, including strongly maximal elements.

Examples include Cantor and Baire domains, partial Dedekind reals, and embeddings of Cantor space.

Abstract

Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Being apart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulation of nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Our first main result is that for a large class of continuous dcpos, the Bridges-V\^i\c{t}\v{a} apartness topology and the Scott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos, we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements of a continuous dcpo. These include the strongly maximal elements, as studied by Smyth and Heckmann. We develop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawson topology. Finally, we illustrate the intrinsic apartness, sharpness and strong maximality by considering several natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals, the lower reals and finally, an embedding of Cantor space into an exponential of lifted sets.