8.5.3 The Hopf fibration

We will first construct a structureMathworldPlanetmath of H-spaceMathworldPlanetmath on the circle π•Š1, hence by \autoreflem:hopf-construction we will get a fibrationMathworldPlanetmath over π•Š2 with fiber π•Š1 and total space π•Š1*π•Š1. We will then prove that this join is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to π•Š3.

Lemma 8.5.1.

There is an H-space structure on the circle S1.


For the base point of the H-space structure we choose π–»π–Ίπ—Œπ–Ύ. Now we need to define the multiplication operationMathworldPlanetmath ΞΌ:π•Š1Γ—π•Š1β†’π•Š1. We will define the curried form ΞΌ~:π•Š1β†’(π•Š1β†’π•Š1) of ΞΌ by recursion on π•Š1:

ΞΌ~(π–»π–Ίπ—Œπ–Ύ):β‰‘π—‚π–½π•Š1,and  μ~(π—…π—ˆπ—ˆπ—‰):=π–Ώπ—Žπ—‡π–Ύπ—‘π—(h).

where h:∏(x:π•Š1)(x=x) is the function defined in \autorefthm:S1-autohtpy, which has the property that h(π–»π–Ίπ—Œπ–Ύ):β‰‘π—…π—ˆπ—ˆπ—‰.

Now we just have to prove that μ⁒(x,π–»π–Ίπ—Œπ–Ύ)=μ⁒(π–»π–Ίπ—Œπ–Ύ,x)=x for every x:π•Š1. By definition, if x:π•Š1 we have μ⁒(π–»π–Ίπ—Œπ–Ύ,x)=ΞΌ~⁒(π–»π–Ίπ—Œπ–Ύ)⁒(x)=π—‚π–½π•Š1⁒(x)=x. For the equality μ⁒(x,π–»π–Ίπ—Œπ–Ύ)=x we do it by inductionMathworldPlanetmath on x:π•Š1:

  • β€’

    If x is π–»π–Ίπ—Œπ–Ύ then μ⁒(π–»π–Ίπ—Œπ–Ύ,π–»π–Ίπ—Œπ–Ύ)=π–»π–Ίπ—Œπ–Ύ by definition, so we have π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ:μ⁒(π–»π–Ίπ—Œπ–Ύ,π–»π–Ίπ—Œπ–Ύ)=π–»π–Ίπ—Œπ–Ύ.

  • β€’

    When x varies along π—…π—ˆπ—ˆπ—‰, we need to prove that


    The left-hand side is equal to π—…π—ˆπ—ˆπ—‰, and for the right-hand side we have:

    𝖺𝗉λ⁒x.μ⁒(x,π–»π–Ίπ—Œπ–Ύ)⁒(π—…π—ˆπ—ˆπ—‰)⁒\centerdotβ’π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ =𝖺𝗉λ⁒x.(ΞΌ~⁒(x))⁒(π–»π–Ίπ—Œπ–Ύ)⁒(π—…π—ˆπ—ˆπ—‰)

Now recall from \autorefsec:colimits that the join A*B of types A and B is the pushout of the diagram

Lemma 8.5.2.

The operation of join is associative: if A, B and C are three types then we have an equivalence (A*B)*C≃A*(B*C).


We define a map f:(A*B)*Cβ†’A*(B*C) by induction. We first need to define fβˆ˜π—‚π—‡π—…:A*Bβ†’A*(B*C) which will be done by induction, then fβˆ˜π—‚π—‡π—‹:Cβ†’A*(B*C), and then 𝖺𝗉fβˆ˜π—€π—…π—Žπ–Ύ:∏(t:(A*B)Γ—C)f⁒(𝗂𝗇𝗅⁒(𝗉𝗋1⁒(t)))=f⁒(𝗂𝗇𝗋⁒(𝗉𝗋2⁒(t))) which will be done by induction on the first component of t:

(fβˆ˜π—‚π—‡π—…)(𝗂𝗇𝗅(a))) :≑𝗂𝗇𝗅(a),
(fβˆ˜π—‚π—‡π—…)(𝗂𝗇𝗋(b))) :≑𝗂𝗇𝗋(𝗂𝗇𝗅(b)),
𝖺𝗉fβˆ˜π—‚π—‡π—…β’(π—€π—…π—Žπ–Ύβ’(a,b)) :=π—€π—…π—Žπ–Ύβ’(a,𝗂𝗇𝗅⁒(b)),
f⁒(𝗂𝗇𝗋⁒(c)) :≑𝗂𝗇𝗋(𝗂𝗇𝗋(c)),
𝖺𝗉f⁒(π—€π—…π—Žπ–Ύβ’(𝗂𝗇𝗅⁒(a),c)) :=π—€π—…π—Žπ–Ύβ’(a,𝗂𝗇𝗋⁒(c)),
𝖺𝗉f⁒(π—€π—…π—Žπ–Ύβ’(𝗂𝗇𝗋⁒(b),c)) :=𝖺𝗉𝗂𝗇𝗋⁒(π—€π—…π—Žπ–Ύβ’(b,c)),
𝖺𝗉𝖽λ⁒x.𝖺𝗉f⁒(π—€π—…π—Žπ–Ύβ’(x,c))⁒(π—€π—…π—Žπ–Ύβ’(a,b)) :=`⁒`⁒𝖺𝗉𝖽λ⁒x.π—€π—…π—Žπ–Ύβ’(a,x)⁒(π—€π—…π—Žπ–Ύβ’(b,c))β€²β€².

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 g:A*(B*C)β†’(A*B)*C, and checking that f and g are inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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 (A*B)*C:


On the other hand, taking the colimit of the lines gives a diagram whose colimit is A*(B*C).

Hence using a Fubini-like theorem for colimits (that we havenÒ҂¬Ò„’t proved) we have an equivalence (A*B)*C≃A*(B*C). The proof of this Fubini theorem for colimits still requires the long and tedious computation, though. ∎

Lemma 8.5.3.

For any type A, there is an equivalence Σ⁒A≃2*A.


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:

Theorem 8.5.4.

There is a fibration over S2 of fiber S1 and total space S3.


We proved that π•Š1 has a structure of H-space (cf \autoreflem:hspace-S1) hence by \autoreflem:hopf-construction there is a fibration over π•Š2 of fiber π•Š1 and total space π•Š1*π•Š1. But by the two previous results and \autorefthm:suspbool we have:

Title 8.5.3 The Hopf fibration