覆盖空间分类与基点转换的规范化
代数拓扑
2024-09-25 v1 计算机科学中的逻辑
逻辑
摘要
本文采用 homotopy type theory (HoTT) 的语言，首先证明了覆盖空间分类定理的合成版本，其次探讨了在同一 homotopy 群之间进行基点转换的规范化同构问题。在将经典代数拓扑概念翻译到 HoTT 时，存在一定的自由选择。我们最终采用的翻译方式比最初使用的更易于操作。我们讨论了一些早期的尝试，以阐明这一翻译过程。所有证明均使用 Coq 证明辅助器实现，并紧密遵循 Hatcher 等经典著作的论述。
引用
@article{arxiv.2409.15351,
title = {Classification of Covering Spaces and Canonical Change of Basepoint},
author = {Jelle Wemmenhove and Cosmin Manea and Jim Portegies},
journal= {arXiv preprint arXiv:2409.15351},
year = {2024}
}
备注
23 pages