Ulrik Buchholtz lectures on Univalent group theory (1-3)

Ulrik Buchholtz (University of Nottingham) holds 3 lectures today about Univalent Group Theory.

First lecture: 10:45 - 11:45
Second lecture: 13:30 - 14:30
Third lecture: 15:00 - 16:00

Abstract:

Insofar as univalent mathematics is a more naive version of homotopical mathematics, univalent group theory is a more naive version of homotopical group theory. Univalent group theory is concerned with doing everything at the level of classifying types. Recall that homotopy types are equivalently infinity groupoids, and groups are equivalently pointed, connected groupoids (i.e., classifying spaces). Indeed, the somewhat annoying circumstance that we don't know how to define many higher algebraic structures in univalent foundations (such as infinity monoids/categories) has stimulated the study of the ones we have, namely infinity groups of various kinds, represented by their classifying spaces. Another distinguished feature of univalent group theory is the prominent use of univalent universes. Indeed, the universe provides many concrete models of classifying spaces that are good for mapping into, and hence suitable for calculating cohomology groups.

No type of theory knowledge is presupposed. Rather, I hope the lectures can serve both as an introduction to homotopy type theory/univalent mathematics via the well-known subject of (undergraduate level) group theory and as an invitation to related topics such as higher topos theory, constructive mathematics, and indeed, homotopical group theory itself.

A possible outline:

  1. Undergraduate group theory from the point of view of homotopy theory/univalent mathematics.
  2. More advanced topics, like the use of path spaces in pushouts for combinatorial group theory, and higher group theory (i.e., pointed (k-1)-connected (n+k)-types as classifying generalized groups).
  3. Reaping the benefits of working constructively by externalizing the results in higher toposes, e.g., for cohomology calculations in synthetic algebraic geometry.

Topics could also vary according to audience preference.