Andrew W Swan - On the Nielsen-Schreier Theorem in Homotopy Type Theory

lmcs:7676 - Logical Methods in Computer Science, January 20, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:18)2022
On the Nielsen-Schreier Theorem in Homotopy Type TheoryArticle

Authors: Andrew W Swan ORCID

    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.


    Volume: Volume 18, Issue 1
    Published on: January 20, 2022
    Accepted on: December 15, 2021
    Submitted on: July 13, 2021
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,03F65, 03B38, 20E05

    1 Document citing this article

    Consultation statistics

    This page has been seen 1363 times.
    This article's PDF has been downloaded 557 times.