On the Nielsen-Schreier Theorem in Homotopy Type Theory
From MaRDI portal
Publication:6350432
arXiv2010.01187MaRDI QIDQ6350432
Publication date: 2 October 2020
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.
Has companion code repository: https://github.com/awswan/nielsenschreier-hott
This page was built for publication: On the Nielsen-Schreier Theorem in Homotopy Type Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6350432)
