# 8.5.2 The Hopf construction

###### Definition 8.5.1.

An H-space consists of

• a type $A$,

• $e:A$,

• $\mu:A\times A\to A$, and

• for every $a:A$, equalities $\mu(e,a)=a$ and $\mu(a,e)=a$.

###### Lemma 8.5.2.

Let $A$ be a connected H-space. Then for every $a:A$, the maps $\mu(a,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):A\to A$ and $\mu(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},a):A\to A$ are equivalences.

###### Proof.

Let us prove that for every $a:A$ the map $\mu(a,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ is an equivalence. The other statement is symmetric. The statement that $\mu(a,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ is an equivalence corresponds to a type family $P:A\to\mathsf{Prop}$ and proving it corresponds to finding a section of this type family.

The type $\mathsf{Prop}$ is a set (\autorefthm:hleveln-of-hlevelSn) hence we can define a new type family $P^{\prime}:\mathopen{}\left\|A\right\|_{0}\mathclose{}\to\mathsf{Prop}$ by $P^{\prime}(\mathopen{}\left|a\right|_{0}\mathclose{}):\!\!\equiv P(a)$. But $A$ is connected by assumption, hence $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ is contractible. This implies that in order to find a section of $P^{\prime}$, it is enough to find a point in the fiber of $P^{\prime}$ over $\mathopen{}\left|e\right|_{0}\mathclose{}$. But we have $P^{\prime}(\mathopen{}\left|e\right|_{0}\mathclose{})=P(e)$ which is inhabited because $\mu(e,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ is equal to the identity map by definition of an H-space, hence is an equivalence.

We have proved that for every $x:\mathopen{}\left\|A\right\|_{0}\mathclose{}$ the proposition $P^{\prime}(x)$ is true, hence in particular for every $a:A$ the proposition $P(a)$ is true because $P(a)$ is $P^{\prime}(\mathopen{}\left|a\right|_{0}\mathclose{})$. ∎

###### Definition 8.5.3.

Let $A$ be a connected H-space. We define a fibration over $\Sigma A$ using \autoreflem:fibration-over-pushout.

Given that $\Sigma A$ is the pushout $\mathbf{1}\sqcup^{A}\mathbf{1}$, we can define a fibration over $\Sigma A$ by specifying

• two fibrations over $\mathbf{1}$ (i.e. two types $F_{1}$ and $F_{2}$), and

• a family $e:A\to(F_{1}\simeq F_{2})$ of equivalences between $F_{1}$ and $F_{2}$, one for every element of $A$.

We take $A$ for $F_{1}$ and $F_{2}$, and for $a:A$ we take the equivalence $\mu(a,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ for $e(a)$.

According to \autoreflem:fibration-over-pushout, we have the following diagram:

 $\xymatrix{A\ar@{->>}[d]&A\times A\ar[l]_{-}{\mathsf{pr}_{2}}\ar@{->>}_{\mathsf% {pr}_{1}}[d]\ar[r]^{-}{\mu}&A\ar@{->>}[d]\\ 1&A\ar[r]\ar[l]&1}$

and the fibration we just constructed is a fibration over $\Sigma A$ whose total space is the pushout of the top line.

Moreover, with $f(x,y):\!\!\equiv(\mu(x,y),y)$ we have the following diagram:

 $\xymatrix{A\ar_{\mathsf{id}}{}_{d}&A\times A\ar[l]_{-}{\mathsf{pr}_{2}}\ar^{f}% [d]\ar[r]^{-}{\mu}&A\ar^{\mathsf{id}}_{d}\\ A&A\times A\ar^{-}{\mathsf{pr}_{2}}[l]\ar_{-}{\mathsf{pr}_{1}}[r]&A}$

The diagram commutes and the three vertical maps are equivalences, the inverse of $f$ being the function $g$ defined by

 $g(u,v):\!\!\equiv(\mathord{{\mu(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},v)% }^{-1}}(u),v).$

This shows that the two lines are equivalent (hence equal) spans, so the total space of the fibration we constructed is equivalent to the pushout of the bottom line. And by definition, this latter pushout is the join of $A$ with itself (see \autorefsec:colimits). We have proven:

###### Lemma 8.5.4.

Given a connected H-space $A$, there is a fibration, called the Hopf construction, over $\Sigma A$ with fiber $A$ and total space $A*A$.

Title 8.5.2 The Hopf construction
\metatable