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