8.5.3 The Hopf fibration
We will first construct a structure of H-space on the circle , hence by \autoreflem:hopf-construction we will get a fibration over with fiber and total space . We will then prove that this join is equivalent to .
There is an H-space structure on the circle .
where is the function defined in \autorefthm:S1-autohtpy, which has the property that .
Now we just have to prove that for every . By definition, if we have . For the equality we do it by induction on :
If is then by definition, so we have .
When varies along , we need to prove that
The left-hand side is equal to , and for the right-hand side we have:
Now recall from \autorefsec:colimits that the join of types and is the pushout of the diagram
We define a map by induction. We first need to define which will be done by induction, then , and then which will be done by induction on the first component of :
For the last equation, note that the right-hand side is of type
whereas it is supposed to be of type
But by the previous clauses in the definition, both of these types are equivalent to the following type:
and so we can coerce by an equivalence to obtain the necessary element. Similarly, we can define a map , and checking that and are inverse to each other is a long and tedious but essentially straightforward computation. ∎
A more conceptual proof sketch is as follows.
Let us consider the following diagram where the maps are the obvious projections:
Taking the colimit of the columns gives the following diagram, whose colimit is :
On the other hand, taking the colimit of the lines gives a diagram whose colimit is .
Hence using a Fubini-like theorem for colimits (that we havenÃ¢â¬â¢t proved) we have an equivalence . The proof of this Fubini theorem for colimits still requires the long and tedious computation, though. ∎
For any type , there is an equivalence .
It is easy to define the two maps back and forth and to prove that they are inverse to each other. The details are left as an exercise to the reader. ∎
We can now construct the Hopf fibration:
There is a fibration over of fiber and total space .
We proved that has a structure of H-space (cf \autoreflem:hspace-S1) hence by \autoreflem:hopf-construction there is a fibration over of fiber and total space . But by the two previous results and \autorefthm:suspbool we have:
|Title||8.5.3 The Hopf fibration|