nLab spectral sequences in homotopy type theory

Spectral sequences in homotopy type theory


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts


This page is about formalizing the notion of spectral sequences in homotopy type theory. For now, it contains mainly a fixed version of two blog posts, one at the n-category cafe and the other on the HoTT blog. For more see the References below.

Spectral sequences in homotopy type theory

What is a spectral sequence?

There are many answers to “what is a spectral sequence?”, but the one I’m proposing right now is the following analogy. (In my experience, category theorists tend to like analogies — possibly because, as John Baez once said, every sufficiently good analogy is yearning to become a functor. This one is no exception.)

Spectral sequences are to long exact sequences as iterated extensions are to extensions.

(Without knowing anything else, the terminology suggests that spectral sequences could also be called “iterated long exact sequences”.)

There are four phrases here that I need to explain, and two more concepts that have a ghostly presence (fibration sequences and iterated fibration sequences). First of all, an extension is a sequence of morphisms of abelian groups (for simplicity — more generally we could be in any abelian category):

AfBgC A \xrightarrow{f} B \xrightarrow{g} C

such that ff is the inclusion of the kernel of gg, and gg is the quotient of BB by the image of ff. Equivalently, ff is injective, gg is surjective, and the image of ff is equal to the kernel of gg. The simplest example is

A(id,0)ACproj 2C. A \xrightarrow{(id,0)} A\oplus C \xrightarrow{proj_2} C.

An extension that’s isomorphic to one of this form is said to be split. In general, we can regard an extension as exhibiting BB as “put together” in some more general way from AA and CC; we say that BB is an “extension of CC by AA”. The underlying set of BB is always isomorphic to the cartesian product A×CA\times C, so we can think of BB as a sort of “twisted product” of AA and CC. (In fact, as usual in this sort of situtaion, the twisting is measured by a cohomology class, living in Ext 1(C,A)Ext^1(C,A), but we won’t need that today.)

Thinking of BB as put together from AA and CC, we can draw certain conclusions about the one from the other, or the other from the one. The most obvious is that if A=C=0A=C=0, then also B=0B=0. The converse also holds: if B=0B=0, then A=C=0A=C=0. If only A=0A=0, then we can conclude B=CB=C, and similarly if C=0C=0 we have A=BA=B. We can also say fancier things of this sort, e.g. BB is finite, or finitely generated, if and only if both AA and CC are.

Next, a long exact sequence (LES) is a longer sequence of morphisms of abelian groups

f n+1A n+1f nA nf n1 \cdots \xrightarrow{f_{n+1}} A_{n+1} \xrightarrow{f_n} A_n \xrightarrow{f_{n-1}} \cdots

such that for each nn, the image of f nf_n is equal to the kernel of f n1f_{n-1} (called “exactness at A nA_n”). The sequence might be infinite or finite in either direction. How are LES’s related to extensions? Well, one obvious relationship is that an extension can equivalently be described as an exact sequence of the form

0AfBgC0 0 \to A \xrightarrow{f} B \xrightarrow{g} C \to 0

(a “short exact sequence”), since in such a sequence, exactness at AA just means injectivity of ff, and exactness at CC just means surjectivity of gg. However, what I want to focus on instead is the basic homotopical origin of LES’s, namely fibration sequences. A fibration sequence is a sequence of maps of pointed spaces

XfYgZ X \xrightarrow{f} Y \xrightarrow{g} Z

such that ff is (up to homotopy) the inclusion of the homotopy fiber of gg over the basepoint. (By “space” I really mean “\infty-groupoid”, which a classical topologist could read as “topological space up to weak homotopy equivalence” or “simplicial set up to weak homotopy equivalence”, and a homotopy type theorist could read as “type”.) The simplest example is

XX×ZZ, X \to X\times Z \to Z,

the “trivial bundle” over ZZ with fiber XX. In general, we can think of YY as being “put together” from XX and ZZ in some more general way, as a “twisted product”. Note that this is very similar to how we think of an extension, except that we’ve replaced our abelian groups with spaces.

Of course, a space is not exactly an abelian group, but it contains many abelian groups, namely its homotopy groups. So we might expect that if YY is a twisted product of XX and ZZ as above, that its homotopy groups π n(Y)\pi_n(Y) would be twisted products of π n(X)\pi_n(X) and π n(Z)\pi_n(Z), i.e. that there would be extensions π n(X)π n(Y)π n(Z)\pi_n(X) \to \pi_n(Y) \to \pi_n(Z). This is not true, since the various dimensions nn can “interact” in a nontrivial way; but instead we have a long exact sequence

π n+1(X)π n+1(Y)π n+1(Z)π n(X)π n(Y)π n(Z). \cdots \to \pi_{n+1}(X) \to \pi_{n+1}(Y) \to \pi_{n+1}(Z) \to \pi_n(X) \to \pi_n(Y) \to \pi_n(Z) \to \cdots.

This LES can be regarded as expressing a way in which the groups π n(Y)\pi_n(Y), considered as a whole, are “put together” out of the π n(X)\pi_n(X)‘s and π n(Z)\pi_n(Z)’s. We get some of the same sorts of results, e.g. if π n(X)=0\pi_n(X)=0 for all nn, then π n(Y)=π n(Z)\pi_n(Y) = \pi_n(Z) for all nn, and dually. But some different things happen, e.g. if π n(Y)=0\pi_n(Y)=0 for all nn, rather than π n(X)=0=π n(Z)\pi_n(X) = 0 = \pi_n(Z) we get π n(X)=π n+1(Z)\pi_n(X) = \pi_{n+1}(Z) for all nn (and indeed, if YY is contractible, then X=ΩZX = \Omega Z).

Another way to express the LES of a fibration, which looks more like what we’ll see for spectral sequences later on, is that there exist maps δ n:π n(Z)π n1(X)\delta_n : \pi_n(Z) \to \pi_{n-1}(X) and extensions

im(δ n+1)π n(Y)ker(δ n). im(\delta_{n+1}) \to \pi_n(Y) \to ker(\delta_n).

In other words, instead of π n(Y)\pi_n(Y) being put together from π n(X)\pi_n(X) and π n(Z)\pi_n(Z), it’s put together from a subgroup of π n(Z)\pi_n(Z) and a quotient of π n(X)\pi_n(X). This allows us to fulfil the yearnings of the analogy between fibration sequences and extensions: for each nn there’s a functor from the category of fibration sequences to the category of extensions, sending XYZX\to Y\to Z to the above extension.

Of course, π n\pi_n is only an abelian group for n2n\ge 2. Some of what we do with abelian groups can be extended to the case of groups (n=1n=1) and pointed sets (n=0n=0), but I don’t want to get into that. Feel free to assume all spaces are simply connected. Another way to avoid nonabelianness is to replace spaces with spectra, in which case π n\pi_n is an abelian group not only for all n0n\ge 0 but for all nn\in \mathbb{Z}. In this case, the LES of a fibration sequence extends infinitely in both directions.

Now let’s move on to the other side of the analogy, starting with iterated extensions. By an iterated extension I mean a sequence of extensions of the following form:

A s+1B s+1B s A sB sB s1 A s1B s1B s2 \array{ \vdots \\ A_{s+1} \to B_{s+1} \to B_s\\ A_s \to B_{s} \to B_{s-1} \\ A_{s-1} \to B_{s-1} \to B_{s-2}\\ \vdots }

The intent here is to regard B:lim(B s+1B s)B :\equiv \lim (\cdots \to B_{s+1} \to B_s \to \cdots) as “put together” from the A sA_s‘s and from C:colim(B s+1B s)C :\equiv \colim (\cdots \to B_{s+1} \to B_s \to \cdots). In many cases, the sequence of A sA_s’s will be eventually zero in one direction or the other, so that the sequence of B sB_s’s will similarly be eventually constant. Eventual constancy as ss\to\infty implies that BB is the eventual value, while eventual constancy as ss\to-\infty implies that CC is that eventual value. In the latter case it simplifies things with no essential loss of generality to end with

A 1B 1B 0 B 0B 00 000 \array{ \vdots \\ A_{1} \to B_{1} \to B_0\\ B_0 \to B_{0} \to 0 \\ 0 \to 0 \to 0 \\ \vdots }

so that C=0C=0 and the A sA_s‘s are the only “ingredients” of BB (with A 0=B 0A_0 = B_0). I’m going to focus mostly on the case where this holds and the sequence is also eventually constant in the other direction, so we have only finitely many extensions. In this case it’s easy to draw some of the same sorts of conclusions as in a single extension, e.g. B=0B=0 if and only if all A s=0A_s=0, and so on; the general case is sometimes trickier but often works out, although “lim 1\lim^1” terms start to pop up.

It’s more common to describe iterated extensions in terms of filtrations. From any iterated extension as above, we have a sequence of subgroups

F sBF s1BB \cdots \subseteq F_s B \subseteq F_{s-1} B \subseteq \cdots \subseteq B

where F sBF_s B is the kernel of the projection BB sB \to B_s. Since this projection is surjective, we have B s=B/F sBB_s = B/F_s B, and hence A s=F s1B/F sBA_s = F_{s-1} B/F_s B. Thus, the whole iterated extension can be recovered from the filtration:

F sB/F s+1BB/F s+1BB/F sB F s1B/F sBB/F sBB/F s1B \array{ \vdots\\ F_s B / F_{s+1} B \to B / F_{s+1}B \to B/F_s B\\ F_{s-1} B / F_{s} B \to B / F_{s}B \to B/F_{s-1} B\\ \vdots }

One problem with this point of view is that just having a filtration doesn’t ensure that BB is the limit lim sB/F sB\lim_s B/ F_s B. When this is the case, one says that the filtration is complete and Hausdorff. (As you might guess, these words refer to a uniformity induced on BB by the filtration.) The other condition we might want is that C=B/ sF sBC = B / \bigcup_s F_s B is zero, i.e. that sF sB=B\bigcup_s F_s B = B; a filtration with this property is called exhaustive. For finite iterated extensions, however, these conditions are all automatic.

A more serious problem with the filtration point of view is that it relies on the fact that the quotient of the kernel of a surjection is that same surjection — otherwise we couldn’t recover B sB_s from F sBF_s B. This is no longer true when we replace abelian groups by pointed spaces and extensions by fibration sequences. Thus, in that case we have to consider instead an iterated fibration sequence, consisting of a sequence of fibration sequences:

X s+1Y s+1Y s X sY sY s1 X s1Y s1Y s2 \array{ \vdots \\ X_{s+1} \to Y_{s+1} \to Y_s\\ X_s \to Y_s \to Y_{s-1}\\ X_{s-1} \to Y_{s-1} \to Y_{s-2}\\ \vdots }

As before, we view this as expressing the limit Y:lim s(Y s+1Y s)Y :\equiv \lim_s (\cdots \to Y_{s+1}\to Y_s \to \cdots) as put together out of the X sX_s‘s. It’s more common to describe this as a tower of fibrations

Y s+1Y sY s1 \cdots \to Y_{s+1}\to Y_s \to Y_{s-1} \to \cdots

since X sX_s is determined as the (homotopy) fiber of the map Y sY s1Y_s \to Y_{s-1}. But by talking about iterated extensions instead of filtrations, and iterated fibration sequences instead of towers of fibrations, we can see the analogy much more easily.

(If we were working with spectra instead of spaces, then from an iterated fibration sequence we could define a “filtration” of the limit YY, where F sYF_s Y is the fiber of the map YY sY\to Y_s. Then Y sY_s would be the cofiber of F sYYF_s Y \to Y. However, F sYYF_s Y \to Y would not necessarily be “injective” in any sense.)

The goal now is to extract some algebraic relationship among the groups π n(X s)\pi_n(X_s) and π n(Y)\pi_n(Y) in an iterated fibration sequence, which relate to iterated extensions just as LES’s relate to extensions. Of course, the first thing we get is a sequence of LES’s:

π n(X s+1)π n(Y s+1)π n(Y s)π n1(X s+1) π n(X s)π n(Y s)π n(Y s1)π n1(X s) \array{ \vdots\\ \cdots \to \pi_n(X_{s+1}) \to \pi_n(Y_{s+1}) \to \pi_n(Y_s) \to \pi_{n-1}(X_{s+1}) \to \cdots \\ \cdots \to \pi_n(X_{s}) \to \pi_n(Y_{s}) \to \pi_n(Y_{s-1}) \to \pi_{n-1}(X_{s}) \to \cdots \\ \vdots }

These sequences are related in that each group π n(Y s)\pi_n(Y_s) appears in two of them. This enables us to construct the following composite “connecting maps”

π n(X s)π n(Y s)π n1(X s+1). \pi_n(X_s) \to \pi_n(Y_s) \to \pi_{n-1}(X_{s+1}).

relating the homotopy groups of the fibers X sX_s. For reasons that will become clear later, we’ll call these maps d 2d^2 (note that this does not mean the square of a map dd; the superscript 22 is just an index). The first interesting thing we notice about them is that they satisfy d 2d 2=0d^2 \circ d^2 = 0, since in the composite

π n(X s)π n(Y s)π n1(X s+1)π n1(Y s+1)π n2(X s+2) \pi_n(X_s) \to \pi_n(Y_s) \to \pi_{n-1}(X_{s+1}) \to \pi_{n-1}(Y_{s+1}) \to \pi_{n-2}(X_{s+2})

the middle two maps are adjacent in a LES, hence compose to 00. Thus, for every value of n+sn+s, we have a chain complex

d 2π n(X s)d 2π n1(X s+1)d 2π n2(X s+2)d 2. \cdots \xrightarrow{d^2} \pi_n(X_s) \xrightarrow{d^2} \pi_{n-1}(X_{s+1}) \xrightarrow{d^2} \pi_{n-2}(X_{s+2}) \xrightarrow{d^2} \cdots.

Of course, if we’re experienced homological-algebraists, the first thing that we want to do with a chain complex is take its homology, but let’s step back a second to make sure that that’s a sensible thing to do.

A cycle in this chain complex is an element xπ n(X s)x\in \pi_n(X_s) that becomes zero in π n1(X s+1)\pi_{n-1}(X_{s+1}). This means that when we map xx into π n(Y s)\pi_n(Y_s), it lands in the kernel of π n(Y s)π n1(X s+1)\pi_n(Y_s) \to \pi_{n-1}(X_{s+1}). But since the sequence

π n(X s+1)π n(Y s+1)π n(Y s)π n1(X s+1) \cdots \to \pi_n(X_{s+1}) \to \pi_n(Y_{s+1}) \to \pi_n(Y_s) \to \pi_{n-1}(X_{s+1}) \to \cdots

is exact, that means exactly that the image of xx in π n(Y s)\pi_n(Y_s) lies in the image of π n(Y s+1)\pi_n(Y_{s+1}). In other words, an element xπ n(X s)x\in \pi_n(X_s) automatically gives us an element of π n(Y s)\pi_n(Y_s), while d 2(x)d^2(x) is precisely the “obstruction” to lifting that to an element of π n(Y s+1)\pi_n(Y_{s+1}). This naturally seems like the “first step” towards lifting it to an element of π n(Y)\pi_n(Y), which is what we’re really interested in.

Similarly, a boundary in this chain complex is an element of π n(X s)\pi_n(X_s) that’s in the image of π n+1(X s1)\pi_{n+1}(X_{s-1}), and hence in particular in the image of π n+1(Y s1)\pi_{n+1}(Y_{s-1}). But since the sequence

π n+1(Y s1)π n(X s)π n(Y s)π n(Y s1) \cdots \to \pi_{n+1}(Y_{s-1}) \to \pi_n(X_{s}) \to \pi_n(Y_{s}) \to \pi_n(Y_{s-1}) \to \cdots

is exact, any such element must map to zero in π n(Y s)\pi_n(Y_{s}), and hence also lift to zero in π n(Y s+1)\pi_n(Y_{s+1}). So the homology at π n(X s)\pi_n(X_s) (the group of cycles modulo the group of boundaries) is indeed a reasonable “second approximation” to “what we can learn about π n(Y)\pi_n(Y) from π n(X s)\pi_n(X_s)”.

For a “third approximation”, we can more or less repeat the process. Given something in this homology “H n,s(π *(X *))H_{n,s}(\pi_\ast(X_\ast))”, we can lift it to π n(Y s+1)\pi_n(Y_{s+1}), then map it into π n1(X s+2)\pi_{n-1}(X_{s+2}). The result is not well-defined because the lift is not well-defined, but its indeterminacy is precisely that of the lift, which by exactness is just an element of π n(X s+1)\pi_n(X_{s+1}). Thus, we do have a well-defined element of the quotient of π n1(X s+2)\pi_{n-1}(X_{s+2}) by the image of d 2d^2, which happens to also lie in the kernel of d 2d^2, and hence a map d 3:H n,s(π *(X *))H n1,s+2(π *(X *))d^3 : H_{n,s}(\pi_\ast(X_\ast)) \to H_{n-1,s+2}(\pi_\ast(X_\ast)). I’ll leave it to you to check that these maps make H n,s(π *(X *))H_{n,s}(\pi_\ast(X_\ast)) into another chain complex, and that elements of its homology can be lifted to π n(Y s+2)\pi_n(Y_{s+2}).

In order to describe these higher approximations uniformly, let’s introduce a bit more terminology. Recall that if GG is an abelian group, then a GG-graded abelian group is just a family (A g) gG(A_g)_{g\in G} of abelian groups indexed by the underlying set of GG. If AA and BB are GG-graded abelian groups and hGh\in G, then a degree-hh map f:ABf:A\to B consists of maps f g:A gB g+hf_g : A_g \to B_{g+h} for all gg. The composite of a degree-h 1h_1 map with a degree-h 2h_2 map is a degree-(h 1+h 2)(h_1+h_2) map. For example, an unbounded chain complex may be defined as a \mathbb{Z}-graded abelian group equipped with a degree-1 (or degree-(1)(-1)) endomap dd such that dd=0d \circ d = 0 (an equality of maps of degree 2 or (2)(-2)).

Now, the groups π n(X s)\pi_n(X_s) and π n(Y s)\pi_n(Y_s) can be assembled into a pair of (×)(\mathbb{Z}\times \mathbb{Z})-graded abelian groups DD and EE, and three maps between them ii, jj, and kk. The obvious grading is by nn and ss, but for historical reasons, I’m going to choose a different basis of ×\mathbb{Z}\times \mathbb{Z}, and write (p,q)(p,q) for the indexing elements.

E p,q:π p+q(X q) E_{p,q} :\equiv \pi_{p+q}(X_q)
D p,q:π p+q(Y q) D_{p,q} :\equiv \pi_{p+q}(Y_q)

If p+q<0p+q\lt 0, then by convention we set π p+q=0\pi_{p+q}=0 (unless we are working with spectra, in which case no special convention is needed). Now each long exact sequence

π n(X s)π n(Y s)π n(Y s1)π n1(X s) \cdots \to \pi_n(X_{s}) \to \pi_n(Y_{s}) \to \pi_n(Y_{s-1}) \to \pi_{n-1}(X_{s}) \to \cdots

can be rewritten as

E ns,sk ns,sD ns,si ns,sD ns+1,s1j ns+1,s1E ns1,s \cdots \to E_{n-s,s} \xrightarrow{k_{n-s,s}} D_{n-s,s} \xrightarrow{i_{n-s,s}} D_{n-s+1,s-1} \xrightarrow{j_{n-s+1,s-1}} E_{n-s-1,s} \to \cdots

Together, the maps in these LES’s assemble into three graded maps

D i D k j E\array{ D & & \xrightarrow{i} & & D\\ & _{k}\nwarrow & & \swarrow_j\\ && E }

where ii, jj, and kk have degrees (1,1)(1,-1), (2,1)(-2,1), and 00 respectively. Moreover, the exactness of the LES’s implies that this triangle is exact at each vertex. This structure (two graded groups DD and EE and maps i:DDi:D\to D, j:DEj:D\to E, and k:EDk:E\to D of some degrees such that the above triangle is exact at each vertex) is called an exact couple.

Now we can formalize the above process of successive approximation through passage to homology as follows. Given any exact couple (D,E,i,j,k)(D,E,i,j,k), we construct a new derived exact couple as follows.

  • The composite d:jk:EEd :\equiv j k : E \to E satisfies dd=jkjk=0d d = j k j k = 0, so we can define E:ker(d)/im(d)E' :\equiv ker(d)/im(d) to be its homology.
  • Let D=im(i)DD' = im(i) \subseteq D. (Of course, both of these should be interpreted “degreewise”, remembering that ii and dd may have nonzero degrees.)
  • Let i:DDi':D'\to D' be the restriction of ii to DD' (which obviously lands inside DD').
  • Define j:DEj':D'\to E' as follows. Given xDx\in D', we have x=i(y)x = i(y) for some yDy\in D; let j(x)j'(x) be the homology class determined by j(y)j(y) (which is a cycle since kj=0k j = 0). This is well-defined since if x=i(y)x = i(y') as well, then i(yy)=0i(y-y') = 0, hence yy=k(z)y-y' = k(z) for some zEz\in E, and thus j(y)j(y)=d(z)j(y) - j(y') = d(z) is a boundary.
  • Define k:EDk':E'\to D' by restricting kk to ker(d)ker(d) (which lands inside DD' since if d(x)=j(k(x))=0d(x) = j(k(x)) = 0, then k(x)k(x) lies in the image of ii by exactness) and then passing to the quotient (which is well-defined since kj=0k j = 0).
  • I’ll leave it as an exercise to check the exactness of ii', jj', and kk'. Note that deg(i)=deg(i)deg(i') = deg(i) and deg(k)=deg(k)deg(k')=deg(k), but deg(j)=deg(j)deg(i)deg(j')=deg(j) - deg(i).

We can thus iterate this process. We write (D r,E r,i r,j r,k r)(D^r,E^r,i^r,j^r,k^r) for the exact couple obtained by r2r-2 iterations. In particular, we have graded abelian groups E rE^r, each of which is equipped with a differential d r:E rE rd^r : E^r \to E^r of degree deg(j)+deg(k)(r2)deg(i)deg(j) + deg(k) - (r-2)\cdot deg(i) satisfying dd=0d\circ d = 0, and such that E r+1E^{r+1} is the homology of (E r,d)(E^r,d). This structure is called a spectral sequence.

Note that I’ve chosen the indexing so that E 2E^2 is the graded group EE we started with. Like the change from (n,s)(n,s) to (p,q)(p,q), this is to match the convention used in the literature. (And that, in turn, is because some other ways of constructing spectral sequences begin with an E 1E^1 whose homology is E 2E^2. And that, I guess, is because someone a long time ago thought that the natural numbers started with 11, since I’ve never heard of an “E 0E^0”. Although no doubt someone in the comments will point out a spectral sequence that starts with E 0E^0.)

When the groups in a spectral sequence are (×)(\mathbb{Z}\times\mathbb{Z})-graded, as in our example and in most cases, it is usual to draw them in a lattice on the plane, with pp the horizontal coordinate and qq the vertical one. For instance, E 2E^2 can be drawn like this:

E 1,2 2 E 0,2 2 E 1,2 2 E 2,2 2 E 1,1 2 E 0,1 2 E 1,1 2 E 2,1 2 E 1,0 2 E 0,0 2 E 1,0 2 E 2,0 2 E 1,1 2 E 0,1 2 E 1,1 2 E 2,1 2 \array{ & \vdots & \vdots & \vdots & \vdots & \\ \cdots & E_{-1,2}^2 & E_{0,2}^2 & E_{1,2}^2 & E_{2,2}^2 & \cdots\\ \cdots & E_{-1,1}^2 & E_{0,1}^2 & E_{1,1}^2 & E_{2,1}^2 & \cdots\\ \cdots & E_{-1,0}^2 & E_{0,0}^2 & E_{1,0}^2 & E_{2,0}^2 & \cdots\\ \cdots & E_{-1,-1}^2 & E_{0,-1}^2 & E_{1,-1}^2 & E_{2,-1}^2 & \cdots\\ & \vdots & \vdots & \vdots & \vdots & }

We call this the E 2E^2 page of the spectral sequence. When the degrees of the differentials are as they are in our example (which is, again, the most common situation), we can draw the differential d 2d^2 on this lattice as moving two steps left and one step up. The best picture I’ve been able to find of this online is here, although it’s of the dual “cohomologically indexed” case where the arrows go down and right instead of up and left.

Just to keep ourselves a bit more grounded, here’s what the E 2E^2 page looks like in the case of an iterated fibration sequence of spaces:

π 1(X 2) π 2(X 2) π 3(X 2) π 4(X 2) π 0(X 1) π 1(X 1) π 2(X 1) π 3(X 1) 0 π 0(X 0) π 1(X 0) π 2(X 0) 0 0 0 0 \array{ & \vdots & \vdots & \vdots & \vdots & \\ \cdots & \pi_1(X_2) & \pi_2(X_2) & \pi_3(X_2) & \pi_4(X_2) & \cdots\\ \cdots & \pi_0(X_1) & \pi_1(X_1) & \pi_2(X_1) & \pi_3(X_1) & \cdots\\ \cdots & 0 & \pi_0(X_0) & \pi_1(X_0) & \pi_2(X_0) & \cdots\\ \cdots & 0 & 0 & 0 & 0 & \cdots\\ & \vdots & \vdots & \vdots & \vdots & }

With spectra, the zero groups above would be replaced by negative homotopy groups such as π 1(X 0)\pi_{-1}(X_0), etc.

We then obtain the E 3E^3 page by replacing each entry E pq 2E^2_{p q} of the E 2E^2 page by the homology of d 2d^2 at that spot, i.e. the kernel of the outgoing differential modulo the image of the incoming one. The E 3E^3 page then has its own differential d 3d^3 which goes three steps left and two steps up, and we repeat. We then “take the limit” of E rE^r as rr\to\infty, and hope that the resulting “E E^\infty” terms are useful — in our example, we hope they tell us something about the groups π n(Y)\pi_n(Y).

First of all, we have to address the question of what it means to “take the limit”, since in general E r+1E^{r+1} is neither a subobject nor a quotient object of E rE^r, but a subquotient (a quotient of a subobject, or equivalently a subobject of a quotient). One can make sense of this in general, but in many (perhaps most) applications of spectral sequences, there’s a much simpler answer. Namely, it often happens that for each grading (p,q)(p,q), the groups E pq rE^r_{p q} eventually stabilize as rr\to\infty, so that we can define E pq E^\infty_{p q} to be their eventual value. (The rr at which this happens generally depends on (p,q)(p,q), so that interesting things are still happening somewhere in E rE^r for arbitrarily large values of rr.)

Of course, having E pq r+1=E pq rE^{r+1}_{p q} = E^r_{p q} means that the differentials coming into and out of E pq rE^r_{p q} are zero, and a good reason for this is if their domain and codomain are respectively the zero group. Note that when the differentials have the usual degrees, they always move from one diagonal p+q=np+q=n to the next lower one p+q=n1p+q=n-1. Thus, if each diagonal in the E 2E^2 page (hence also in every other page) contains only finitely many nonzero groups, then the groups E pq rE^r_{p q} will eventually stabilize for each (p,q)(p,q).

In particular, this is the case in the example arising from a finite iterated fibration sequence, where the nonzero part of the spectral sequence lives entirely in a finite strip 0qQ0\le q\le Q. It’s also the case for a bounded above fibration sequence (which stabilizes above some point s=Ts=T but extends infinitely downwards) as long as for every nn, there is a point below which π n(X s)=π n(Y s)=0\pi_n(X_s) = \pi_n(Y_s)=0, such as if the truncatedness of Y sY_s decreases, or their connectedness increases, as ss\to-\infty. In this case, we have the following.

Convergence Theorem: Suppose given a bounded-above iterated fibration sequence

X TY TY T1 X sY sY s1 X s1Y s1Y s2 \array{ X_{T} \to Y_{T} \to Y_{T-1}\\ \vdots \\ X_s \to Y_s \to Y_{s-1}\\ X_{s-1} \to Y_{s-1} \to Y_{s-2}\\ \vdots }

such that for every nn, there is an RR such that π n(X s)=π n(Y s)=0\pi_n(X_s) =\pi_n(Y_s)=0 for sRs\le R, and let Y=lim sY s=Y TY = \lim_s Y_s = Y_T. Then for every nn, there is a finite iterated extension:

E nT,T B n,TB n,T1 E ns,s B n,sB n,s1 E ns+1,s1 B n,s1B n,s2 E nR,R B n,R0\array{ E^\infty_{n-T,T} \to B_{n,T} \to B_{n,T-1}\\ \vdots \\ E^\infty_{n-s,s} \to B_{n,s} \to B_{n,s-1}\\ E^\infty_{n-s+1,s-1} \to B_{n,s-1} \to B_{n,s-2}\\ \vdots\\ E^\infty_{n-R,R} \to B_{n,R} \to 0 }

such that B n=lim sB n,s=B n,TB_n = \lim_s B_{n,s}= B_{n,T} is equal to π n(Y)\pi_n(Y).

This theorem makes our second analogy also into a functor between suitable categories of iterated fibration sequences and iterated extensions.

Note that the E E^\infty groups appearing in the iterated extension for π n(Y)\pi_n(Y) are those on the diagonal p+q=np+q=n. Thus, the theorem says that when YY is put together out of the X sX_s‘s, then π n(Y)\pi_n(Y) is put together out of the groups on this diagonal, which are computed from the homotopy groups of the X sX_s’s in some way (encoded by the spectral sequence). It’s traditional to write this sort of “convergence” as

E p,q 2=π p+q(X q)π p+q(Y) E^2_{p,q} = \pi_{p+q}(X_q) \;\Rightarrow\; \pi_{p+q}(Y)

to indicate which E E^\infty groups are the “ingredients” of which group in the target.

At this point I should remind you that we’re either assuming all spaces are simply connected, or working with spectra instead of spaces. The notion of “convergence” is a lot trickier when you have to deal with nonabelianness of π 1\pi_1 and nongroupness of π 0\pi_0. There are also fancier convergence theorems that allow more infinite behavior, such as when E pq rE^r_{p q} doesn’t stabilize but still has a “limit”. Finally, with an unbounded-above iterated fibration sequence we would also have to deal with the fact that π n(lim sY s)\pi_n(\lim_s Y_s) may not equal lim sπ n(Y s)\lim_s \pi_n(Y_s).

Proof of convergence theorem: For any (p,q)(p,q), let rmax(Tq+3,qR+1)r \ge max(T-q+3,q-R+1). Then E pq rE^r_{p q} has stabilized, so that E pq =E pq rE^\infty_{p q} = E^r_{p q}. For such an rr, D pq rD^r_{p q} is the (r2)(r-2)-fold image of i:D 2D 2i:D^2\to D^2, i.e. those elements in D 2D^2 of the form i(i(i(x)))i(i(\cdots i(x)\cdots )) with (r2)(r-2) copies of ii. Since ii consists of the maps π n(Y s)π n(Y s1)\pi_n(Y_s) \to \pi_n(Y_{s-1}), and π n(Y s)=π n(Y)\pi_n(Y_s) = \pi_n(Y) for sTs\ge T, this means D pq rD^r_{p q} is the image of π p+q(Y)\pi_{p+q}(Y) in π p+q(Y q)\pi_{p+q}(Y_q) (and in particular is independent of rr sufficiently large). Let B n,s=D ns,s rB_{n,s}= D^r_{n-s,s} for any such rr, i.e. the image of π n(Y)\pi_n(Y) in π n(Y s)\pi_n(Y_s).

It remains to construct the extensions E ns,s B n,sB n,s1E^\infty_{n-s,s} \to B_{n,s} \to B_{n,s-1} displayed above. However, just as we put together the exact couple (D 2,E 2,i 2,j 2,k 2)(D^2,E^2,i^2,j^2,k^2) from long exact sequences, from the exact couple (D r,E r,i r,j r,k r)(D^{r},E^{r},i^{r},j^{r},k^{r}) we can extract some other long exact sequences. Note that by iterating the above formulas for degrees in a derived exact couple, we have deg(i r)=(1,1)deg(i^{r}) = (1,-1) and deg(k r)=0deg(k^{r}) = 0, but deg(j r)=(r,r1)deg(j^{r}) = (-r,r-1). Thus, we have LES’s

D p+r,qr+1 rjE p,q rkD p,q riD p+1,q1 rjE pr+1,q+r2 r \cdots \to D^{r}_{p+r,q-r+1} \xrightarrow{j} E^{r}_{p,q} \xrightarrow{k} D^{r}_{p,q} \xrightarrow{i} D^{r}_{p+1,q-1} \xrightarrow{j} E^{r}_{p-r+1,q+r-2} \to\cdots

If we choose rmax(Ts+4,sR+1)r \ge max(T-s+4,s-R+1), then all three terms in the middle have stabilized, while the two on the ends are zero. Thus, inside this LES we have a short exact sequence

0E ns,s B n,sB n,s100 \to E^\infty_{n-s,s} \to B_{n,s} \to B_{n,s-1} \to 0

which is the extension that we wanted. \Box

This is all very abstract, so let’s look at a couple of degenerate cases. First, in the case of a finite iterated fibration sequence with T=1T=1, we have

X 1YX 0 X 0X 0*\array{ X_1 \to Y \to X_0\\ X_0 \to X_0 \to \ast }

hence essentially just a single fibration sequence. The spectral sequence is confined to the strip q{0,1}q\in \{0,1\}, with E 2E^2 page looking like:

π 0(X 1) π 1(X 1) π 2(X 1) π 3(X 1) 0 π 0(X 0) π 1(X 0) π 2(X 0) \array{ \cdots & \pi_0(X_1) & \pi_1(X_1) & \pi_2(X_1) & \pi_3(X_1) & \cdots \\ \cdots & 0 & \pi_0(X_0) & \pi_1(X_0) & \pi_2(X_0) & \cdots }

The differentials on this page go, as always, left two and up one, hence from π n(X 0)π n1(X 1)\pi_n(X_0) \to \pi_{n-1}(X_1); these are exactly the “connecting maps” δ n\delta_n in the ordinary LES of the fibration. Since the differentials entering π n(X 0)\pi_n(X_0) come from zero, and those leaving π n(X 1)\pi_n(X_1) go to zero, on passage to homology we get the E 3E^3 page

im(δ 1) im(δ 2) im(δ 3) im(δ 4) 0 ker(δ 0) ker(δ 1) ker(δ 2) \array{ \cdots & im(\delta_1) & im(\delta_2) & im(\delta_3) & im(\delta_4) & \cdots \\ \cdots & 0 & ker(\delta_0) & ker(\delta_1) & ker(\delta_2) & \cdots }

We have E 3=E E^3 = E^\infty since all the remaining differentials hit zero on one side or the other, so that E p,0 =ker(δ p)E^\infty_{p,0} = ker(\delta_p) and E p,1 =im(δ p+2)E^\infty_{p,1} = im(\delta_{p+2}). The theorem then gives an iterated extension

im(δ n+1)π n(Y)ker(δ n) ker(δ n)ker(δ n)0 \array{ im(\delta_{n+1}) \to \pi_n(Y) \to ker(\delta_n)\\ ker(\delta_n) \to ker(\delta_n) \to 0 }

which is just the ordinary extension we observed above as coming from an LES.

Another degenerate case is when the iterated fibration sequence is the Postnikov tower of a space (or spectrum) YY. Suppose YY is an mm-type, i.e. π n(Y)=0\pi_n(Y)=0 for n>mn\gt m. Then for any nmn\le m we have an nn-type Y n{\Vert Y\Vert}_n, with fibration sequences

X nY nY n1 X_n \to {\Vert Y\Vert}_n \to {\Vert Y\Vert}_{n-1}

where X n=K(π n(Y),n)X_n = K(\pi_n(Y),n) is an Eilenberg-Mac Lane space, with π n(X n)=π n(Y)\pi_n(X_n) = \pi_n(Y) and π i(X n)=0\pi_i(X_n) = 0 for ini\neq n. Together these form an iterated fibration sequence with limit YY. When YY is an mm-type space, it is a finite sequence; when YY is an mm-type spectrum it is bounded above and satisfies the condition on downward homotopy groups; thus the convergence theorem applies. Since each fiber X nX_n is an Eilenberg-Mac Lane space of dimension nn, the E 2E^2 page of the spectral sequence is concentrated on the line p=0p=0, looking like this:

π 2(Y) π 1(Y) π 0(Y) \array{ \vdots \\ \pi_2(Y)\\ \pi_1(Y) \\ \pi_0(Y)\\ \vdots }

There is no room for any nontrivial differentials, E 2=E E^2=E^\infty, and for each nn we obtain the trivial iterated extension

0π n(Y)π n(Y) 0π n(Y)π n(Y) π n(Y)π n(Y)0 000 000.\array{ 0 \to \pi_n(Y) \to \pi_n(Y) \\ \vdots\\ 0 \to \pi_n(Y) \to \pi_n(Y) \\ \pi_n(Y) \to \pi_n(Y) \to 0 \\ 0 \to 0 \to 0 \\ \vdots\\ 0 \to 0 \to 0. }

Of course, the interesting applications of spectral sequences are less trivial, but this post is already quite long enough. In the companion post on the HoTT blog, I’ll talk about how to use this spectral sequence (with spectra) to extract versions of the Atiyah-Hirzebruch and Serre spectral sequences, and see what they can do for us.

One final teaser: note that while the groups in the E r+1E^{r+1} page of a spectral sequence are determined by the groups and the differentials in the E rE^r page, the differential in the E r+1E^{r+1} page is not so determined. To figure out what it is, we need to know about the rest of the r thr^{\mathrm{th}} exact couple, which can be tedious to work out. In many applications it suffices to know that such a differential exists, without knowing anything about it; but sometimes the values of the differential do matter. However, if we had a fully constructive definition of the whole exact couple and spectral sequence, as we would obtain by implementing the definition in a hypothetical fully constructive version of homotopy type theory, then the definition would be a program, and we could simply ask the computer to evaluate it on any input we cared about. This suggests to me a vague possibility of a way that homotopy type theory might conceivably one day be useful even to the “working algebraic topologist”.

Spectral Sequences in HoTT

Now we want to construct the cohomological Serre spectral sequence of a fibration (i.e. a type family). First recall that a spectrum is a family of pointed types Y:Type * Y : \mathbb{N} \to \mathsf{Type}_\ast such that Y n=ΩY n+1 Y_n = \Omega Y_{n+1} for all nn. Last time I defined the cohomology of a type XX with coefficients in a spectrum YY to be

H n(X;Y):XΩ knY k 0 H^n(X;Y) :\equiv \Vert X \to \Omega^{k-n} Y_k \Vert_0

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

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

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

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

for any n n \in \mathbb{Z} and any kk sufficiently large that n+k0 n+k\ge 0. Again, the definition of a spectrum makes this independent of kk. 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: (n:)Y nZ n f : \prod_{(n:\mathbb{N})} Y_n \to Z_n such that the evident squares commute relating it to the equivalences Y n=ΩY n+1 Y_n = \Omega Y_{n+1} and Z n=ΩZ n+1 Z_n = \Omega Z_{n+1}. Similarly, the fiber of such a map is defined levelwise, with fib(f) n:fib(f n) \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 fib(f n)Y nZ n \mathsf{fib}(f_n) \to Y_n \to Z_n splice together into a long exact sequence

π n(fib(f))π n(Y)π n(Z) \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 above, I explained how from an iterated fibration sequence

X s+1Y s+1Y s X sY sY s1 X s1Y s1Y s2 \array{\vdots \\ X_{s+1} \to Y_{s+1} \to Y_s\\ X_s \to Y_s \to Y_{s-1}\\ X_{s-1} \to Y_{s-1} \to Y_{s-2}\\ \vdots}

we obtain a spectral sequence with E pq 2=π p+q(X q) E^2_{p q} = \pi_{p+q}(X_q). Moreover, if the iterated fibration sequence stabilizes as s s\to \infty (i.e. for s>T s\gt T it becomes 1YY \mathbf{1} \to Y \to Y) and eventually becomes zero at each homotopy group separately as s s \to -\infty, then this spectral sequence “converges” to the homotopy groups of YY, in the sense that for each nn we have a finite iterated extension

E nT,T π n(Y)B n,T1 E ns,s B n,sB n,s1 E ns+1,s1 B n,s1B n,s2 E nR,R E nR,R 0\array{ E^\infty_{n-T,T} \to \pi_n(Y) \to B_{n,T-1}\\ \vdots\\ E^\infty_{n-s,s} \to B_{n,s} \to B_{n,s-1}\\ E^\infty_{n-s+1,s-1} \to B_{n,s-1} \to B_{n,s-2} \\ \vdots\\ E^\infty_{n-R,R} \to E^\infty_{n-R,R} \to 0 }

in which the E E^\infty terms occurring are precisely the nonzero ones on the diagonal p+q=n p+q=n of the E 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 p,q 2=π p+q(X q)π p+q(Y) E^2_{p,q} = \pi_{p+q}(X_q) \Rightarrow \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 YY:

K(π s(Y),s)Y sY s1 K(π s1(Y),s1)Y s1Y s2 \array{ K(\pi_s(Y),s) \to {\Vert Y\Vert}_s \to {\Vert Y\Vert}_{s-1}\\ K(\pi_{s-1}(Y),s-1) \to {\Vert Y\Vert}_{s-1} \to {\Vert Y\Vert}_{s-2}\\ \vdots }

If YY is an mm-type for some m< m\lt \infty, then this satisfies our simple hypotheses for convergence. A spectrum also has a Postnikov tower, with (Y s) n (\Vert Y \Vert_s)_n defined to be Y n n+s \Vert Y_n\Vert_{n+s}. This makes sense for any s s \in \mathbb{Z}, as long as we make the convention that X m=1 \Vert X\Vert_{m} = \mathbf{1} if m<1 m \lt -1. If we define an mm-type spectrum to be one for which Y n Y_n is an ordinary (n+m) (n+m)-type for all nm2 n \ge -m-2, then the Postnikov tower of such a YY also satisfies our simple hypotheses for convergence despite potentially being infinite downwards (an mm-type spectrum can have nontrivial π n \pi_n for all <nm -\infty \lt 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 XX and spectrum YY we have an induced iterated fibration sequence

SpMap(X,K(π s(Y),s))SpMap(X,Y s)SpMap(X,Y s1) SpMap(X,K(π s1(Y),s1))SpMap(X,Y s1)SpMap(X,Y s2) \array{ \mathsf{SpMap}(X,K(\pi_s(Y),s)) \to \mathsf{SpMap}(X,{\Vert Y\Vert}_s) \to \mathsf{SpMap}(X,{\Vert Y\Vert}_{s-1}) \\ \mathsf{SpMap}(X,K(\pi_{s-1}(Y),s-1)) \to \mathsf{SpMap}(X,{\Vert Y\Vert}_{s-1}) \to \mathsf{SpMap}(X,{\Vert Y\Vert}_{s-2}) \\ \vdots }

where K(A,s) K(A,s) denotes the spectrum whose n th n^{\mathrm{th}} space is the usual Eilenberg-Mac Lane space K(A,s+n) K(A,s+n) if s+n0 s+n\ge 0, and contractible otherwise. Note that the spectrum K(A,0) K(A,0) is the Eilenberg-Mac Lane spectrum that we denoted HA H A last time.

Hence, we have a spectral sequence with

E pq 2 =π p+q(SpMap(X,K(π q(Y),q))) =π p(SpMap(X,H(π q(y))) =H p(X;π q(Y))\begin{aligned} E^2_{p q} &= \pi_{p+q}(\mathsf{SpMap}(X,K(\pi_q(Y),q)))\\ &= \pi_p(\mathsf{SpMap}(X,H(\pi_q(y)))\\ &= H^{-p}(X;\pi_q(Y)) \end{aligned}

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

This is called the Atiyah-Hirzebruch spectral sequence. It says that for any (sufficiently nice) spectrum YY, the cohomology of any type XX with coefficients in YY (what algebraic topologists call “generalized cohomology”) can be put together out of the “ordinary” cohomology of XX with coefficients in the homotopy groups of YY. One usually flips the sign of pp and qq in “cohomological” spectral sequences of this sort, simultaneously switching the subscripts and superscripts; thus we write instead

E 2 pq=H p(X;π q(Y))H p+q(X;Y) E_2^{p q} = H^p(X;\pi_{-q}(Y)) \Rightarrow 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 π q(Y)=H q(1;Y) \pi_{-q}(Y) = H^q(\mathbf{1};Y) is also the q th q^{\mathrm{th}} cohomology of a point with coefficients in YY.)

Of course, this may not seem very interesting unless you have some spectra up your sleeve other than HA 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 XX is a type and Y:XSpectrum Y : X \to \mathsf{Spectrum} is an XX-indexed family of spectra. We define the cohomology of XX with coefficients in YY to be

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

where SpSect(X,Y) \mathsf{SpSect}(X,Y) is the “spectrum of sections of YY” defined by SpSect(X,Y) n: (x:X)Y(x) n) \mathsf{SpSect}(X,Y)_n :\equiv \prod_{(x:X)} Y(x)_n). As usual with dependent function types, when YY 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:XAbGp A : X \to \mathsf{AbGp} is such, then composing it with the “Eilenberg-Mac Lane spectrum” function H:ApGpSpectrum H : \mathsf{ApGp}\to \mathsf{Spectrum} we obtain an XX-indexed family of spectra, HA H A. Note that since abelian groups are sets, AbGp \mathsf{AbGp} is a 1-type, and hence any such AA factors through X 1 \Vert X \Vert_1, the “fundamental groupoid” of XX. This is the homotopy-type-theory version of what classical algebraic topologists would call a local system on XX. If XX is pointed and connected, then X 1=K(π 1(X),1) \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 π 1(X) \pi_1(X), the most classical notion. The cohomology of XX with coefficients in HA 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 π n:Type *AbGp \pi_n : \mathsf{Type}_\ast \to \mathsf{AbGp} or π n:SpectrumAbGp \pi_n : \mathsf{Spectrum} \to \mathsf{AbGp} with any family Y:XType * Y : X \to \mathsf{Type}_\ast of pointed types or Y:XSpectrum 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:XSpectrum Y : X \to \mathsf{Spectrum}, obtaining an XX-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 π q(Y):XAbGp \pi_q(Y) : X \to \mathsf{AbGp}. Sinc SpSect \mathsf{SpSect}, like SpMap \mathsf{SpMap}, preserves fibration sequences, we get a more general Atiyah-Hirzebruch spectral sequence with E 2 pq=H p(X;π q(Y)) E^{p q}_2 = H^{p}(X;\pi_{-q}(Y)) (meaning the cohomology with local coefficients in the local system π q(Y) \pi_{-q}(Y)), which converges to H p+q(X;Y) H^{p+q}(X;Y) if YY is a family of mm-type spectra.

Now we’re ready to deduce the Serre spectral sequence. Let YY be an ordinary spectrum, such as HAH A, and let F:XType F : X \to \mathsf{Type} be a type family. Then xSpMap(F x,Y) x\mapsto \mathsf{SpMap}(F_x,Y) is an XX-indexed family of spectra, which are mm-type spectra if YY is. Thus, we have the above “parametrized” Atiyah-Hirzebruch spectral sequence:

H p(X;λx.π q(SpMap(F x,Y)))H p+q(X;λx.SpMap(F x,Y)). H^p(X;\lambda x.\pi_{-q}(\mathsf{SpMap}(F_x,Y))) \Rightarrow H^{p+q}(X;\lambda x.\mathsf{SpMap}(F_x,Y)).

On the left, we have π q(SpMap(F x,Y))=H q(F x;Y) \pi_{-q}(\mathsf{SpMap}(F_x,Y)) = H^q(F_x;Y) by definition. And as for the right side, we have

H n(X;λx.SpMap(F x,Y)) =π n(SpSect(X,λx.SpMap(F x,Y))) =π n(SpMap( (x:X)F x,Y)) =H n( (x:X)F x;F) \begin{aligned} H^n(X;\lambda x.\mathsf{SpMap}(F_x,Y)) &= \pi_{-n}(\mathsf{SpSect}(X,\lambda x.\mathsf{SpMap}(F_x,Y)))\\ &= \pi_{-n}(\mathsf{SpMap}(\sum_{(x:X)} F_x, Y))\\ &= H^n(\sum_{(x:X)}F_x;F) \end{aligned}

the cohomology of the total space of the fibration F with coefficients in YY. (The second step is a spectral version of the ordinary universal mapping property of Σ \Sigma-types, (( (x;X)F x)Z)= (x:X)(F xZ) ((\sum_{(x;X)} F_x) \to Z) = \prod_{(x:X)} (F_x \to Z).) Thus, our spectral sequence becomes

H p(X;λx.H q(F x;Y))H p+q( (x:X)F x;Y) H^p(X;\lambda x. H^q(F_x;Y)) \Rightarrow 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 XX is pointed and simply connected, so that X 1=1 \Vert X \Vert_1 = \mathbf{1}, then any local system on XX is constant, and so the cohomology with local coefficients in the domain reduces simply to the ordinary cohomology of XX 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 aS bS c S^a \to S^b \to S^c in which all three types are spheres of some dimension, and suppose that c>1 c\gt1 so that S c S^c is simply connected and that a>0 a\gt0 and b>0 b\gt0 for nontriviality. Then we have a Serre spectral sequence

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

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

On indexing choices

The “natural” indexing of the spectral sequence π n(X s)\pi_n(X_s) constructed above is by nn and ss, and in this indexing the initial differential has degree (1,1)(-1,1). We chose to reindex it by writing n=p+qn = p+q and s=qs=q, in which case the initial differential has (p,q)(p,q) degree (2,1)(-2,1), thereby matching the indexing and degrees for the E 2E_2 page of some known spectral sequences (such as the Serre and Atiyah-Hirzebruch SS).

However, there are other ways to do the reindexing. For instance, if we instead set n=tsn = t-s, then the initial differential will have (s,t)(s,t) degree (1,0)(1,0), which looks more like the E 1E_1 page of a spectral sequence. For instance, the Adams spectral sequence can be obtained in this way from a suitably chosen tower of fibrations (although usually in that case one talk about cofibers rather than fibers, which in the world of spectra are the same up to a furtherh degree shift). Thanks to Urs Schreiber for pointing this out.


Some notes not in the original blog posts:

  • In the section on Spectral Sequences on HoTT it is ambiguous whether SpMap(X,Y)\mathsf{SpMap}(X,Y) and SpSect(X,Y)\mathsf{SpSect}(X,Y) consists of pointed or unpointed maps. Most steps taken are true both when they are interpreted as pointed or as unpointed maps. If SpMap(X,Y)\mathsf{SpMap}(X,Y) is unpointed then XX is unpointed and π n(SpMap(X,Y))\pi_{-n} (\mathsf{SpMap}(X,Y)) is the unreduced cohomology of XX (with coefficients in YY). If SpMap(X,Y)\mathsf{SpMap}(X,Y) is pointed then XX is interpreted as a pointed type and π n(SpMap(X,Y))\pi_{-n} (\mathsf{SpMap}(X,Y)) is the reduced cohomology. Everything in the proof of the Atiyah-Hirzebruch spectral sequence holds for both cases, so the Atiyah-Hirzebruch spectral sequence exists for both reduced and unreduced cohomology. However, the Serre Spectral sequence is only valid for unreduced cohomology, since the equivalence

    SpSect(X,λx.SpMap(F x,Y))=SpMap( (x:X)F x,Y)\mathsf{SpSect}(X,\lambda x.\mathsf{SpMap}(F_x,Y)) = \mathsf{SpMap}(\sum_{(x:X)} F_x, Y)

    used in the proof is only true for unpointed maps.

  • Urs Schreiber has pointed out that this construction of the AHSS appears in C. R. F. Maunder (1963), who also shows that it agrees with the standard construction by constructing an isomorphism of exact couples. It seems likely that a similar method would work for the Serre SS.


Formalization in Lean:

category: homotopy theory

Last revised on January 1, 2024 at 13:48:47. See the history of this page for a list of all contributions to it.