natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
quaternionic projective line$\,\mathbb{H}P^1$
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
This entry is about homotopy groups of spheres formalized in homotopy type theory (HoTT).
The homotopy groups of spheres are a fundamental concept in algebraic topology and homotopy theory. They are the homotopy classes of maps between $n$-spheres, as $n$ varies. These may equivalently be understood as collection of different ways to attach spheres to each other. For instance, the homotopy type of a CW complex is completely determined by the homotopy types of the attaching maps.
The following is a quick reference for the state of the art on formalizing and computing homotopy groups of spheres in homotopy type theory.
n/k | 0 | 1 | 2 | 3 | 4 |
---|---|---|---|---|---|
0 | π_{0}(S^{0}) | π_{0}(S^{1}) | π_{0}(S^{2}) | π_{0}(S^{3}) | π_{0}(S^{4}) |
1 | π_{1}(S^{0}) | π_{1}(S^{1}) | π_{1}(S^{2}) | π_{1}(S^{3}) | π_{1}(S^{4}) |
2 | π_{2}(S^{0}) | π_{2}(S^{1}) | π_{2}(S^{2}) | π_{2}(S^{3}) | π_{2}(S^{4}) |
3 | π_{3}(S^{0}) | π_{3}(S^{1}) | π_{3}(S^{2}) | π_{3}(S^{3}) | π_{3}(S^{4}) |
4 | π_{4}(S^{0}) | π_{4}(S^{1}) | π_{4}(S^{2}) | π_{4}(S^{3}) | π_{4}(S^{4}) |
The following is a list of results for which at least one proof has been formalized in HoTT.
See also at first stable homotopy group of spheres.
Peter LeFanu Lumsdaine has constructed the Hopf fibration as a dependent type. Lots of people around know the construction, but I don’t know anywhere it’s written up. Here’s some Agda code with it in it.
Brunerie 2016, proof that the total space of the Hopf fibration is $S^3$, together with $\pi_n(S^n)$, imply this by a long-exact-sequence argument.
This was formalized in Lean in 2016.
See also at second stable homotopy group of spheres.
Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \le 2n - 2$
See also at Hopf degree theorem.
Mike Shulman‘s proof by contractibility of total space of universal cover (HoTT blog).
Dan Licata‘s encode/decode-style proof (HoTT blog). A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.
Guillaume Brunerie‘s proof using the flattening lemma.
See also at circle type for more.
Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory $[$arxiv:1606.05916$]$
Axel Ljungström, The Brunerie Number Is -2 (June 2022) $[$blog entry$]$
Last revised on June 15, 2022 at 12:54:07. See the history of this page for a list of all contributions to it.