论文标题
部分地图类别
Bilimits in categories of partial maps
论文作者
论文摘要
在某些类别的主要域和域中双利杆菌下嵌入预测对（Epairs）的链的闭合是标准的和众所周知的。例如，斯科特（Scott）的$ d_ \ infty $ construction众所周知，可以在定向完整的部分订单类别中产生ePairs的指向双木，而de jong andEscardó在建设性领域理论中正式化了这一结果。就建设性而言，双利单元的明确约束对主要图和部分地图的类别的明确约束更为模糊。大多数博览会都采用了一个建设性的禁忌，即每个升降机代数都是免费的，将问题降低为在一类尖的域和严格地图中的双利杆菌的构建。在论文的论文中，提出了双imit的明确构造，但没有证据表明，因此在托普斯的epair的指示双膜下关闭了dcpos和部分地图的类别。我们提供了（Grothendieck）-topos-Valid证据，证明DCPOS的类别及其之间的部分地图在Bilimits下关闭；然后，我们描述了一些针对公理和合成领域理论模型的应用。
The closure of chains of embedding-projection pairs (ep-pairs) under bilimits in some categories of predomains and domains is standard and well-known. For instance, Scott's $D_\infty$ construction is well-known to produce directed bilimits of ep-pairs in the category of directed-complete partial orders, and de Jong and Escardó have formalized this result in the constructive domain theory of a topos. The explicit construcition of bilimits for categories of predomains and partial maps is considerably murkier as far as constructivity is concerned; most expositions employ the constructive taboo that every lift-algebra is free, reducing the problem to the construction of bilimits in a category of pointed domains and strict maps. An explicit construction of the bilimit is proposed in the dissertation of Claire Jones, but no proof is given so it remained unclear if the category of dcpos and partial maps was closed under directed bilimits of ep-pairs in a topos. We provide a (Grothendieck)-topos-valid proof that the category of dcpos and partial maps between them is closed under bilimits; then we describe some applications toward models of axiomatic and synthetic domain theory.
