Axel Ljungström: A Cubical Formalisation of Cohomology Theory and $\pi_4(S^3)$ = Z/2Z
Time: Tue 2023-05-16 13.00 - 14.00
Location: Classroom 29, Albano campus, house 4, floor 2
Doctoral student: Axel Ljungström
Opponent: Eric Finster
Supervisor: Anders Mörtberg
Examiner: Alexander Berglund
Abstract
The primary goal of this thesis is to provide a computer formalisation on the main result of Guillaume Brunerie's 2016 PhD thesis, namely that $\pi_4(S^3)$ = Z/2Z in Homotopy Type Theory (HoTT). The formalisation is carried out in Cubical Agda, an extension of the Agda proof assistant based on cubical type theory.
The thesis consists of two papers. In the first paper, we provide a formalisation of integral cohomology theory in Cubical Agda. This includes many fundamental constructions crucially used in Brunerie's proof. In particular, we provide a novel construction of the cup product in HoTT which both avoids smash products and is easier to work with. This allows us to provide the first complete construction and formalisation of the fact that the cup product satisfies the graded-commutative ring laws. We also compute the cohomology groups of some simple spaces. While the proofs of the main results in this paper are often easy to translate into standard HoTT, all constructions are carefully chosen to exhibit optimal computational behaviour in Cubical Agda.
The second paper is a summary of three formalisations of \(\pi_4(S^3) = \mathbb{Z}/2\mathbb{Z}\). The primary formalisation follows Brunerie's thesis closely but diverges in some details. In particular, we only work with a special case of the so called James construction, providing direct proofs of the relevant theorems. We also completely avoid the smash product by using the cohomology theory of the first paper. In addition, we present two new formalisations of the main result. In these, we circumvent the second half of Brunerie's thesis by providing direct computations of the so called Brunerie number, i.e. the number β such that \(\pi_4(S^3) = \mathbb{Z}/β\mathbb{Z}\), as defined in the first half of Brunerie's thesis. The first of these formalisations uses a new direct proof of the fact that β = -2. In the second one, we attempt to show that \(β = \pm 2\) by simply normalising it in Cubical Agda. While this normalisation still fails to terminate (in reasonable time), we can, by following the proof strategy in the second formalisation, rewrite β until we arrive at a definition which actually normalises.