Homotopy Type Theory
hopf fibration (Rev #4)

In classical algebraic topology we have four Hopf fibrations (of spheres):

  1. S 0S 1S 1S^0 \hookrightarrow S^1 \to S^1 The real Hopf fibration
  2. S 1S 3S 2S^1 \hookrightarrow S^3 \to S^2 The usual complex Hopf fibration
  3. S 3S 7S 4S^3 \hookrightarrow S^7 \to S^4 The quaternionic Hopf fibration
  4. S 7S 15S 8S^7 \hookrightarrow S^15 \to S^8 The octonionic Hopf fibration

These can be constructed in HoTT as part of a more general construction:

A H-space structure on a pointed (connected?) type AA gives a fibration over ΣA\Sigma A via the hopf construction. This fibration can be written classically as: AA*AΣAA \to A\ast A \to \Sigma A where A*AA\ast A is the join of AA and AA. This is all done in the HoTT book. Note that ΣA\Sigma A can be written as a homotopy pushout ΣA:=1 A1\Sigma A := \mathbf 1 \sqcup^A \mathbf 1 , and there is a lemma in the HoTT book allowing you to construct a fibration on a pushout (the equivalence AAA \to A needed is simply the multiplication from the H-space μ(a,)\mu(a,-)).

Thus the problem of constructing a hopf fibration reduces to finding a H-space structure on the spheres: the S 0S^0, S 1S^1, S 3S^3 and S 7S^7.

  • For S 0=2S^0=\mathbf 2 this is a trivial exercise and it is in the book.

  • For S 1S^1 Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.

  • For S 3S^3 Buchholtz-Rijke 16 solved this through a homotopy theoretic version of the Cayley-Dickson construction.

  • For S 7S^7 this is still an open problem.

It is still an open problem to show that these are the only spaces to have a H-space structure.


category: homotopy theory

Revision on September 4, 2018 at 05:12:14 by Ali Caglayan. See the history of this page for a list of all contributions to it.