文章基本信息

标题：ON THE NIELSEN-SCHREIER THEOREM IN HOMOTOPY TYPE THEORY
本地全文：下载
作者：Andrew W Swan
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2022
卷号：18
期号：1
页码：1-15
DOI：10.46298/lmcs-18(1:18)2022
语种：English
出版社：Technical University of Braunschweig
摘要：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.
关键词：homotopy type theory;free groups