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.
翻译:在构造性框架下,我们研究连续定向完备偏序集(dcpos)及斯科特拓扑。本文的两项核心创新在于:内蕴分离性概念与尖锐元素概念。分离性是对不等关系的正面刻画,类似于"非空性"作为"非空"的正面表述。为阐释尖锐性,我们指出:下实数具有尖锐性当且仅当其具有定位性。第一个主要结论表明:对于一大类连续dcpos,布里奇斯-维策亚分离拓扑与斯科特拓扑等价。尽管无法期望非平凡dcpos上存在紧致或共传递的分离关系,我们证明当限制在连续dcpo的尖锐元素上时,内蕴分离性同时具有紧致性与共传递性。这些尖锐元素包含Smyth与Heckmann所研究的强极大元素。我们发展了强极大元素理论,着重揭示其与尖锐性及劳森拓扑的关联。最后,通过分析连续dcpos的若干自然实例:康托尔域与贝尔域、部分戴德金实数、下实数,以及康托尔空间到提升集指数空间的嵌入,对内蕴分离性、尖锐性与强极大性进行实例化说明。