Skip to main content

The quaternionic Hopf fibration in HoTT via a modified Cayley-Dickson construction

Posted in
Ulrik Buchholtz
Fri, 12/02/2016 - 15:30 - 17:00
MPIM Lecture Hall

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
-A A +A