The Cayley-Dickson construction in HoTT

Our paper on the Cayley-Dickson construction in HoTT, which is joint work with Ulrik Buchholtz, has been submitted to the Arxiv:

The Cayley-Dickson construction in Homotopy Type Theory

In this paper, we formalize the H-space structure on the 3-sphere. One can think of the 3-sphere as the unit-sphere in the quaternions. Since the quaternions form a normed division algebra, multiplication of quaternions can be used to obtain the H-space structure on the 3-sphere. However, these methods are not directly available in HoTT.

Instead, we construct this H-space structure using only homotopy invariant methods. One consequence of this, is that our methods should be applicable to get the H-space structure of the 3-sphere in any setting for homotopy theory where homotopy pushouts are available.

Given the H-space structure on the 3-sphere, we also obtain via the Hopf-construction a fibration S^3 \hookrightarrow{} S^7 \twoheadrightarrow{} S^4. And since inclusion S^3 \hookrightarrow{} S^7 in the Hopf-construction is null-homotopic, we get embeddings \pi_k(S^7) \to{} \pi_k(S^4) of homotopy groups, for any k. In particular, since \pi_7(S^7)=\mathbb{Z}, we get an element of \pi_7(S^4) of infinite order.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s