The Hurewicz theorem in homotopy type theory

Journal article

We prove the Hurewicz theorem in homotopy type theory, i.e., that for $X$ a pointed, $(n-1)$-connected type $(n \geq 1)$ and $A$ an abelian group, there is a natural isomorphism $\pi_n(X)^{ab} \otimes A \cong \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 non-trivial 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.

Authors: Christensen, JD; Scoccola, L

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Mathematical Sciences Publishers
• Journal: Algebraic & Geometric Topology
• Volume: 23
• Issue: 5
• Pages: 2107-2140
• Publication date: 2023-07-25
• DOI: 10.2140/agt.2023.23.2107
• ISSN: 1472-2739
• Language: English
• Keywords: Mathematics; Tensor product; Pure mathematics; Homotopy category; Homotopy group; n-connected; Homotopy; Regular homotopy; Homotopy sphere; Type (biology)