分离性、锐元素与 Domain 的 Scott 拓扑
Apartness, sharp elements, and the Scott topology of domains
AI总结：
在构造性框架下研究连续 dcpos 与 Scott 拓扑，提出内在分离性与锐元素概念，证明在锐元素限制下分离性具有紧密与余可递性，并揭示其与强极大元素及 Lawson 拓扑的联系。
摘要：
在构造性数学框架下，我们研究了连续定向完备偏序集（dcpos）和 Scott 拓扑。我们的两个主要创新是内在分离性（intrinsic apartness）和锐元素（sharp elements）的概念。分离是一种不等关系的正面表述，类似于非空性（inhabitedness）是空集的否定这一正面表述。为了说明锐性，我们指出下实数是锐的当且仅当它是可定位的。我们的第一个主要结果是，对于一大类连续 dcpos，Bridges-Vîţǎ 分离拓扑与 Scott 拓扑重合。尽管我们不能期望在非平凡的 dcpos 上存在紧密或余可递的分离，但我们证明了当限制在连续 dcpo 的锐元素上时，内在分离性既是紧密的也是余可递的。这些元素包括 Smyth 和 Heckmann 所研究的强极大元素。我们发展了强极大元素理论，强调了它与锐性和 Lawson 拓扑的联系。最后，我们通过考虑连续 dcpos 的几个自然例子来说明内在分离性、锐性和强极大性：Cantor 和 Baire domain、部分 Dedekind 实数、下实数，以及 Cantor 空间到提升集指数的嵌入。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
