8.5.2 The Hopf construction

Definition 8.5.1.

An H-space consists of

  • a type A,

  • a base point e:A,

  • a binary operationMathworldPlanetmath μ:A×AA, and

  • for every a:A, equalities μ(e,a)=a and μ(a,e)=a.

Lemma 8.5.2.

Let A be a connected H-space. Then for every a:A, the maps μ(a,):AA and μ(,a):AA are equivalences.


Let us prove that for every a:A the map μ(a,) is an equivalence. The other statement is symmetricMathworldPlanetmathPlanetmathPlanetmath. The statement that μ(a,) is an equivalence corresponds to a type family P:A𝖯𝗋𝗈𝗉 and proving it corresponds to finding a sectionMathworldPlanetmath of this type family.

The type 𝖯𝗋𝗈𝗉 is a set (\autorefthm:hleveln-of-hlevelSn) hence we can define a new type family P:A0𝖯𝗋𝗈𝗉 by P(|a|0):P(a). But A is connected by assumptionPlanetmathPlanetmath, hence A0 is contractible. This implies that in order to find a section of P, it is enough to find a point in the fiber of P over |e|0. But we have P(|e|0)=P(e) which is inhabited because μ(e,) is equal to the identity mapMathworldPlanetmath by definition of an H-space, hence is an equivalence.

We have proved that for every x:A0 the propositionPlanetmathPlanetmathPlanetmath P(x) is true, hence in particular for every a:A the proposition P(a) is true because P(a) is P(|a|0). ∎

Definition 8.5.3.

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

Given that ΣA is the pushout 1A1, we can define a fibration over ΣA by specifying

  • two fibrations over 𝟏 (i.e. two types F1 and F2), and

  • a family e:A(F1F2) of equivalences between F1 and F2, one for every element of A.

We take A for F1 and F2, and for a:A we take the equivalence μ(a,) for e(a).

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


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

Moreover, with f(x,y):(μ(x,y),y) we have the following diagram:


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


This shows that the two lines are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath (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 ΣA with fiber A and total space A*A.

Title 8.5.2 The Hopf construction