Posted in
Speaker:
Ulrik Buchholtz
Datum:
Fre, 12/02/2016 - 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 |