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:

1. f is the homotopy fiber of a map .
2. 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 !