一句话:证明 σ-frame/σ-locale 可归入形式拓扑,并构造性地刻画最小强稠密 σ-子locale。
本文研究 σ-frame 与 σ-locale 在构造性、无点拓扑中的位置。σ-frame 是具有可数并和有限交、且二元交对可数并分配的偏序集。作者证明 σ-frame(更准确地说是 σ-locale)可视为形式拓扑的一个分支,即直觉主义与直谓式的无点拓扑。具体地,每个 σ-frame L 都可实现为某类特殊形式拓扑中 Lindelöf 元素(其每个覆盖都有可数子覆盖)构成的格,而该形式拓扑又是 L 上自由 frame 的一个表示。随后,文章给出给定 σ-locale 的最小(强)稠密 σ-子locale 的构造性刻画,从而得到 Boolean locale 的“σ-版本”。该发展依赖于可数选择公理。
A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindel\"of elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.