The long exact sequence of homotopy n-groups

Buchholtz, Ulrik; Rijke, Egbert

Abstract

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence F→E→BF→E→B of pointed types and show that any fiber sequence F↪E↠BF↪E↠B of arbitrary types induces a short sequence

Fn−1 En−1 Bn−1

that is n-exact at ∥E∥n−1‖E‖n−1. We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for n=1,2n=1,2. As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.

Citation

Buchholtz, U., & Rijke, E. (2023). The long exact sequence of homotopy n-groups. Mathematical Structures in Computer Science, 33(Special Issue 8: Homotopy Type Theory 2019), 679-687. https://doi.org/10.1017/S0960129523000038

• Journal Article Type: Article
• Acceptance Date: Jan 17, 2023
• Online Publication Date: Sep 7, 2023
• Publication Date: 2023-09
• Deposit Date: Oct 11, 2024
• Publicly Available Date: Oct 16, 2024
• Journal: Mathematical Structures in Computer Science
• Print ISSN: 0960-1295
• Electronic ISSN: 1469-8072
• Publisher: Cambridge University Press
• Peer Reviewed: Peer Reviewed
• Volume: 33
• Issue: Special Issue 8: Homotopy Type Theory 2019
• Pages: 679-687
• DOI: https://doi.org/10.1017/S0960129523000038
• Public URL: https://nottingham-repository.worktribe.com/output/39730588
• Publisher URL: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/long-exact-sequence-of-homotopy-ngroups/D332A8C1475F22036CD140C2BA429FE0