Egbert Rijke: Concrete permutation groups

Joint work with Éléonore Mangel (École normale supérieure Paris-Saclay).

Groups were originally invented to study symmetries of things. This lead to the abstract definition of groups that we all know. With the advance of type theory and univalence, however, we are in a unique position to solidify group theory's connection to symmetries. The dihedral groups, for instance, are the symmetries of the polygons. In type theory we would represent the $n$-th dihedral group as the type of all $n$-gons. Similarly, the $n$-th hyperoctahedral group is presented concretely as the type of all n-cubes. The examples that are most relevant for the present talk are the permutation groups: they are the symmetries of the n-element sets so the permutation groups are presented concretely as the type of all $n$-element sets. All of these concrete presentations of groups are pointed connected 1-types. Thus we define a concrete group to be a pointed connected 1-type, and concrete group homomorphisms are just base-point preserving maps between them. The category of pointed connected 1-types is equivalent to the category of abstract groups.

This leads to a simple question: What does the sign homomorphism from the $n$-th permutation group $S_n$ into $S_2$ look like in the world of concrete groups. In other words, which base-point preserving map from the type of all $n$-element types to the type of all $2$-element types is the concrete counterpart of the sign homomorphism. Or, to put it differently yet another time: How do we define a full functor (i.e. surjective on morphisms) from the groupoid of all $n$-element sets to the groupoid of all $2$-element sets. I will present two solutions to this problem, both motivated by the theory of group torsors (which I will explain).