Delooping the sign homomorphism in univalent mathematics

TL;DR

This paper explores the equivalence between algebraic and concrete presentations of groups in univalent mathematics, characterizing and constructing the delooping of the sign homomorphism using univalence and formalized in Agda.

Contribution

It provides a precise characterization of when a pointed map is a delooping of the sign homomorphism and offers multiple constructions, including a sign-homomorphism-free method.

Findings

Characterization of when a pointed map is a delooping of the sign homomorphism

Multiple constructions of the delooping, including a sign-homomorphism-free approach

Formalization of results in the agda-unimath library

Abstract

In univalent mathematics there are at least two equivalent ways to present the category of groups. Groups presented in their usual algebraic form are called abstract groups, and groups presented as pointed connected $1$-types are called concrete groups. Since these two descriptions of the category of groups are equivalent, we find that every algebraic group corresponds uniquely to a concrete group -- its delooping -- and that each abstract group homomorphisms corresponds uniquely to a pointed map between concrete groups. The $n$-th abstract symmetric group $S_n$ of all bijections $[n]\simeq [n]$, for instance, corresponds to the concrete group of all $n$-element types. The sign homomorphism from $S_n$ to $S_2$ should therefore correspond to a pointed map from the type $BS_n$ of all $n$-element types to the type $BS_2$ of all $2$-element types. Making use of the univalence axiom, we characterize precisely when a pointed map $BS_n\to_\ast BS_2$ is a delooping of the sign homomorphism. Then we proceed to give several constructions of the delooping of the sign homomorphism. Notably, the construction following a method of Cartier can be given without reference to the sign homomorphism. Our results are formalized in the agda-unimath library.