Commit 2025-11-28 17:46 ae7605fb

feat(CategoryTheory/Triangulated): spectral objects (#31586) In this file, we introduce the category SpectralObject C ι of spectral objects in a pretriangulated category C indexed by the category ι, a notion introduced by Verdier in order to give a nice presentation of spectral sequences. In the short term, I intend to PR the construction of the spectral object consisting of all truncations of an object in a triangulated category equipped with a t-structure. In a more distant future, the analogous notion of spectral object in an abelian category shall be introduced, and spectral sequences will be constructed by combining two facts :

1. by applying an homological functor, a spectral object in a triangulated category can be transformed into a spectral object in an abelian category (easy)
2. spectral sequences are attached to spectral objects in abelian categories (very technical)