Spectral sequences

[Alizter]

Back in 2020 I wrote down a definition of spectral sequence in Mike's spectral branch:

https://github.com/HoTT/Coq-HoTT/commit/85774225b9319af566bca2b4be1d5ba0da42020f

it took values in abelian groups and it was based on Floris van Doorn's formalization and work on spectral sequences in HoTT.

Now that we have abelian categories #1929, I would like to rethink how we might define spectral sequences. One appealing idea is to follow this remark in the Stacks project.

Let $\mathcal{A}$ be an abelian category. Let $T_r$ be a sequence of isomorphisms $\mathcal A \to \mathcal A$. A spectral sequence is given by a sequence of objects $E_r$ of $\mathcal A$ together with a sequence of differentials $d_r : E_r \to T_r E_r$ such that $T_r d_r \circ dr = 0$ and $E{r+1} \cong \mathrm{Ker}(d_r)/\mathrm{Im}(T_r^{-1} d_r)$.

Now this definition is nice because it allows us to package up all the bureaucracy of integer gradings behind the equivalences. This is related to Floris' idea of successor structures, with the added condition that the successor can be inverted. This should reduce some of the technical debt of working with gradings hopefully.

Another advantage is that this definition is agnostic to the kind of grading we have available. In most cases, we will be interested in the bigraded case, but there are times when some leniency could prove useful.

I also observed an interesting fact that such a shift functor would give $\mathcal{A}$ the structure of a triangulated category. I don't know if it's useful to think about however.<\s>

[jdchristensen]

Interesting idea. I haven't tried to formalize anything about spectral sequences, so I don't know what the best approach is.

One minor comment about:

I also observed an interesting fact that such a shift functor would give A the structure of a triangulated category.

Abelian categories are very rarely triangulated, so this won't be true in general. (There's a lemma due to Verdier, stated at https://math.stackexchange.com/questions/189769/when-is-the-derived-category-abelian, which characterizes triangulated categories that are also abelian.)

[jdchristensen]

Just to add a bit more, in a triangulated category, every epimorphism has a section and every monomorphism has a retraction.

[Alizter]

I see where I was confused about the triangulated category. I was thinking about chain complexes in an abelian category forming a triangulated category with distinguished triangles given by exact sequences. This is however not at all true! The example I was misremembering was the homotopy category of chain complexes where you localize the quasiisomorphsims. Anyway, thanks for the correction. Let's drop this silly example from the discussion.

[Alizter]

Interesting idea. I haven't tried to formalize anything about spectral sequences, so I don't know what the best approach is.

One thing I learnt from Floris' attempt at formalising Serre spectral sequence is that the bureaucracy of integer arithmetic can get very heavy. I believe this is what motivated him to introduce successor structures.

[mikeshulman]

The definition using automorphisms $T_r$ does seem likely to lend itself well to a successor-structures version.

Another thing I've wondered about is whether, in this and other cases where the bureaucracy of integer arithmetic gets heavy, it could be improved by using a relational rather than functional definition of arithmetic. E.g. addition is

Inductive plus : nat -> nat -> nat -> Type :=
| plus_O : forall {n : nat}, plus n O n
| plus_S : forall {m n mn : nat}, plus m n mn -> plus m (S n) (S mn).

One advantage of this is that associativity can be phrased without any equalities: it says that if plus m n mn and plus mn p mnp and plus n p np, then also plus m np mnp. So there is no transport, but the cost of course is carrying around witnesses of plus in various places.

The reason this occurred to me is that I've recently been using this idiom a lot with type-level natural numbers in OCaml (for intrinsically well-scoped De Bruijn indices), where it is the only possibility since you can't define recursive functions on types, and I've been impressed by how cleanly things generally work out.