Since being introduced to HoTT around 3 years ago, I have, like so many others before me, developed a healthy(?) obsession with the Brunerie number (i.e. the number such that , as defined in Guillaume Brunerie’s PhD thesis). Over the last year, I have, under the supervision of Anders Mörtberg, been working on the formalisation of in Cubical Agda. With some smaller alterations to Brunerie’s original proof, this formalisation was completed a few months ago. Although I was very happy with this achievement, one thing was still bothering me: I still felt like I didn’t really understand the Brunerie number.
To explain what I mean by this, let me first explain the structure of Brunerie’s original proof. In chapters 1–3, Brunerie uses the Blakers-Massey theorem and the James construction to construct his (in)famous number. In some more detail, he constructs a map such that the image of under the equivalence satisfies . I’ll refer to the map as the Brunerie map from now on (its definition will have to wait). Chapter 3 ends with the following remark:
This result is quite remarkable in that even though it is a constructive proof, it is not at all obvious how to actually compute this n. At the time of writing, we still haven’t managed to extract its value from its definition.
Brunerie then continues to develop high level machinery such as cohomology rings, the Gysin sequence, the Hopf invariant and, another 3 chapters later, manages to conclude that . This is all incredibly impressive, and, naturally, it’s great to see that we can actually rephrase so many classical results in HoTT. Undoubtedly, the argument shows why the equivalence takes the Brunerie map to , but it doesn’t really tell us (explicitly) how this happens.
This was my frustration with the Brunerie number: no matter how carefully I read Brunerie’s proof of , I didn’t feel like I got a better understanding of what the equivalence actually did to the elements you fed it. Surely, we should be able to ‘extract’ the value of by simply plugging in the Brunerie map and tracing it, step by step, down to ; after all, both the Brunerie map and the (inverse of the) equivalence have very concrete definitions. I have made such bold claims before, and almost without exception, I’ve had to admit defeat. But for once, I actually have something to back up my claims: there is a direct way to prove that the Brunerie number is — in fact, with this proof, it is .
The idea of the proof is to construct a sequence of new Brunerie maps — elements of other homotopy groups which the equivalence factors through. One then goes on to show that under the equivalence in question. The neat thing here is that the sequence gives rise to a sequence of new definitions of the Brunerie number, in decreasing level of ‘complexity’. The numbers corresponding to (the original definition of the Brunerie number), and are still too heavy for Cubical Agda to handle, but (an optimised version of) normalises to ! But don’t worry: the proof is equally straightforward without relying on normalisation, and in this post I’ll write it down in plain Book HoTT. Let’s get on with it.
We’ll need the following higher inductive types:
- We’ll need . We define it using the standard construction:
- We’ll need suspensions too. We define the suspension of a type using the following constructors:
- Finally, we’ll need joins. We define the join using the following constructors:
We define the -sphere by -fold suspension of , i.e. . We take to be pointed by and higher spheres to be pointed by . Another type of interest, , will be taken to be pointed by . Given a pointed type , we define its th homotopy group by , i.e. the set truncated type of pointed functions from to . We will use to denote addition on and to denote inversion on arbitrary -spheres. Finally, we will use for the canonical function (where is pointed). Recall, it is defined by
The fact that there is an equivalence is a well-known fact in HoTT; the equivalence appears in the very definition of the Brunerie number. Unfortunately, the easiest construction of the equivalence is rather indirect, which makes it hard to reason about. Therefore, our first goal is to get a better idea of what it looks like. For this, we’ll first need the obvious map . In HoTT, we can define it by and
The name is suggestive – it satisfies most properties that you’d expect from a ‘cup product’ (in fact it induces a ‘true’ cup product via the map ). It satisfies the following properties, all provable by circle induction:
This product induces an equivalence by
That’s a really cute function! Its inverse isn’t, but let’s not bother with that now.
The reason the Brunerie map is so hard to analyse is because it is defined as the precomposition of a nice map with a not so nice map, namely . However, what if we defined instead? Clearly, this definition is equivalent to the usual one by precomposition with . This would allow us redefine the Brunerie map to be simply and ignore that annoying precomposition with . Let’s make this happen.
For a pointed type , let us define
We can give this group an explicit multiplication. Given a function , we get an induced map defined by
Looks horrible! Fortunately, the above tends to be equal to when is reasonable. The multiplication of two maps and in is induced by the composition .
It is relatively straightforward (at least if one assumes that is -connected) to show that induces a group isomorphism . This is the key to understanding .
Now we’re ready to tackle the problem at hand. Recall that we have an equivalence . In the first 3 chapters of Brunerie’s thesis, he shows that where and where is the Brunerie map . It’s probably time to define . We’ll first need to actually define the aforementioned map . We define it by:
The map is then just defined by .
Note that the choice of equivalence does not matter — any two differ at most by a sign. Our job will therefore now be to construct a suitable equivalence and trace under it. We will see that when we land in , will have been mapped to , establishing that the Brunerie number (well, our definition of it) is . We achieve this by defining as a composition of 4 group isomorphisms and simultaneously tracing step by step.
This is defined by precomposition with . By definition, gets mapped to .
I have not been able to come up with a concrete definition of the map — it comes from the long exact sequence of homotopy groups induced from the Hopf fibration. Fortunately, however, its inverse is easy to describe: it is simply postcomposition with the Hopf map . The Hopf map is defined as follows:
Let’s construct the element such that . It is defined as follows:
This looks pretty ad hoc, but the construction is chosen carefully. In order to show , we show . For this, we need to show that . I won’t do this here, but the proof is very direct. The idea is that the terms in the -case are chosen precisely to take care of the appearing in the definition of the Hopf map.
This is where our construction of kicks in. The isomorphism is defined by postcomposition with . Let’s define . It is defined by
I claim that . To prove this, we need to show that . Let’s consider the definition of (modulo some light rewriting):
So, and agree definitionally on point constructors, and the push case is immediate by the properties of and the fact that .
Showing that maps to under the obvious isomorphism is straightforward. I won’t do this here, but the idea is that by following under , we see that . In fact, we can also show that (a slight rephrasing of) maps to by normalisation in Cubical Agda!
Now we’re done! We have constructed an equivalence and shown that it maps to . Hence, we get, by chapters 1–3 in Brunerie’s thesis, that is .
We know, by Chapters 1–3 in Brunerie’s thesis that the map is related to . But what if we had not read these chapters? The above argument is not by itself enough to show that . However, it is enough to show that
If , then
In other words, the fact that is mapped to is enough to detect the -torsion in .
To see this, let us consider , the easier-to-work-with cousin of , again. There is a map very similar to with the two composites in the -case flipped. Let’s call it . It is defined by
It is an easy lemma that is homotopic to the constant map . In other words, if we could flip the two path components in the definition of , we would have . Naturally, this is not possible. But what happens if we suspend the situation?
By the Fredenthal suspension theorem, postcomposition with induces a surjection . We can easily show that : for point constructors it holds definitionally and for the -case, we are left to show
But this time, we are allowed to flip the path components: we have landed in , and thus the Eckmann-Hilton argument applies, making the above equation hold. So the surjection takes to the constant map, and hence must be a subgroup of .
A formalisation of this proof in Cubical Agda is available here (for some reason, is called in the formalisation — sorry!). I suspect that the argument shouldn’t be much harder to formalise in standard Agda or Coq.
The second half of the file contains the proof by normalising . This, of course, relies on univalence and higher inductive types computing properly and should be doable in other cubical systems, but not in Book HoTT.