Spectral Sequences

Posted on 8 August 2013 by Mike Shulman

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.

(Note: the quicklatex images originally included in this post are now broken. A version that includes the intended math displays can be found here.)

First recall that a spectrum is a family of pointed types $Y : \mathbb{N} \to \mathsf{Type}_\ast$ such that $Y_n = \Omega Y_{n+1}$ for all n. Last time I defined the cohomology of a type X with coefficients in a spectrum Y to be

$H^n(X;Y) :\equiv \Vert X \to \Omega^{k-n} Y_n \Vert_0$

for k sufficiently large that $k-n \ge 0$ . An equivalent way to define this is as

$H^n(X;Y) :\equiv \pi_{-n} (\mathsf{SpMap}(X,Y))$

where $\mathsf{SpMap}(X,Y)$ is the mapping spectrum defined by $\mathsf{SpMap}(X,Y)_n :\equiv (X\to Y_n)$ , and the homotopy groups of a spectrum Z are defined by

$\pi_n (Z) :\equiv \pi_{k+n}( Z_k)$

for any $n \in \mathbb{Z}$ and any k sufficiently large that $n+k\ge 0$ . 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 $f : \prod_{(n:\mathbb{N})} Y_n \to Z_n$ such that the evident squares commute relating it to the equivalences $Y_n = \Omega Y_{n+1}$ and $Z_n = \Omega Z_{n+1}$ . Similarly, the fiber of such a map is defined levelwise, with $\mathsf{fib}(f)_n :\equiv \mathsf{fib}(f_n)$ . It’s easy to see that this inherits a spectrum structure. Moreover, the long exact sequences of homotopy groups for the fiber sequences $\mathsf{fib}(f_n) \to Y_n \to Z_n$ splice together into a long exact sequence

$\cdots \to \pi_n(\mathsf{fib}(f)) \to \pi_n(Y) \to \pi_n(Z) \to \cdots$

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 $E^2_{p q} = \pi_{p+q}(X_q)$ . Moreover, if the iterated fibration sequence stabilizes as $s\to \infty$ (i.e. for $s>T$ it becomes $\mathbf{1} \to Y \to Y$ ) and eventually becomes zero at each homotopy group separately as $s \to -\infty$ , 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 $E^\infty$ terms occurring are precisely the nonzero ones on the diagonal $p+q=n$ of the $E^\infty$ 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

$E^2_{p,q} = \pi_{p+q}(X_q) \Longrightarrow \pi_{p+q}(Y)$

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 $m<\infty$ , then this satisfies our simple hypotheses for convergence. A spectrum also has a Postnikov tower, with $(\Vert Y \Vert_s)_n$ defined to be $\Vert Y_n\Vert_{n+s}$ . This makes sense for any $s \in \mathbb{Z}$ , as long as we make the convention that $\Vert X\Vert_{m} = \mathbf{1}$ if $m < -1$ . If we define an m-type spectrum to be one for which $Y_n$ is an ordinary $(n+m)$ -type for all $n \ge -m-2$ , 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 $\pi_n$ for all $-\infty < n \le m$ ).

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 $K(A,s)$ denotes the spectrum whose $n^{\mathrm{th}}$ space is the usual Eilenberg-Mac Lane space $K(A,s+n)$ if $s+n\ge 0$ , and contractible otherwise. Note that the spectrum $K(A,0)$ is the Eilenberg-Mac Lane spectrum that we denoted $H A$ last time.

Hence, we have a spectral sequence with

the “ordinary” $(-p)^{\mathrm{th}}$ cohomology of X with coefficients in the abelian group $\pi_q(Y)$ . If Y is an m-type spectrum for some m, then this spectral sequence converges in the above sense to the homotopy groups $\pi_n( \mathsf{SpMap}(X,Y))$ , which as remarked above are the cohomology $H^{-n}(X;Y)$ .

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

$E_2^{pq} = H^q(X;\pi_{-q}(Y)) \Longrightarrow H^{p+q}(X;Y)$

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 $\pi_{-q}(Y) = H^q(\mathbf{1};Y)$ is also the $q^{\mathrm{th}}$ 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 $H A$ 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 $Y : X \to \mathsf{Spectrum}$ is an X-indexed family of spectra. We define the cohomology of X with coefficients in Y to be

$H^n(X;Y) :\equiv \pi_{-n} (\mathsf{SpSect}(X,Y))$

where $\mathsf{SpSect}(X,Y)$ is the “spectrum of sections of Y” defined by $\mathsf{SpSect}(X,Y)_n :\equiv \prod_{(x:X)} Y(x)_n)$ . 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 $A : X \to \mathsf{AbGp}$ is such, then composing it with the “Eilenberg-Mac Lane spectrum” function $H : \mathsf{ApGp}\to \mathsf{Spectrum}$ we obtain an X-indexed family of spectra, $H A$ . Note that since abelian groups are sets, $\mathsf{AbGp}$ is a 1-type, and hence any such A factors through $\Vert X \Vert_1$ , 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 $\Vert X \Vert_1 = K(\pi_1(X),1)$ , and so (using the univalence axiom) we can further reduce a local system to a single abelian group with an action by $\pi_1(X)$ , the most classical notion. The cohomology of X with coefficients in $H A$ 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 $\pi_n : \mathsf{Type}_\ast \to \mathsf{AbGp}$ or $\pi_n : \mathsf{Spectrum} \to \mathsf{AbGp}$ with any family $Y : X \to \mathsf{Type}_\ast$ of pointed types or $Y : X \to \mathsf{Spectrum}$ 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 $Y : X \to \mathsf{Spectrum}$ , 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 $\pi_q(Y) : X \to \mathsf{AbGp}$ . Sinc $\mathsf{SpSect}$ , like $\mathsf{SpMap}$ , preserves fibration sequences, we get a more general Atiyah-Hirzebruch spectral sequence with $E^{p q}_2 = H^{p}(X;\pi_{-q}(Y))$ (meaning the cohomology with local coefficients in the local system $\pi_{-q}(Y)$ ), which converges to $H^{p+q}(X;Y)$ 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 $F : X \to \mathsf{Type}$ be a type family. Then $x\mapsto \mathsf{SpMap}(F_x,Y)$ 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:

$H^p(X;\lambda x.\pi_{-q}(\mathsf{SpMap}(F_x,Y))) \Longrightarrow H^{p+q}(X;\mathsf{SpMap}(F_x,Y)).$

On the left, we have $\pi_{-q}(\mathsf{SpMap}(F_x,Y)) = H^q(F_x;Y)$ 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 $\Sigma$ -types, $((\sum_{(x;X)} F_x) \to Z) = \prod_{(x:X)} (F_x \to Z)$ .) Thus, our spectral sequence becomes

$H^p(X;\lambda x. H^q(F_x;Y)) \Longrightarrow H^{p+q}(\sum_{(x:X)} F_x;Y)$

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 $\Vert X \Vert_1 = \mathbf{1}$ , 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 $S^a \to S^b \to S^c$ in which all three types are spheres of some dimension, and suppose that $c>1$ so that $S^c$ is simply connected and that $a>0$ and $b>0$ for nontriviality. Then we have a Serre spectral sequence

$H^p(S^c; H^q(S^a;\mathbb{Z})) \Longrightarrow H^{p+q}(S^b;\mathbb{Z})$ .

The Eilenberg-Steenrod axioms for ordinary cohomology (i.e. with coefficients in $H \mathbb{Z}$ ) easily imply that $H^n(S^m;\mathbb{Z})$ is $\mathbb{Z}$ when $n=0$ and $n=m$ , and zero otherwise. Thus, the $E_2$ page of this spectral sequence is $\mathbb{Z}$ at $(0,0), (c,0), (0,a), (c,a)$ , and zero everywhere else. The only possible nontrivial differential would be a map from $E^r_{0,a}$ to $E^r_{c,0}$ , and this is only possible if $c = a+1$ . If there is no such differential, then $E_\infty = E_2$ , and so the target $H^n(S^b;\mathbb{Z})$ will be built out of nontrivial groups for $n = 0,a,c,a+c$ . However, we know that $H^n(S^b;\mathbb{Z})$ is zero unless $n = 0,b$ , so this is impossible. Therefore, $c = a+1$ , the differential $E^r_{0,a} \to E^r_{c,0}$ is an isomorphism and “kills” both of these groups, and $b = a+c = 2a+1$ . (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 $S^a \to S^{2a+1}\to S^{a+1}$ . When $a=1$ we do have such a fibration, namely the Hopf fibration. (Classically, there are also such fibrations for $a=3,7$ 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 $E_2$ 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.

This entry was posted in Homotopy Theory. Bookmark the permalink.

19 Responses to Spectral Sequences

Kari says:

9 August 2013 at 01:54

“at the n-Category” link points to this blog post itself.

Reply
- Mike Shulman says:
  
  9 August 2013 at 01:58
  
  Thanks, fixed.
  
  Reply
jessemckeown says:

9 August 2013 at 15:11

most constructions use instead a CW decomposition of X, which is unavailable to us. …

Yeah, this sort-of bothered me, too, when trying to build one of these spectral sequences the other way. On The Other Hand, a CW complex isn’t much more than a colimit of iterated colimits (of planar diagrams!), which a HoTT fan should read as “higher inductive type”; and then the classic Serre Spectral Sequence, starting on page 1 rather than page 2, is essentially what the flattening lemma has to say about cohomology. So, another side of the question is whether there is a script that, given a HIT presentation (in increasing dimension order, to be nice), outputs a proof that the flattening sequence and the dependent-spectra sequence are the same.

The last one small thing is, for some reason, according to McCleary’s book, we’re supposed to restrict the adjective “Serre” (or “Leray-Serre”) to when the fibers are all connected — and I think what he’d do with disconnected fibers is pull back along a universal cover of the base, to where fiber components are in bijection with total-space components in the natural way, and then use the Cartan-Leray sequence to relate to the original fibration; it’s possible that the present spectral sequence is genuinely different, or that it generalizes both cases, or it’s possible that this argument, starting at the next page down, obviates whatever difficulties arise from disconnected fibers. Of course, if the base space is already *simply* connected, it’s a non-issue because of the component bijection.

Reply
- Mike Shulman says:
  
  9 August 2013 at 15:51
  
  Ah, yes, the traditional algebraic topologist’s inexplicable myopia of connectedness. I can never remember when reading an algebraic topology book whether at that point “all spaces are assumed to be connected” or not.
  
  the classic Serre Spectral Sequence, starting on page 1 rather than page 2, is essentially what the flattening lemma has to say about cohomology
  
  Can you elaborate on that? Obviously the flattening lemma is relevant, but doesn’t there still have to be either a double-complex or an exact-couple argument to get out a SS?
  
  Reply
  - jessemckeown says:
    
    10 August 2013 at 00:29
    
    Exact couples, it seems, are equivalent in some sense to filtrations (or there are ways to get one gadget from the other such that their respective spectral sequences are naturally isomorphic)
    
    Here you’ve chosen to filter a cohomology theory; back in february I tried a different filtration of a cohomology theory, and I suspect (though can’t yet argue) that these give “the same” SS; the Serre spectral sequence chooses to filter the total space instead, but specifically by pulling-back over a homologically-good filtration of the base space. Flattening says that this filtration realizes the total space as a colimit of iterated pushouts along projections to copies of the fibers (one copy for each component of the base if we’re being that careful). So, there’s an early page in the related SS that’s described by the Mayer-Vietoris long exact sequence for this sequence of pushout squares; etc.
    
    Does that help?
    
    Reply
    - Mike Shulman says:
      
      10 August 2013 at 01:07
      
      I guess it depends on what you’re willing to sweep under the carpet of “essentially”. To me, the construction of a spectral sequence from a filtration or exact couple is the nontrivial bit, while the fact that a filtration of the base space induces one on the total space is “obvious” (flattening).
      
      Is there a general way to obtain a filtration from an exact couple? I can see how the other direction works, via a collection of long exact sequences, but from just an arbitrary exact couple, what is it that’s being filtered?
      
      Reply
      - jessemckeown says:
        
        11 August 2013 at 01:01
        
        It’s the standard filtration of the mapping telescope for the endomorphism $\varphi$ , I think.
        
        Reply
        
        Mike Shulman says:
        
        11 August 2013 at 01:13
        
        What is $\varphi$ ?
        
        Reply
        
        jessemckeown says:
        
        11 August 2013 at 08:26
        
        right… ehem.
        “Let the exact couple be $D \overset{\varphi}{\to} D \to E \to D$ , and filter the infinite mapping telescope $\colim [ D \overset{\varphi}{\to} D \overset{\varphi}{\to} \cdots ]$ by… “
        
        Reply
        
        Mike Shulman says:
        
        11 August 2013 at 12:30
        
        That gives you a filtered graded group. To get a spectral sequence, don’t you have to have a filtered chain complex? (Plus, here we’re talking about a filtered space.)
        
        Reply
      - jessemckeown says:
        
        12 August 2013 at 18:03
        
        Starting a somewhat-wider reply thread…
        Upon reviewing the section in McCleary that is titled “Equivalence of the two approaches”, the two being filtrations and exact couples, indeed only the summary of the filtration sequence as a special exact couple is considered.
        
        Upon review of the earlier section introducing exact couples, there is a remark that the target of an exact couple sequence is in general difficult to describe, though I can only surmise that he means eventual images (and in what sense the pages approach them) are difficult to describe.
        
        Upon review of the telescope construction, it seems that the filtration sequences these lead to are not altogether interesting nor helpful, so I’ll let that suggestion drop; but I had in mind mapping telescopes of graded complexes, if it helps at all.
        
        Reply
Ulrik says:

14 October 2015 at 17:54

“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.”

Perhaps the uniqueness theorem from Barnes’ 1985 “Spectral sequence constructors in algebra and topology” could apply?

BTW, it’s a shame that the images for this post that were hosted on quicklatex.com don’t seem to be accessible any more. Is there a way to recover them?

Reply
- Mike Shulman says:
  
  16 October 2015 at 14:41
  
  Thanks for the suggestion! I glanced at the introduction to Barnes’ book quickly on google books and saw that it mentions filtered complexes. Does the uniqueness theorem (not shown in preview) also use filtered complexes? The construction sketched in this post goes directly to an exact couple without using a filtered complex (although it’s possible it could be rephrased using a filtered complex, I don’t know).
  
  I don’t know about quicklatex, does anyone?
  
  Reply
Urs Schreiber says:

10 February 2016 at 05:38

This is quite an excellent discussion. In the interest of posterity, maybe you could fix the following issues:

All the images are broken now. (They didn’t used to.)

In the maths line after “Thus, we have the above ‘parametrized’ Atiyah-Hirzebruch spectral sequence:” I think you’ll want another “lambda x”.

In “Now in part one,” the link is broken (probably the source code gives an empty url, which is then automatically replaced by a pointer to this page here.)

Would it be hard to transport the entire source of this entry and its “Part I” over to the nLab? There we could hist this more stably, and with more cross-links

Reply
- Mike Shulman says:
  
  11 February 2016 at 11:50
  
  Thanks! The wayback machine helped me recover what the images were supposed to say, and I’ve now put both parts of the post here.
  
  Reply
Urs Schreiber says:

29 April 2016 at 08:57

Coming back to the open question at the end:

> So does this “Serre spectral sequence” agree with the
> classical one when interpreted in the simplicial model?

It look like this has been proven in

C. R. F. Maunder,
“The spectral sequence of an extraordinary cohomology theory”
Mathematical Proceedings of the Cambridge Philosophical Society
Volume 59 / Issue 03 / pp 567- 574
July 1963
DOI: 10.1017/S0305004100037245,
http://journals.cambridge.org/abstract_S0305004100037245

Page 5 shows the two spectral sequences (using the notation for Postnikov towers of spectra on p. 3). One is the standard AHSS, the other one should be Mike’s version from above (I haven’t checked in detail, but it seems clear enough). Theorem 3.3 states that both are isomorphic.

Reply
- Mike Shulman says:
  
  2 May 2016 at 00:28
  
  Wow! That’s some impressive sleuthing; how did you find it? I have not read through the proof yet, but the statement does indeed seem to claim that the AHSS constructed in the way that I did it above is isomorphic to the standard one. (Glancing at the proof, I see it proceeds by constructing an isomorphism of exact couples from the derived exact couple of the standard approach to the one that I used, which seems eminently plausible.) That doesn’t directly give a comparison for the Serre SS, but it seems likely that the same method would work for the parametrized AHSS, hence also the Serre SS. Thanks!
  
  Reply
  - Urs Schreiber says:
    
    2 May 2016 at 03:37
    
    > how did you find it?
    
    Hisham Sati found it. With Dan Grady he is presently finalizing an article on Atiyah-Hirzebruch-type spectral sequences for differential cohomology, represented as cohesive sheaves of spectra. In discussing possibilities for how to set this up, in the introduction they remark that some Maunder has shown that two natural ways of going about the classical AHSS are isomorphic. Hisham has recently sent me a preliminary version of the article to read, and when I came across that remark, I immediately thought that they must have found the relation that you were looking for here.
    
    Reply
- Mike Shulman says:
  
  2 May 2016 at 17:24
  
  Interestingly, apparently Maunder’s motivation for proving this comparison was that he considered the differentials to be more computable when the AHSS is constructed with truncations, the way I did it. I can’t really evaluate that, but it’s promising for the day when we need to start computing differentials in HoTT applications of spectral sequences.
  
  Reply