hopf fibration (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

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

- $S^0 \hookrightarrow S^1 \to S^1$ The
~~junior~~~~hopf~~~~fibration~~real Hopf fibration - $S^1 \hookrightarrow S^3 \to S^2$ The usual
~~hopf~~~~fibration~~complex Hopf fibration - $S^3 \hookrightarrow S^7 \to S^4$ The
~~quarterionic~~~~hopf~~~~fibration~~quaternionic Hopf fibration - $S^7 \hookrightarrow S^15 \to S^8$ The
~~(octionic/cayley)~~~~hopf~~~~fibration~~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 $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}^{\mathrm{10}}$~~ S^1~~ S^0, ${S}^{\mathrm{31}}$~~ S^3~~ S^1~~ ~~ ,~~ and~~${S}^{\mathrm{73}}$~~ 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~~~~a~~~~homotopy 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.

- Ulrik Buchholtz, Egbert Rijke,
*The Cayley-Dickson Construction in Homotopy Type Theory*(arXiv:1610.01134)

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.