构造性域论中提升学说的张量结构
Tensorial structure of the lifting doctrine in constructive domain theory
AI总结：
本文综述了构造性域论中提升学说的二维与张量结构，建立了dcpos提升的泛性质，推导了提升代数范畴的余完备性及其对称幺半闭包，并提供了具体计算。
摘要：
我们综述了构造性域论中提升学说的二维与张量结构，即任意初等拓扑斯上的有向完备偏序集（dcpos）理论中的提升学说。我们建立了dcpos提升作为Sierpiński锥的泛性质，由此推导出：（1）提升构成Kock-Zöberlein学说；（2）提升代数、有向dcpos和归纳偏序集构成典范等价的局部偏序2-范畴；（3）提升代数范畴是余完备的，其连通余极限由到dcpos的遗忘函子创建。最后，我们通过smash积推导出提升2-单子的Eilenberg-Moore分解的对称幺半闭包；这些被证明可对双线性映射和严格映射进行分类，我们证明二者在构造性设定中是重合的。我们提供了smash积作为dcpo余等值子和提升代数余等值子的若干具体计算，并将其与Seal更抽象的结果进行比较。尽管所有这些结果在经典情况下是众所周知的，但现有证明不适用于构造性设定；事实上，对提升单子的Eilenberg-Moore范畴的经典分析依赖于所有提升代数都是自由的这一事实，而该条件在构造性上是否成立尚属未知。
英文摘要：
We present a survey of the two-dimensional and tensorial structure of the lifting doctrine in constructive domain theory, i.e. in the theory of directed-complete partial orders (dcpos) over an arbitrary elementary topos. We establish the universal property of lifting of dcpos as the Sierpiński cone, from which we deduce (1) that lifting forms a Kock-Zöberlein doctrine, (2) that lifting algebras, pointed dcpos, and inductive partial orders form canonically equivalent locally posetal 2-categories, and (3) that the category of lifting algebras is cocomplete, with connected colimits created by the forgetful functor to dcpos. Finally we deduce the symmetric monoidal closure of the Eilenberg-Moore resolution of the lifting 2-monad by means of smash products; these are shown to classify both bilinear maps and strict maps, which we prove to coincide in the constructive setting. We provide several concrete computations of the smash product as dcpo coequalisers and lifting algebra coequalisers, and compare these with the more abstract results of Seal. Although all these results are well-known classically, the existing proofs do not apply in a constructive setting; indeed, the classical analysis of the Eilenberg-Moore category of the lifting monad relies on the fact that all lifting algebras are free, a condition that is not known to hold constructively.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
