One of the fundamental constructions of classical homotopy theory is the Postnikov tower of a space X. In homotopy type theory, this is just its tower of truncations:
One thing that’s special about this tower is that each map has a (homotopy) fiber that is an Eilenberg-MacLane space
. This is easy to see from the long exact sequence. Moreover, when X is a special sort of space, such fibrations are classified by cohomology classes, according to the following theorem:
Theorem: Suppose has (homotopy) fibers that are all merely isomorphic to
, for some
and some abelian group A. Then the following are equivalent:
- f is the homotopy fiber of a map
.
- The induced action of
(at all basepoints) on A is trivial.
A space for which each map has this property is called simple, and the resulting maps
are called its k-invariants. Note that they live in the cohomology group
.
The above theorem can be found, for instance, as Lemma 3.4.2 in More Concise Algebraic Topology, where it is proven using the Serre spectral sequence. In this post I want to explain how in homotopy type theory, it has a clean conceptual proof with no need for spectral sequences.
Dan recently posted about the construction of Eilenberg-MacLane spaces. Here we’ll only need the fact that they exist, together with the following:
Lemma: The type of pointed maps between Eilenberg-MacLane spaces is equivalent to the set
of group homomorphisms.
Proof: by induction on . When
, the construction of
as a HIT gives this fairly immediately. For the induction step, by definition we have
. Since
is an
-type, pointed maps
are equivalent to pointed maps
, hence to pointed maps
.
Now suppose given as in the above theorem. We may as well assume that
is
for some
, and by assumption
factors through the type
. Thus, we need to analyze the homotopy type of this space, which I will denote
, the type of Eilenberg-MacLane spaces
.
This type should not be confused with the type , the type of pointed Eilenberg-MacLane spaces, which is defined as
, with
the type of pointed types. Since two connected pointed types are merely equal in
if and only if they are merely equal in
, we can write
. Therefore, the fiber of the forgetful map
over the canonical space
is
itself. On the other hand, by the lemma,
can be identified with
. In other words, we have a fiber sequence
If , the resulting long exact sequence tells us that
and
and all other homotopy groups are
.
If we have to do a little more work: we compute that the map
corresponds to the map
which is the action of A on itself by conjugation, so that
, the outer automorphism group of A (the quotient of this action), while
, the center of A (the kernel of this action). Since A is abelian, we have
and
, so this is the same as the case
.
It follows that , and the long exact sequence of the truncation map
tells us that its fiber is
. That is, we have a fiber sequence
It follows that our classifying map (remember it?) factors through
if and only if its image in
is trivial. But
is a 1-type, so maps from
into it factor uniquely through
. And a map
essentially consists of maps
for all basepoints, i.e. actions of
on A, and is trivial just when those actions are trivial.
We’re almost done with the theorem! The only thing left to show is that when the classifying map factors through
, then
is in fact the homotopy fiber of the factorization. In other words, we want to show that when the canonical fibration
is pulled back to
, its domain is contractible. But this pulled back fibration over
has fiber
, so contractibility of its domain follows from its long exact sequence.
Q.E.D.
Note that this proof gives us a bit more: if and A is not abelian, then
with fiber
is classified by a map
if and only if
acts on
through inner automorphisms. But even leaving that slight generalization aside, I find this proof to be more illuminating than a spectral sequence argument. It also makes it clear that if the action is nontrivial, then the k-invariants live in some kind of more general cohomology (specifically, cohomology with local coefficients).
I should emphasize, though, that there is a related surprise for classical homotopy theorists: the space X may not be the limit of its Postnikov tower unless it is already finitely truncated. This is a bit unfortunate, but we can still extract useful information about X from its tower.
For instance, suppose is a map of simple spaces which induces an isomorphism
on cohomology with coefficients in all abelian groups
, for all
Now suppose Z is a simple n-type, which is therefore the limit of its Postnikov tower that has k-invariants in ordinary cohomology. By inducting up this tower, therefore, we can show that the induced map
is a bijection, where
is the set of homotopy classes of maps.
Now take ; then the truncation map
extends to some homotopy class of maps
. And by uniqueness, the resulting composite
must be the truncation map of
. Applying n-truncation again to this whole sequence of maps
, we see that
is an equivalence.
In other words, a map of simple spaces which induces an isomorphism on ordinary cohomology is necessarily -connected. This can be extended to “nilpotent” spaces as well, which are basically those whose truncations can be contructed out of Postnikov-like towers with more than one space at each “level”. Thus, for a large class of spaces, isomorphisms on ordinary cohomology suffice to detect isomorphisms of homotopy groups. This gives a bit of a clue as to why algebraic topologists spend so much time computing cohomology.
To get some idea for how amazing this is, consider . This is 1-connected, so it’s simple. It has all sorts of complicated higher homotopy groups, but its cohomology is quite trivial:
if
and 0 otherwise. This result says that if we have any other simple space Y with the same boring cohomology,
if
and 0 otherwise — and a map
inducing the isomorphism on cohomology — then Y necessarily has all the same complicated higher homotopy groups as
!
This was fun to read!
I keep wondering whether “nilpotent” has a generalization that ought to be called “solvable”.
Thanks! That’s an interesting question. Is there a way to say what it means for one group to “act solvably” on another one?