# 8.5.3 The Hopf fibration

We will first construct a structure of H-space on the circle $\mathbb{S}^{1}$, hence by \autoreflem:hopf-construction we will get a fibration over $\mathbb{S}^{2}$ with fiber $\mathbb{S}^{1}$ and total space $\mathbb{S}^{1}*\mathbb{S}^{1}$. We will then prove that this join is equivalent to $\mathbb{S}^{3}$.

###### Lemma 8.5.1.

There is an H-space structure on the circle $\mathbb{S}^{1}$.

###### Proof.

For the base point of the H-space structure we choose $\mathsf{base}$. Now we need to define the multiplication operation $\mu:\mathbb{S}^{1}\times\mathbb{S}^{1}\to\mathbb{S}^{1}$. We will define the curried form $\widetilde{\mu}:\mathbb{S}^{1}\to(\mathbb{S}^{1}\to\mathbb{S}^{1})$ of $\mu$ by recursion on $\mathbb{S}^{1}$:

 $\widetilde{\mu}(\mathsf{base}):\!\!\equiv\mathsf{id}_{\mathbb{S}^{1}},\qquad% \text{and}\qquad{\widetilde{\mu}}\mathopen{}\left({\mathsf{loop}}\right)% \mathclose{}:=\mathsf{funext}(h).$

where $h:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}(x=x)$ is the function defined in \autorefthm:S1-autohtpy, which has the property that $h(\mathsf{base}):\!\!\equiv\mathsf{loop}$.

Now we just have to prove that $\mu(x,\mathsf{base})=\mu(\mathsf{base},x)=x$ for every $x:\mathbb{S}^{1}$. By definition, if $x:\mathbb{S}^{1}$ we have $\mu(\mathsf{base},x)=\widetilde{\mu}(\mathsf{base})(x)=\mathsf{id}_{\mathbb{S}% ^{1}}(x)=x$. For the equality $\mu(x,\mathsf{base})=x$ we do it by induction on $x:\mathbb{S}^{1}$:

• If $x$ is $\mathsf{base}$ then $\mu(\mathsf{base},\mathsf{base})=\mathsf{base}$ by definition, so we have $\mathsf{refl}_{\mathsf{base}}:\mu(\mathsf{base},\mathsf{base})=\mathsf{base}$.

• When $x$ varies along $\mathsf{loop}$, we need to prove that

 $\mathsf{refl}_{\mathsf{base}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{{\lambda}x.\,x}({% \mathsf{loop}})=\mathsf{ap}_{{\lambda}x.\,\mu(x,\mathsf{base})}({\mathsf{loop}% })\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin% {\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{refl}_{\mathsf{base}}.$

The left-hand side is equal to $\mathsf{loop}$, and for the right-hand side we have:

 $\displaystyle\mathsf{ap}_{{\lambda}x.\,\mu(x,\mathsf{base})}({\mathsf{loop}})% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{refl}_{\mathsf{base}}$ $\displaystyle=\mathsf{ap}_{{\lambda}x.\,(\widetilde{\mu}(x))(\mathsf{base})}({% \mathsf{loop}})$ $\displaystyle=\mathsf{happly}(\mathsf{ap}_{{\lambda}x.\,(\widetilde{\mu}(x))}(% {\mathsf{loop}}),\mathsf{base})$ $\displaystyle=\mathsf{happly}(\mathsf{funext}(h),\mathsf{base})$ $\displaystyle=h(\mathsf{base})$ $\displaystyle=\mathsf{loop}.\qed$

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

 $A\xleftarrow{\mathsf{pr}_{1}}A\times B\xrightarrow{\mathsf{pr}_{2}}B.$
###### 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\simeq A*(B*C)$.

###### Proof.

We define a map $f:(A*B)*C\to A*(B*C)$ by induction. We first need to define $f\circ{\mathsf{inl}}:A*B\to A*(B*C)$ which will be done by induction, then $f\circ{\mathsf{inr}}:C\to A*(B*C)$, and then $\mathsf{ap}_{f}\circ\mathsf{glue}:\mathchoice{\prod_{t:(A*B)\times C}\,}{% \mathchoice{{\textstyle\prod_{(t:(A*B)\times C)}}}{\prod_{(t:(A*B)\times C)}}{% \prod_{(t:(A*B)\times C)}}{\prod_{(t:(A*B)\times C)}}}{\mathchoice{{\textstyle% \prod_{(t:(A*B)\times C)}}}{\prod_{(t:(A*B)\times C)}}{\prod_{(t:(A*B)\times C% )}}{\prod_{(t:(A*B)\times C)}}}{\mathchoice{{\textstyle\prod_{(t:(A*B)\times C% )}}}{\prod_{(t:(A*B)\times C)}}{\prod_{(t:(A*B)\times C)}}{\prod_{(t:(A*B)% \times C)}}}f({\mathsf{inl}}(\mathsf{pr}_{1}(t)))=f({\mathsf{inr}}(\mathsf{pr}% _{2}(t)))$ which will be done by induction on the first component of $t$:

 $\displaystyle(f\circ{\mathsf{inl}})({\mathsf{inl}}(a)))$ $\displaystyle:\!\!\equiv{\mathsf{inl}}(a),$ $\displaystyle(f\circ{\mathsf{inl}})({\mathsf{inr}}(b)))$ $\displaystyle:\!\!\equiv{\mathsf{inr}}({\mathsf{inl}}(b)),$ $\displaystyle\mathsf{ap}_{f\circ{\mathsf{inl}}}(\mathsf{glue}(a,b))$ $\displaystyle:=\mathsf{glue}(a,{\mathsf{inl}}(b)),$ $\displaystyle f({\mathsf{inr}}(c))$ $\displaystyle:\!\!\equiv{\mathsf{inr}}({\mathsf{inr}}(c)),$ $\displaystyle\mathsf{ap}_{f}(\mathsf{glue}({\mathsf{inl}}(a),c))$ $\displaystyle:=\mathsf{glue}(a,{\mathsf{inr}}(c)),$ $\displaystyle\mathsf{ap}_{f}(\mathsf{glue}({\mathsf{inr}}(b),c))$ $\displaystyle:=\mathsf{ap}_{{\mathsf{inr}}}(\mathsf{glue}(b,c)),$ $\displaystyle\mathsf{apd}_{{\lambda}x.\,\mathsf{ap}_{f}(\mathsf{glue}(x,c))}(% \mathsf{glue}(a,b))$ $\displaystyle:=\mathsf{apd}_{{\lambda}x.\,\mathsf{glue}(a,x)}(\mathsf{glue}(% b,c))^{\prime\prime}.$

For the last equation, note that the right-hand side is of type

 $\mathsf{transport}^{{\lambda}x.\,{\mathsf{inl}}(a)={\mathsf{inr}}(x)}(\mathsf{% glue}(b,c),\mathsf{glue}(a,{\mathsf{inl}}(b)))=\mathsf{glue}(a,{\mathsf{inr}}(% c))$

whereas it is supposed to be of type

 $\mathsf{transport}^{{\lambda}x.\,f({\mathsf{inl}}(x))=f({\mathsf{inr}}(c))}(% \mathsf{glue}(a,b),\mathsf{ap}_{f}(\mathsf{glue}({\mathsf{inl}}(a),c)))=% \mathsf{ap}_{f}(\mathsf{glue}({\mathsf{inr}}(b),c)).$

But by the previous clauses in the definition, both of these types are equivalent to the following type:

 $\mathsf{glue}(a,{\mathsf{inr}}(c))=\mathsf{glue}(a,{\mathsf{inl}}(b))% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{ap}_{{\mathsf{inr}}}(\mathsf{glue}(b,c)),$

and so we can coerce by an equivalence to obtain the necessary element. Similarly, we can define a map $g:A*(B*C)\to(A*B)*C$, and checking that $f$ and $g$ are inverse to each other is a long and tedious but essentially straightforward computation. ∎

A more conceptual proof sketch is as follows.

###### Proof.

Let us consider the following diagram where the maps are the obvious projections:

 $\xymatrix{A&A\times C\ar[l]\ar[r]&A\times C\\ A\times B\ar[u]\ar[d]&A\times B\times C\ar[l]\ar[u]\ar[r]\ar[d]&A\times C\ar[u% ]\ar[d]\\ B&B\times C\ar[l]\ar[r]&C}$

Taking the colimit of the columns gives the following diagram, whose colimit is $(A*B)*C$:

 $\xymatrix{A*B&(A*B)\times C\ar[l]\ar[r]&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\simeq 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 $\Sigma A\simeq\mathbf{2}*A$.

###### Proof.

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 $\mathbb{S}^{2}$ of fiber $\mathbb{S}^{1}$ and total space $\mathbb{S}^{3}$.

###### Proof.

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

 $\mathbb{S}^{1}*\mathbb{S}^{1}=(\Sigma\mathbf{2})*\mathbb{S}^{1}=(\mathbf{2}*% \mathbf{2})*\mathbb{S}^{1}=\mathbf{2}*(\mathbf{2}*\mathbb{S}^{1})=\Sigma(% \Sigma\mathbb{S}^{1})=\mathbb{S}^{3}.\qed$
Title 8.5.3 The Hopf fibration
\metatable