Spectral sequences

Stream: homology

[Joël Riou]

I have just completed draft code for a general machinery for spectral sequences. It is exactly what I outlined at the end of my Banff talk when @Filippo A. E. Nuccio asked me about the Grothendieck spectral sequence: use the constructions by Verdier in Des catégories dérivées des catégories abéliennes.

[Joël Riou]

The idea is to use the notion of spectral object in a triangulated category T (it consists of a bunch of objects and functorial distinguished triangles): a filtered cochain complex induces such a spectral object in the derived category, and I have also formalized the spectral object attached to a t-structure (it "contains" all the truncations of a given object). Then, when we apply a homological functor T ⥤ A (A is an abelian category) to such a spectral object, the distinguished triangles become long exact sequences and we get a spectral object in the abelian category A. Then, the hard part is to attach a spectral sequence to a spectral object in A. Up to a renumbering, it consists of beautiful as well as absurdly abstract and technical constructions: definition of the terms of all the pages, definition of the differentials, checking the compositions are zero, computing the homology, analysing convergence.

[Joël Riou]

This machinery should eventually be able to produce all the spectral sequences I know once the relevant specific definitions are introduced. For example, I already have a prototype of the Grothendieck spectral sequence of a composition of functors (it is stated for a composition of triangulated functors between derived categories, but once we have good notions for total derived functors, it will almost immediately give what is usually understood as the Grothendieck spectral sequence), see https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/SpectralSequence/Examples/Grothendieck.lean

[Johan Commelin]

Amazing!

[Adam Topaz]

Very nice! What's the relationship between such spectral objects and exact couples?

[Joël Riou]

@Adam Topaz: There might be slightly more information embedded in a spectral object as compared to an exact couple, but I am not completely sure.

[Adam Topaz]

I see. I'll take a look at the definition soon (but I have to give a talk in 13 mins)

[Kevin Buzzard]

I am a bit unclear about the role that derived categories have to play in mathematics now humans have invented the derived infinity-category. Is it still important to set up a theory of derived categories? If it gives us spectral sequences then it's definitely a useful tool :-)

[Matthew Ballard]

@Kevin Buzzard Bro?

[Kevin Buzzard]

Oh I'm serious :-) I don't know much about this stuff, but earlier this year Lenny Taelman gave some talks at Imperial and he was really down on the derived category, he said that triangulated categories were just a mess and infinity categories solved the problems.

[Kevin Buzzard]

But maybe he was just justifying the fact that he was going to lecture on infinity categories :-)

[Matthew Ballard]

• Not all triangulated categories arise as homotopy categories of stable infinity categories
• When they do, the utility of the $\infty$-perspective is mainly ease of use. People were already using enhancements to make the right constructions. Heck it is even implicitly in LTE.

[Joël Riou]

@Kevin Buzzard My guess is that in a stable infinity category, a "ℤ-indexed sequence of maps" (if this makes sense to anyone) should obviously induce a spectral object in the associated triangulated category, hence spectral sequences via Verdier's construction...