On the Nielsen-Schreier Theorem in Homotopy Type Theory

TL;DR

This paper formulates the Nielsen-Schreier theorem within homotopy type theory, demonstrating its constructive validity for finite index subgroups and analyzing the theorem's limitations in certain topos models.

Contribution

It provides a homotopy type theory formulation of the Nielsen-Schreier theorem and explores its validity under different logical assumptions and models.

Findings

Finite index subgroups case holds constructively.

Full theorem requires the axiom of choice.

Counterexample in a boolean infinity topos.

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.