Central types and their bands

Jarl G. Taxeras Flaten (Western Univ. Canada)

19-Jan-2024, 16:00-17:15 (23 months ago)

Abstract: We will introduce and motivate the concept of a central type (or space) and explain their associated notion of torsor, called a band. Much like one can deloop a group G by its type of torsors BG, the type of bands of a central type A forms a delooping of A. Moreover, we show that the delooping of A is itself central, allowing us to iterate. This procedure yields a new construction of Eilenberg-Mac Lane spaces, which are examples of central types. We also produce a mysterious formula for delooping pointed self-maps of A, and study the moduli space of H-space structures on a pointed type.

Our results have been shown in homotopy type theory, and most have been formalized using the Coq-HoTT library [1]. For this talk, we do not assume familiarity with type theory; rather, we will translate our results for topologists. This work is joint with Ulrik Buchholtz, Dan Christensen, and Egbert Rijke. [2]

[1] github.com/jarlg/central-types [2] arxiv.org/abs/2301.02636

algebraic geometryanalysis of PDEsalgebraic topologycomplex variablesdifferential geometrygeneral topologygeometric topologyK-theory and homologymetric geometrysymplectic geometry

Audience: researchers in the topic


CRM - Séminaire du CIRGET / Géométrie et Topologie

Series comments: Hybrid seminar of geometry and topology. Laboratory : CIRGET - www.cirget.uqam.ca The homepage of the seminar is www.cirget.uqam.ca/fr/seminaires.html

[[Please provide your first and last name so that the speaker can identify you. Kindly submit your questions or comments using the chat box, not via audio.]]

The livestream is on Zoom at uqam.zoom.us/j/88383789249 It is recommended to subscribe to the CIRGET newsletter. Please send an email to haedrich.alexandra@uqam.ca , providing your name and affiliation.

Some talks can be seen at www.youtube.com/channel/UCLkFm-uEvXSf9y-iQtWOLWA

Organizers: Julien Keller*, Duncan McCoy
*contact for this listing

Export talk to