8.6 The Freudenthal suspension theorem
Before proving the Freudenthal suspension theorem, we need some auxiliary lemmas about connectedness. In \autorefcha:hlevels we proved a number of facts about -connected maps and -types for fixed ; here we are now interested in what happens when we vary . For instance, in \autorefprop:nconnected_tested_by_lv_n_dependent types we showed that -connected maps are characterized by an “induction principle” relative to families of -types. If we want to “induct along” an -connected map into a family of -types for , we don’t immediately know that there is a function by such an induction principle, but the following lemma says that at least our ignorance can be quantified.
If is -connected and is a family of -types for , then the induced function
We induct on the natural number . When , this is \autorefprop:nconnected_tested_by_lv_n_dependent types. For the inductive step, suppose is -connected and is a family of -types. To show that is -truncated, let ; then we have
Let and lie in this type, so and ; then we also have
However, here the right-hand side is a fiber of the map
Recall that if and are pointed types, then their wedge is defined to be the pushout of . There is a canonical map defined by the two maps and ; the following lemma essentially says that this map is highly connected if and are so. It is a bit more convenient both to prove and use, however, if we use the characterization of connectedness from \autorefprop:nconnected_tested_by_lv_n_dependent types and substitute in the universal property of the wedge (generalized to type families).
Lemma 8.6.2 (Wedge connectivity lemma).
Suppose that and are - and -connected pointed types, respectively, with , and let Then for any and with , there exists with homotopies
such that .
Then we have . Since is -connected, if is a family of -types then we will have such that , in which case we can define . However, for fixed , the type is the fiber over of the map
given by precomposition with . Since is -connected, for this fiber to be -connected, by \autorefthm:conn-trunc-variable-ind it suffices for each type to be an -type, which we have assumed. ∎
Let be a pointed type, and recall the definition of the suspension from \autorefsec:suspension, with constructors and . We regard as a pointed space with basepoint , so that we have . Then there is a canonical map
In classical algebraic topology, one considers the reduced suspension, in which the path is collapsed down to a point, identifying and . The reduced and unreduced suspensions are homotopy equivalent, so the distinction is invisible to our purely homotopy-theoretic eyes — and higher inductive types only allow us to “identify” points up to a higher path anyway, there is no purpose to considering reduced suspensions in homotopy type theory. However, the “unreducedness” of our suspension is the reason for the (possibly unexpected) appearance of in the definition of .
Our goal is now to prove the following.
Theorem 8.6.4 (The Freudenthal suspension theorem).
Suppose that is -connected and pointed, with . Then the map is -connected.
We will use the encode-decode method, but applied in a slightly different way. In most cases so far, we have used it to characterize the loop space of some type as equivalent to some other type , by constructing a family with and a family of equivalences .
In this case, however, we want to show that is -connected. We could use a truncated version of the previous method, such as we will see in \autorefsec:van-kampen, to prove that is an equivalence—but this is a slightly weaker statement than the map being -connected (see \autorefthm:conn-pik,\autorefthm:pik-conn). However, note that in the general case, to prove that is an equivalence, we could equivalently be proving that its fibers are contractible, and we would still be able to use induction over the base type. This we can generalize to prove connectedness of a map into a loop space, i.e. that the truncations of its fibers are contractible. Moreover, instead of constructing and separately, we can construct directly a family of codes for the truncations of the fibers.
If is -connected and pointed with , then there is a family
Our eventual goal will be to prove that is contractible for all and . Applying this with will show that all fibers of are -connected, and thus is -connected.
Proof of \autorefthm:freudcode.
By \autorefthm:dpath-arrow, this is equivalent to giving a family of paths
And by univalence and transport in path types, this is equivalent to a family of equivalences
We will define a family of maps
and then show that they are all equivalences. Thus, let ; by the universal property of truncation and the definitions of and , it will suffice to define for each , a map
Now for each , this type is -truncated, while is -connected. Thus, by \autorefthm:wedge-connectivity, it suffices to define this map when is , when is , and check that they agree when both are .
When is , the hypothesis is . Thus, by canceling from to get , so we can define the image to be .
When is , the hypothesis is . Rearranging this, we obtain , and we can define the image to be .
Finally, when both and are , it suffices to show the resulting and agree; this is an easy lemma about path composition. This completes the definition of (8.6.7). To show that it is a family of equivalences, since being an equivalence is a mere proposition and is (at least) -connected, it suffices to assume is . In this case, inspecting the above construction we see that it is essentially the -truncation of the function that cancels , which is an equivalence. ∎
Let , , and , and also with and . Then the function
where is the obvious coherence path and is the uncurried form of , is equal to the equivalence obtained by univalence from the composite
By path induction, we may assume is and is , in which case both functions are the identity. ∎
We apply this lemma with and and , while and and for some , and finally is some path . The computation rule for induction over identifies with a path constructed in a certain way out of univalence and function extensionality. The second function described in \autorefthm:freudlemma essentially consists of undoing these applications of univalence and function extensionality, reducing back to the particular functions (8.6.7) that we defined using \autorefthm:wedge-connectivity. Therefore, \autorefthm:freudlemma says that transporting along essentially recovers these functions.
Finally, by construction, when or coincides with and the input is in the image of , we know more explicitly what these functions are. Thus, for any , we have
where is arbitrary as before, and is obtained from by identifying its end point with and canceling . Similarly, for any , we have
where , and is obtained by identifying its end point and rearranging paths.
Proof of \autorefthm:freudenthal.
It remains to show that is contractible for each and . First we must choose a center of contraction, say . This corresponds to the definition of the function in our previous proofs, so we define it by transport. Note that in the special case when is and is , we have
Thus, we can choose , where is the obvious path for any . We can now obtain by path induction on , but it will be important below that we can also give a concrete definition in terms of transport:
where is the uncurried version of , and is a standard lemma.
Next, we must show that every element of is equal to . Again, by path induction, it suffices to assume is and is . In fact, we will prove it more generally when is and is arbitrary. That is, we will show that for any and we have . Since this equality is a -type, we may assume is of the form for some and .
Now by a further path induction, we may assume that is reflexivity, and is . (This is why we generalized to arbitrary above.) Thus, we have to prove that
By definition, the right-hand side of this equality is
where the underscore ought to be filled in with suitable coherence paths. Here the first step is functoriality of transport, the second invokes (8.6.10), and the third invokes (8.6.9) (with transport moved to the other side). Thus we have the same first component as the left-hand side of (8.6.11). We leave it to the reader to verify that the coherence paths all cancel, giving reflexivity in the second component. ∎
Corollary 8.6.12 (Freudenthal Equivalence).
Suppose that is -connected and pointed, with . Then .
By \crefthm:freudenthal, is -connected. By \creflem:connected-map-equiv-truncation, it is therefore an equivalence on -truncations. ∎
One important corollary of the Freudenthal suspension theorem is that the homotopy groups of spheres are stable in a certain range (these are the northeast-to-southwest diagonals in \autoreftab:homotopy-groups-of-spheres):
Corollary 8.6.13 (Stability for Spheres).
If , then .
Assume . By \crefcor:sn-connected, is -connected. Therefore, by \crefcor:freudenthal-equiv,
By \creflem:truncation-le, because , applying to both sides shows that this equation holds for :
Then, the main idea of the proof is as follows; we omit checking that these equivalences act appropriately on the base points of these spaces:
This means that once we have calculated one entry in one of these stable diagonals, we know all of them. For example:
for every .
The proof is by induction on . We already have (\autorefcor:pi1s1) and (\autorefcor:pis2-hopf). When , . Therefore, by \crefcor:stability-spheres, , and this equivalence, combined with the inductive hypothesis, gives the result. ∎
is not an -type for any .
|Title||8.6 The Freudenthal suspension theorem|