同伦类型理论中的Nielsen-Schreier定理
逻辑
2023-06-22 v5 计算机科学中的逻辑
代数拓扑
摘要
我们利用群作为带点连通1-截断类型的表示，在同伦类型理论中给出Nielsen-Schreier定理（自由群的子群是自由的）的一种表述。我们证明有限指数子群的特殊情形可构造性地成立，而完整定理由选择公理推出。我们给出一个布尔无穷topos的例子，其中我们对该定理的表述不成立，并展示该定理一个更强的“未截断”版本在同伦类型理论中被证明为假。
引用
@article{arxiv.2010.01187,
title = {On the Nielsen-Schreier Theorem in Homotopy Type Theory},
author = {Andrew W Swan},
journal= {arXiv preprint arXiv:2010.01187},
year = {2023}
}