Léo Mangel: Formalisation of Cartier's delooping of the sign homomorphism
Léo Mangel (École normale supérieure Paris-Saclay)
Joint work with Egbert Rijke.
Abstract: Homotopy type theory allows us to study group theory more concretely by focusing on symmetries. We define concrete groups as pointed connected 1-types and concrete group homomorphisms as base-point preserving maps between them. By taking the loop space of a concrete group, we obtain the usual notion of a group, called here abstract group. We can also easily obtain an abstract group homomorphism from a concrete one by using the functorial action of the loop space functor. The operation turning concrete groups into abstract groups is an equivalence of categories. The inverse functor, delooping groups and their homomorphisms, is more complicated.
This raises the question what the deloopings of familiar group homomorphisms are. The goal of our project was to find an explicit description of the delooping of the sign homomorphism from $S_n$ to $S_2$. I will present a definition attributed to Cartier, making use of the univalence axiom. All the work presented was formalised with Agda in the agda-unimath library.