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?