Posted in

Speaker:

Ulrik Buchholtz
Date:

Fri, 2016-02-12 15:30 - 17:00
Location:

MPIM Lecture Hall
Parent event:

Workshop on Homotopy Type Theory One of the open problems in the development of synthetic homotopy

theory in homotopy type theory has been the construction of the

quaternionic and octonionic Hopf fibrations, arising from the H-space

structures on the three- and seven-sphere, respectively. Classically,

we can get these by considering the unit spheres in the quaternion and

octonion algebras, which we in turn can define using the

Cayley-Dickson construction. Here, we give a modified version of this

construction that works directly with the unit spheres, and in the

process we get the H-space structure on the three-sphere in HoTT (the

result has been formalized in Lean). This is based on joint work with

Egbert Rijke.

© MPI f. Mathematik, Bonn | Impressum & Datenschutz |