On the homotopy groups of spheres in homotopy type theory

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<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$.

PhD thesis, 187 pages, summary in French at the end

References in corpus (2)

• Higher Topos Theory
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

Cited by in corpus (13)

• Quotient inductive-inductive types
• An introduction to univalent foundations for mathematicians
• All $(\infty ,1)$-toposes have strict univalent universes
• Models of Type Theory with Strict Equality
• Computational Higher Type Theory IV: Inductive Types
• Formalization of the fundamental group in untyped set theory using auto2
• Synthetic Homology in Homotopy Type Theory
• Globular weak $\omega$-categories as models of a type theory
• Synthetic Spectra via a Monadic and Comonadic Modality
• Coherence of strict equalities in dependent type theories
• From dependent type theory to higher algebraic structures
• Cost-Aware Type Theory
• Hom weak $\omega$-categories of a weak $\omega$-category