_On the homotopy groups of spheres in homotopy type theory_, [[Guillaume Brunerie]], ## Links ## [arxiv](https://arxiv.org/abs/1606.05916) ## Abstract ## The goal of this thesis is to prove that $\pi_4(S^3)\simeq \mathbb{Z}/2\mathbb{Z}$ in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the [[homotopy groups of spheres]]: the computation of the homotopy groups of the [[circle]], the triviality of those of the form $\pi_k(S^n)$ with $k\lt n$, and the construction of the [[Hopf fibration]]. We then move to more advanced tools. In particular, we define the [[James construction]] which allows us to prove the [[Freudenthal suspension theorem]] and the fact that there exists a natural number $n$ such that $\pi_4(S^3)\simeq\mathbb{Z}/n\mathbb{Z}$. Then we study the [[smash product]] of spheres, we construct the [[cohomology]] ring of a space, and we introduce the [[Hopf invariant]], allowing us to narrow down the $n$ to either $1$ or $2$. The Hopf invariant also allows us to prove that all the [[groups]] of the form ${\pi_{4n-1}}(S^{2n})$ are infinite. Finally we construct the [[Gysin exact sequence]], allowing us to compute the [[cohomology]] of $\mathbb{C}P^2$ and to prove that $\pi_4(S^3)\simeq \mathbb{Z}/2\mathbb{Z}$ and that more generally $\pi_{n+1}(S^n)\simeq \mathbb{Z}/2\mathbb{Z}$ for every $n\ge 3$. category: reference