Homotopy Type Theory
hopf fibration (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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

  1. S 0S 1S 1S^0 \hookrightarrow S^1 \to S^1 The junior hopf fibrationreal Hopf fibration
  2. S 1S 3S 2S^1 \hookrightarrow S^3 \to S^2 The usual hopf fibrationcomplex Hopf fibration
  3. S 3S 7S 4S^3 \hookrightarrow S^7 \to S^4 The quarterionic hopf fibrationquaternionic Hopf fibration
  4. S 7S 15S 8S^7 \hookrightarrow S^15 \to S^8 The (octionic/cayley) hopf fibrationoctonionic 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:S 0S^0spheres , : theS 1 0 S^1 S^0, S 3 1 S^3 S^1 , andS 7 3 S^7 S^3 and S 7S^7.

  • ForS 0=2S^0=\mathbf 2

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

    this is a trivial exercise and it is in the book.
  • ForS 1S^1

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

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

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

    Buchholtz and Rijke solved this early 2016 through ahomotopy version of the Cayley-Dickson construction.
  • ForS 7S^7

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

    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.

References

Revision on August 5, 2018 at 10:01:39 by Urs Schreiber. See the history of this page for a list of all contributions to it.