8.10 Additional Results

Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory.

Theorem 8.10.1.

There exists a k such that for all n3, πn+1(Sn)=Zk.

Notes on the proof..

The proof consists of a calculation of π4(𝕊3), together with an appeal to stability (\crefcor:stability-spheres). In the classical statement of this result, k is 2. While we have not yet checked that k is in fact 2, our calcluation of π4(𝕊3) is constructive, like all the rest of the proofs in this chapter. (More precisely, it doesn’t use any additional axioms such as 𝖫𝖤𝖬 or 𝖠𝖢, making it as constructive as univalence and higher inductive types are.) Thus, given a computational interpretationMathworldPlanetmathPlanetmath of homotopy type theory, we could run the proof on a computer to verify that k is 2. This example is quite intriguing, because it is the first calculation of a homotopy groupMathworldPlanetmath for which we have not needed to know the answer in advance. ∎

Theorem 8.10.2 (Blakers–Massey theorem).

Suppose we are given maps f:CX, and g:CY. Taking first the pushout XCY of f and g and then the pullback of its inclusions inl:XXCYY:inr, we have an induced map CX×(XCY)Y.

If f is i-connected and g is j-connected, then this induced map is (i+j)-connected. In other words, for any points x:X, y:Y, the corresponding fiber Cx,y of (f,g):CX×Y gives an approximation to the path space inl(x)=XCYinr(y) in the pushout.

It should be noted that in classical algebraic topology, the Blakers–Massey theorem is often stated in a somewhat different form, where the maps f and g are replaced by inclusions of subcomplexes of CW complexes, and the homotopyMathworldPlanetmathPlanetmath pushout and homotopy pullback by a union and intersectionMathworldPlanetmath, respectively. In order to express the theorem in homotopy type theory, we have to replace notions of this sort with ones that are homotopy-invariant. We have seen another example of this in the van Kampen theoremMathworldPlanetmath (\autorefsec:van-kampen), where we had to replace a union of open subsets by a homotopy pushout.

Theorem 8.10.3 (Eilenberg–Mac Lane Spaces).

For any abelian groupMathworldPlanetmath G and positive integer n, there is an n-type K(G,n) such that πn(K(G,n))=G, and πk(K(G,n))=0 for kn.

Theorem 8.10.4 (Covering spaces).

For a connected space A, there is an equivalence between covering spaces over A and sets with an action of π1(A).

Title 8.10 Additional Results