Apartness, sharp elements, and the Scott topology of domains

de Jong, Tom

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îţǎ 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.

Citation

de Jong, T. (2023). Apartness, sharp elements, and the Scott topology of domains. Mathematical Structures in Computer Science, 33(7), 573-604. https://doi.org/10.1017/S0960129523000282

• Journal Article Type: Article
• Acceptance Date: Jul 3, 2023
• Online Publication Date: Aug 2, 2023
• Publication Date: 2023-08
• Deposit Date: Sep 11, 2023
• Publicly Available Date: Sep 11, 2023
• Journal: Mathematical Structures in Computer Science
• Print ISSN: 0960-1295
• Electronic ISSN: 1469-8072
• Publisher: Cambridge University Press
• Peer Reviewed: Peer Reviewed
• Volume: 33
• Issue: 7
• Pages: 573-604
• DOI: https://doi.org/10.1017/S0960129523000282
• Keywords: Constructive mathematics; domain theory; continuous directed complete posets (dcpos); Scott topology; apartness; sharp elements; strongly maximal elements
• Public URL: https://nottingham-repository.worktribe.com/output/25183173
• Publisher URL: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/apartness-sharp-elements-and-the-scott-topology-of-domains/FCF2C566AA1D309CDC9258A7C319981E
• Additional Information: Copyright: © The Author(s), 2023. Published by Cambridge University Press; License: This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.; Free to read: This content has been made available to all.