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 isequivalent 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 wehave $\\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 typesthen 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 thefirst 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 essentiallystraightforward computation.∎

A more conceptual proof sketch is as follows.

Proof.

Let us consider the following diagram where the maps are the obviousprojections:

\\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 followingdiagram, 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 whosecolimit is $A*(B*C)$ .

Hence using a Fubini-like theorem for colimits (that we havenÃ¢â¬â¢t proved) wehave an equivalence $(A*B)*C\\simeq A*(B*C)$ . The proof of this Fubini theoremfor 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 areinverse 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}$ offiber $\\mathbb{S}^{1}$ and total space $\\mathbb{S}^{1}*\\mathbb{S}^{1}$ . But by the two previous resultsand \\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