On the Nielsen-Schreier Theorem in Homotopy Type Theory
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 axi...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7676/pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |