关于Stone-Cech紧化的存在性
On the existence of Stone-Cech compactification
摘要：
在[G. Curi，“Stone-Cech紧化的精确近似”，Ann. Pure Appl. Logic，146，2-3，2007，pp. 103-123]给出了Stone-Cech紧化在构造型理论CTT中可定义的locale的特征，以及在形式系统CZF+uREA+DC中，通过加强正则扩张公理REA和依赖选择原理，得到了Aczel的构造集合论CZF系统的自然扩张.在本文中，我表明，这种特性继续持有的标准系统CZF加REA，从而消除特别是任何依赖的选择原则。这将遵循一个结果的独立利益，即证明类的连续映射从一个紧凑的正规区域X到一个正规的一个集呈现区域Y是一个集在CZF，即使没有REA。然后证明了非退化布尔locale的Stone-Cech紧化的存在性与CZF（+REA）的公理无关，使得所得到的刻画刻画了所有locale集合的一个恰当子集.这同样适用于CZF+REA的几个甚至是非谓词的扩展，以及CTT。这与高阶海廷算术HHA的上下文中所发生的情况形成对比，因此在任何拓扑论宇宙中：通过Johnstone，Banaschewski和Mulvey的构造，在HHA中，Stone-Cech紧化可以为每个locale定义。
英文摘要：
In [G. Curi, "Exact approximations to Stone-Cech compactification'', Ann. Pure Appl. Logic, 146, 2-3, 2007, pp. 103-123] a characterization is obtained of the locales of which the Stone-Cech compactification can be defined in constructive type theory CTT, and in the formal system CZF+uREA+DC, a natural extension of Aczel's system for constructive set theory CZF by a strengthening of the Regular Extension Axiom REA and the principle of dependent choice. In this paper I show that this characterization continues to hold over the standard system CZF plus REA, thus removing in particular any dependency from a choice principle. This will follow by a result of independent interest, namely the proof that the class of continuous mappings from a compact regular locale X to a regular a set-presented locale Y is a set in CZF, even without REA. It is then shown that the existence of Stone-Cech compactification of a non-degenerate Boolean locale is independent of the axioms of CZF (+REA), so that the obtained characterization characterizes a proper subcollection of the collection of all locales. The same also holds for several, even impredicative, extensions of CZF+REA, as well as for CTT. This is in contrast with what happens in the context of Higher-order Heyting arithmetic HHA - and thus in any topos-theoretic universe: by constructions of Johnstone, Banaschewski and Mulvey, within HHA Stone-Cech compactification can be defined for every locale.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
