构造性域论中提升教义的张量结构
范畴论
2025-01-31 v5 计算机科学中的逻辑
摘要
我们综述了构造性域论（即任意初等拓扑斯上的有向完全偏序集 (dcpos) 理论）中提升教义的二维和张量结构。我们确立了 dcpos 提升作为 Sierpiński 锥的泛性质，由此推导出：(1) 提升构成一个 Kock-Zöberlein 教义；(2) 提升代数、 pointed dcpos 和归纳偏序集构成了规范等价的局部偏序 2-范畴；(3) 提升代数范畴是余完备的，其连通余极限由到 dcpos 的遗忘函子创建。最后，我们通过 smash 积推导了提升 2-单子的 Eilenberg-Moore resolutions 的对称幺半闭包；这些 smash 积被证明既能分类双线性映射也能分类严格映射，我们在构造性设定下证明了这两者是重合的。我们提供了将 smash 积计算为 dcpo 余等化子和提升代数余等化子的几个具体算例，并将其与 Seal 的更抽象结果进行了比较。尽管所有这些结果在经典情形下是众所周知的，但现有的证明并不适用于构造性设定；事实上，提升单子 Eilenberg-Moore 范畴的经典分析依赖于所有提升代数都是自由的这一事实，而该条件在构造性情形下尚未知是否成立。
引用
@article{arxiv.2312.17023,
title = {Tensorial structure of the lifting doctrine in constructive domain theory},
author = {Jonathan Sterling},
journal= {arXiv preprint arXiv:2312.17023},
year = {2025}
}
备注
Minor errors fixed; final version to appear in the CATMI (Category Theory at Work in Computational Mathematics and Theoretical Informatics) volume of Fundamental Structures in Computational and Pure Mathematics