The long exact sequence of homotopy n-groups

DOI10.1017/S0960129523000038MaRDI QIDQ6149949zbMATH OpenOpenAlexFDO

Authors Ulrik Buchholtz, Egbert Rijke

Publication date 5 March 2024

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1912.08696

zbMATH Keywords

higher groupshomotopy type theorylong exact sequenceunivalent foundations

Mathematics Subject Classification ID

Computer science (68-XX)

Abstract: Working in homotopy type theory, we introduce the notion of $n$-exactness for a short sequence $FoEoB$ of pointed types, and show that any fiber sequence $FhookrightarrowEwoheadrightarrowB$ of arbitrary types induces a short sequence $|F{|}_{n-1}o|E{|}_{n-1}o|B{|}_{n-1}$ that is $n$-exact at $|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,2$. As the main application, we obtain the long $n$-exact sequence of homotopy $n$-groups of a fiber sequence.

Cites work

• A Picard-Brauer exact sequence of categorical groups
• Butterflies. I: Morphisms of 2-group stacks
• Eilenberg-MacLane spaces in homotopy type theory
• Higher groups in homotopy type theory
• Higher Topos Theory (AM-170)
• Homotopy type theory. Univalent foundations of mathematics
• Modalities in homotopy type theory
• Semantics of higher inductive types
• The ziqqurath of exact sequences of n-groupoids

This page was built for publication: The long exact sequence of homotopy n-groups

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149949)