The Hurewicz theorem in homotopy type theory

Christensen, J Daniel; Scoccola, Luis

doi:10.2140/agt.2023.23.2107

Download this article
	For screen
	For printing

Recent Issues

The Journal

About the Journal

Editorial Board

Subscriptions

Submission Guidelines

Submission Page

Policies for Authors

Ethics Statement

ISSN 1472-2739 (online)

ISSN 1472-2747 (print)

Author Index

To Appear

Other MSP Journals

The Hurewicz theorem in homotopy type theory

J Daniel Christensen and Luis Scoccola

Algebraic & Geometric Topology 23 (2023) 2107–2140

DOI: 10.2140/agt.2023.23.2107

Abstract

We prove the Hurewicz theorem in homotopy type theory, ie that for $X$ a pointed, $(n - 1)$ –connected type, with $n \geq 1$ , and $A$ an abelian group, there is a natural isomorphism $π_{n} {(X)}^{ab} \otimes A ≅ {\tilde{H}}_{n} (X; A)$ relating the abelianization of the homotopy groups with the homology. We also compute the connectivity of a smash product of types and express the lowest nontrivial homotopy group as a tensor product. Along the way, we study magmas, loop spaces, connected covers and prespectra, and we use $1$ –coherent categories to express naturality and for the Yoneda lemma.

As homotopy type theory has models in all $\infty$ –toposes, our results can be viewed as extending known results about spaces to all other $\infty$ –toposes.

Keywords

Hurewicz theorem, homotopy group, homology group, magma, loop space, tensor product, homotopy type theory

Mathematical Subject Classification

Primary: 55Q99

Secondary: 03B38, 18N60, 55N99

References

Publication

Received: 29 September 2020

Revised: 24 January 2022

Accepted: 16 February 2022

Published: 25 July 2023

Authors

J Daniel Christensen
Department of Mathematics University of Western Ontario London, ON Canada

Luis Scoccola
Department of Mathematics University of Western Ontario London, ON Canada

Open Access made possible by participating institutions via Subscribe to Open.

Volume 23, issue 5 (2023)