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.
Preliminaries
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 equivalence 
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.
via joins
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
.
The proof
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
.
A corollary
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
.
Formalisation
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.
This is quite excellent! Congratulations! I’m still wrapping my head around it, but I have a couple of questions.
1. It feels funny to me to use a representable definition of homotopy groups in HoTT. It’s always seemed to me like the primitive notion of path-space supplied by identity types is easier to work with, indeed kind of the point. I wonder whether your representable definition of
using
can be transferred back to a “primitive” notion? (E.g., write out the universal property of maps out of
and re-express it entirely in terms of paths and higher paths in
.) If so, how much of the calculation could be reformulated in such primitive language?
2. You say that it doesn’t matter which isomorphism
we use, since as long as it’s a group isomorphism there are only two choices and they differ by a sign. That’s certainly true if we only care about calculating
up to isomorphism, since
and
generate the same subgroup of
. But can’t one still ask whether your isomorphism is the same as the “canonical” one given by the usual definition of the Hopf fibration, and thus whether the “original” Brunerie number really is
or
? Presumably this depends on a choice made in the definition of the Hopf fibration, but it would still be interesting to know whether the “usual” choice leads to
or
.
Thanks for the comment:-)
1. Yeah, this feels funny to me too. I always try to avoid the representable definition, but it does have its advantages (clearer correspondence to cohomology/cohomotopy groups of spheres for instance — not that I used that here, but in theory at least…)
I think the most important thing with
is not that it’s defined using joins, but the fact that it’s equivalent to
(for this to really be an equivalent I think we need to also require pointedness in both arguments of the functions
) which I’m kind of using implicitly.
However, I don’t think we want to simplify things more than this. The really neat thing about the
definition (actually, this should probably be
for arbitrary
but I haven’t formalised that yet) is precisely that it allows us to consider maps
as maps
instead. As was the case in the proof, this often allows us to describe the map we’re considering in terms of
and
. In particular, proving things about such maps boils down to proving things about
and
, which breaks everything into small and elementary lemmas. You can, of course, also translate everything and work entirely in something like
, but then you have to deal with big terms involving annoying coherence paths.
2. Yeah, this is true. A reasonable criterion for the isomorphism
being the canonical one seems to me to be that
gets mapped to the Hopf map
. With my definition, this should be the case. However, the definition of the Hopf map depends on two things: the definition of the (‘pre’-) Hopf map
and the definition of the equivalence
. For the Hopf map, I think my definition should agree with Guillaume’s. He describes it via the Hopf construction, so one has to work a bit to see that it actually unfolds to my definition — this is what I remember verifying in Agda at least, but I might have got a sign wrong somewhere. The equivalence
is also sensitive. I defined it in terms of
whereas Guillaume defined it using a more general argument. I’m not sure that my definition agrees with his exactly, but think it does (both are defined, in some sense, by pattern matching on the left argument). If, however, I would’ve constructed
via pattern matching on the right, the Hopf map would’ve been flipped. Assuming our definitions of
are different, that of course begs the question: which one is the canonical one? It actually seems to me that the Hopf map does not have a canonical definition in HoTT, in the sense of its classical counterpart.
Just to say that a prolific but anonymous and unresponsive contributor has recently created an nLab page on the topic, titled:
“homotopy groups of spheres in HoTT”
<ncatlab.org/nlab/show/homotopy+groups+of+spheres+in+HoTT
(maybe this was copied over from the now deprecated “homotopytheory” sub web?, I am not sure)
The page remains a little telegraphic, but it could serve a good service to anyone interested in the topic.
I have now added there a pointer to this blog entry here, but if anyone would like to add more material, please feel invited.
(Just be sure to leave a brief log message of what you did, and check out the nForum discussion regarding the page, [here](https://nforum.ncatlab.org/discussion/14559/homotopy-groups-of-spheres-in-hott/?Focus=99755#Comment_99755))
In particular, if or when there is any citable publication on the work reported here, it would be nice to add a reference on the nLab page.