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^0 \hookrightarrow S^1 \to S^1$ The junior hopf fibrationreal Hopf fibration
2. $S^1 \hookrightarrow S^3 \to S^2$ The usual hopf fibrationcomplex Hopf fibration
3. $S^3 \hookrightarrow S^7 \to S^4$ The quarterionic hopf fibrationquaternionic Hopf fibration
4. $S^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 $A$ gives a fibration over $\Sigma A$ via the hopf construction. This fibration can be written classically as: $A \to A\ast A \to \Sigma A$ where $A\ast A$ is the join of $A$ and $A$. This is all done in the HoTT book. Note that $\Sigma A$ can be written as a homotopy pushout $\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 $A \to A$ needed is simply the multiplication from the H-space $\mu(a,-)$).

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

• For$S^0=\mathbf 2$

For $S^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.
• For$S^1$

For $S^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.
• For$S^3$

For $S^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.
• For$S^7$

For $S^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.