同伦类型论中的胞腔上同调
计算机科学中的逻辑
2023-06-22 v4 代数拓扑
摘要
我们呈现同伦类型论中胞腔上同调的一种发展。上同调将一串阿贝尔群与每个空间相关联以捕捉其部分结构，并且相比同伦群的优势在于许多常见空间的这些阿贝尔群更易计算。胞腔上同调是一类专为胞腔复形设计的上同调：胞腔复形通过逐阶段粘贴维数渐高的球面构建，而胞腔上同调由球面如何粘贴的组合描述定义这些群。我们的主要结果是，对有限胞腔复形，广泛一类上同调理论（包括通过 Eilenberg-MacLane 空间定义者）可经胞腔上同调计算。该结果在 Agda 证明助手中形式化。
引用
@article{arxiv.1802.02191,
title = {Cellular Cohomology in Homotopy Type Theory},
author = {Ulrik Buchholtz and Kuen-Bang Hou},
journal= {arXiv preprint arXiv:1802.02191},
year = {2023}
}