8.5.2 The Hopf construction
Let be a connected H-space. Then for every , the maps and are equivalences.
Let us prove that for every the map is an equivalence. The other statement is symmetric. The statement that is an equivalence corresponds to a type family and proving it corresponds to finding a section of this type family.
The type is a set (\autorefthm:hleveln-of-hlevelSn) hence we can define a new type family by . But is connected by assumption, hence is contractible. This implies that in order to find a section of , it is enough to find a point in the fiber of over . But we have which is inhabited because is equal to the identity map by definition of an H-space, hence is an equivalence.
We have proved that for every the proposition is true, hence in particular for every the proposition is true because is . ∎
Let be a connected H-space. We define a fibration over using \autoreflem:fibration-over-pushout.
Given that is the pushout , we can define a fibration over by specifying
two fibrations over (i.e. two types and ), and
a family of equivalences between and , one for every element of .
We take for and , and for we take the equivalence for .
According to \autoreflem:fibration-over-pushout, we have the following diagram:
and the fibration we just constructed is a fibration over whose total space is the pushout of the top line.
Moreover, with we have the following diagram:
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 with itself (see \autorefsec:colimits). We have proven:
Given a connected H-space , there is a fibration, called the Hopf construction, over with fiber and total space .
|Title||8.5.2 The Hopf construction|