On the Nielsen-Schreier Theorem in Homotopy Type Theory
Logic
2023-06-22 v5 Logic in Computer Science
Algebraic Topology
Abstract
We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger "untruncated" version of the theorem is provably false in homotopy type theory.
Keywords
Cite
@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}
}