February 15, Émile Oleon, Delooping cyclic groups with lens spaces in homotopy type theory
Angiuli, Carlo
Émile Oleon will speak about "Delooping cyclic groups with lens spaces in homotopy type theory". The talk will be 60 minutes long, followed by up to 30 minutes of discussion. The abstract is below.
The Zoom link is https://zoom.us/j/994874377
Further information, including the list of upcoming speakers, and videos and slides from past talks, is available at:
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
Carlo
(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)
--
Émile Oleon
Delooping cyclic groups with lens spaces in homotopy type theory
In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called *delooping*. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to arbitrary types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups Z_m which are *cellular*, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of *lens spaces*, which constitute an important family of spaces in algebraic topology. In some sense, this work generalizes the construction of real projective spaces by Buchholtz and Rijke in their LICS'17 paper, which handles the case m = 2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.