Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910427713110016 |
|---|---|
| author | Ljungström, Axel Mörtberg, Anders |
| author_facet | Ljungström, Axel Mörtberg, Anders |
| contents | Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is $\mathbb{Z}/2\mathbb{Z}$. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses a lot of advanced classical algebraic topology rephrased synthetically. Furthermore, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" $β$ can be normalised to $\pm 2$. The question of whether Brunerie's proof could be formalised in a proof assistant, either by computing this number or by formalising the pen-and-paper proof, has since remained open. In this paper, we present a complete formalisation in Cubical Agda. We do this by modifying Brunerie's proof so that a key technical result, whose proof Brunerie only sketched in his thesis, can be avoided. We also present a formalisation of a new and much simpler proof that $β$ is $\pm 2$. This formalisation provides us with a sequence of simpler Brunerie numbers, one of which normalises very quickly to $-2$ in Cubical Agda, resulting in a fully formalised computer-assisted proof that $π_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_00151 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda Ljungström, Axel Mörtberg, Anders Algebraic Topology Logic in Computer Science Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is $\mathbb{Z}/2\mathbb{Z}$. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses a lot of advanced classical algebraic topology rephrased synthetically. Furthermore, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" $β$ can be normalised to $\pm 2$. The question of whether Brunerie's proof could be formalised in a proof assistant, either by computing this number or by formalising the pen-and-paper proof, has since remained open. In this paper, we present a complete formalisation in Cubical Agda. We do this by modifying Brunerie's proof so that a key technical result, whose proof Brunerie only sketched in his thesis, can be avoided. We also present a formalisation of a new and much simpler proof that $β$ is $\pm 2$. This formalisation provides us with a sequence of simpler Brunerie numbers, one of which normalises very quickly to $-2$ in Cubical Agda, resulting in a fully formalised computer-assisted proof that $π_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$. |
| title | Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda |
| topic | Algebraic Topology Logic in Computer Science |
| url | https://arxiv.org/abs/2302.00151 |