Last time we defined cohomology in homotopy type theory; in this post I want to construct the cohomological Serre spectral sequence of a fibration (i.e. a type family). This is the second part of a two-part blog post. The first part, in which I attempted to motivate the notion of spectral sequence, and constructed the basic example that we’ll be using, is at the n-Category Cafe here.
First recall that a spectrum is a family of pointed types such that for all n. Last time I defined the cohomology of a type X with coefficients in a spectrum Y to be
for k sufficiently large that . An equivalent way to define this is as
where is the mapping spectrum defined by , and the homotopy groups of a spectrum Z are defined by
for any and any k sufficiently large that . Again, the definition of a spectrum makes this independent of k. In general, we can “do homotopy theory” with spectra just as we can with types. A map of spectra is, of course, a fiberwise pointed map such that the evident squares commute relating it to the equivalences and . Similarly, the fiber of such a map is defined levelwise, with . It’s easy to see that this inherits a spectrum structure. Moreover, the long exact sequences of homotopy groups for the fiber sequences splice together into a long exact sequence
which is infinite in both directions, with all entries being abelian groups.
Now in part one, I explained how from an iterated fibration sequence
we obtain a spectral sequence with . Moreover, if the iterated fibration sequence stabilizes as (i.e. for it becomes ) and eventually becomes zero at each homotopy group separately as , then this spectral sequence “converges” to the homotopy groups of Y, in the sense that for each n we have a finite iterated extension
in which the terms occurring are precisely the nonzero ones on the diagonal of the page. (There are fancier sorts of convergence that apply to more general situations, but I don’t want to get into that right now.) One writes this as
The only homotopical input required was the long exact sequences of homotopy groups associated to the iterated fibration sequence, which as we’ve seen applies just as well to spectra as to types. After that, it was only homological algebra of abelian groups, which was fully constructive, and hence formalizable using sets in homotopy type theory, with higher inductive types for quotients and images.
Part one was kind of light on examples, though. I mentioned the obvious example of an iterated fibration sequence, namely the Postnikov tower of Y:
If Y is an m-type for some , then this satisfies our simple hypotheses for convergence. A spectrum also has a Postnikov tower, with defined to be . This makes sense for any , as long as we make the convention that if . If we define an m-type spectrum to be one for which is an ordinary -type for all , then the Postnikov tower of such a Y also satisfies our simple hypotheses for convergence despite potentially being infinite downwards (an m-type spectrum can have nontrivial for all ).
The Postnikov tower of a space or spectrum doesn't give rise to an interesting or useful spectral sequence. However, mapping out of a type preserves fibration sequences, so for any type X and spectrum Y we have an induced iterated fibration sequence
where denotes the spectrum whose space is the usual Eilenberg-Mac Lane space if , and contractible otherwise. Note that the spectrum is the Eilenberg-Mac Lane spectrum that we denoted last time.
Hence, we have a spectral sequence with
the “ordinary” cohomology of X with coefficients in the abelian group . If Y is an m-type spectrum for some m, then this spectral sequence converges in the above sense to the homotopy groups , which as remarked above are the cohomology .
This is called the Atiyah-Hirzebruch spectral sequence. It says that for any (sufficiently nice) spectrum Y, the cohomology of any type X with coefficients in Y (what algebraic topologists call “generalized cohomology”) can be put together out of the “ordinary” cohomology of X with coefficients in the homotopy groups of Y. One usually flips the sign of p and q in “cohomological” spectral sequences of this sort, simultaneously switching the subscripts and superscripts; thus we write instead
Graphically, this corresponds to rotating all the “pages” of the spectral sequence by 180 degrees about the origin. This causes the differentials to go down and right rather than left and up. (Note also that is also the cohomology of a point with coefficients in Y.)
Of course, this may not seem very interesting unless you have some spectra up your sleeve other than whose cohomology you care about. However, we can also use it to construct the Serre spectral sequence, which is interesting even as a statement only about ordinary cohomology.
First we have to generalize our notion of cohomology a bit. In the language of classical algebraic topology, we’re going to define parametrized cohomology theories, including as a special case cohomology with local coefficients. However, in type-theoretic language, what’s going on is extremely simple and natural: replacing function types with dependent function types.
Thus, suppose X is a type and is an X-indexed family of spectra. We define the cohomology of X with coefficients in Y to be
where is the “spectrum of sections of Y” defined by . As usual with dependent function types, when Y is a constant family this reduces to the previously defined notion of cohomology.
Where do families of spectra come from? One place they come from is families of abelian groups. If is such, then composing it with the “Eilenberg-Mac Lane spectrum” function we obtain an X-indexed family of spectra, . Note that since abelian groups are sets, is a 1-type, and hence any such A factors through , the “fundamental groupoid” of X. This is the homotopy-type-theory version of what classical algebraic topologists would call a local system on X. If X is pointed and connected, then , and so (using the univalence axiom) we can further reduce a local system to a single abelian group with an action by , the most classical notion. The cohomology of X with coefficients in is called cohomology with local coefficients.
Where do local systems come from? One place they come from is homotopy groups of families of types (or spectra). We can compose or with any family of pointed types or of spectra to obtain a local system. I think the ease with which we can pass back and forth between local systems and families of spectra is a good example of the value of the type-theoretic framework.
In the same way, we can construct the “fiberwise” Postnikov tower of a family of spectra , obtaining an X-indexed family of iterated fibration sequences. The fibers of these fibration sequences are loopings or deloopings of “parametrized Eilenberg-Mac Lane spectra” associated to the local systems . Sinc , like , preserves fibration sequences, we get a more general Atiyah-Hirzebruch spectral sequence with (meaning the cohomology with local coefficients in the local system ), which converges to if Y is a family of m-type spectra.
Now we’re ready to deduce the Serre spectral sequence. Let Y be an ordinary spectrum, such as H A, and let be a type family. Then is an X-indexed family of spectra, which are m-type spectra if Y is. Thus, we have the above “parametrized” Atiyah-Hirzebruch spectral sequence:
On the left, we have by definition. And as for the right side, we have
the cohomology of the total space of the fibration F with coefficients in Y. (The second step is a spectral version of the ordinary universal mapping property of -types, .) Thus, our spectral sequence becomes
which is the usual cohomological Serre spectral sequence, relating the cohomology of the base, with local coefficients in the cohomology of the fiber, to the cohomology of the total space. Note that if X is pointed and simply connected, so that , then any local system on X is constant, and so the cohomology with local coefficients in the domain reduces simply to the ordinary cohomology of X with coefficients in the cohomology of the fiber over the basepoint.
After all of this theory, I ought to give you at least one application to justify it all. Here’s a fairly easy one. Suppose we have a fibration of spheres, i.e. a fiber sequence in which all three types are spheres of some dimension, and suppose that so that is simply connected and that and for nontriviality. Then we have a Serre spectral sequence
The Eilenberg-Steenrod axioms for ordinary cohomology (i.e. with coefficients in ) easily imply that is when and , and zero otherwise. Thus, the page of this spectral sequence is at , and zero everywhere else. The only possible nontrivial differential would be a map from to , and this is only possible if . If there is no such differential, then , and so the target will be built out of nontrivial groups for . However, we know that is zero unless , so this is impossible. Therefore, , the differential is an isomorphism and “kills” both of these groups, and . (This argument by contradiction is valid constructively, since natural numbers have decidable equality.)
In conclusion, the only possible fibrations of spheres are of the form . When we do have such a fibration, namely the Hopf fibration. (Classically, there are also such fibrations for and no other positive values of a — the latter is a famous theorem called the “Hopf invariant one problem”.)
There are lots of other applications of spectral sequences; it’ll be fun to see how many of them we can reproduce. Many of them require homology in addition to cohomology, though, which would be a whole other post.
One last comment deserves to be made. I claimed that this “is” the Serre spectral sequence, but actually I haven’t proven that. It has the same groups in its page, and converges to the same thing, but that doesn’t imply that the whole spectral sequence is the same (although it strongly suggests it). And I haven’t seen this construction of the Serre SS anywhere in the classical algebraic topology literature (although I’d be surprised if it were new) — most constructions use instead a CW decomposition of X, which is unavailable to us. So does this “Serre spectral sequence” agree with the classical one when interpreted in the simplicial model? I’m not sure how to go about trying to prove that.