### 5.4.5 Examples of spectral sequences

The machinery for the construction of spectral sequences which was outlined above shows that in order to construct a spectral sequence in an abelian category $\mathcal{C}$, it suffices to provide two data:

* a homological functor $H^0 : \mathcal{T} \Rightarrow \mathcal{C}$,

* a spectral object $E$ in the triangulated category $\mathcal{T}$.

The main example of a homological functor is the homology functor attached to a $t$-structure, which obviously includes the functor $H^0 : D(\mathcal{C}) \Rightarrow \mathcal{C}$ when $\mathcal{C}$ is an abelian category. It is also important to note that if $H^0 : \mathcal{T} \Rightarrow \mathcal{C}$ is a homological functor, then for any triangulated functor $F : \mathcal{T}' \Rightarrow \mathcal{T}$, the composition $F \ggg H^0 : \mathcal{T}' \Rightarrow \mathcal{C}$ is also a homological functor.

In order to construct a spectral object in the derived category, we may use any filtration on a cochain complex. In particular, we may use the canonical filtration which is related to the spectral objects attached to $t$-structures (see 5.2.4), but we may also use the stupid filtration. Similarly, the total complex of a bicomplex may also be equipped with a filtration by the rows or by the columns.

I have completely formalized the following theorem, which is the Grothendieck spectral sequence for the composition of right derived functors:

**Theorem 5.4.5.1 ([Gro57, 2.4.1]).** Let $F : \mathcal{A} \to \mathcal{B}$ and $G : \mathcal{B} \to \mathcal{C}$ be additive functors between abelian categories. We assume that $\mathcal{A}$ and $\mathcal{B}$ have enough injectives. Moreover, we assume that for any injective object $I$ in $\mathcal{C}$, the object $F(I)$ is “acyclic” for $G$, i.e. the canonical map $G(F(I)) \to RG(F(I))$ is an isomorphism.<fnref n="21" />

Then, for any $X \in \mathcal{A}$, there is a first quadrant cohomological spectral sequence with first page $E_2^{p,q} \cong R^p G(R^q F(X))$ which converges to $R^{p+q}(F \ggg G)(X)$.

We apply the machinery of spectral sequences to the homological functor $RG \ggg H^0 : D^+(\mathcal{B}) \Rightarrow \mathcal{C}$ and the spectral object attached to $RF(X)$ using the canonical $t$-structure on $D^+(\mathcal{B})$. This spectral sequence converges to $H^{p+q}(RG(RF(X)))$, but the assumptions on $F$ and $G$ allow to show that the natural transformation $R(F \ggg G) \to RF \ggg RG$ is an isomorphism. It follows that there is a canonical isomorphism $R^{p+q}(F \ggg G)(X) \cong H^{p+q}(RG(RF(X)))$.

<figure><img src="image_49.png" /></figure>

<footnote n="21">²¹If $G$ is left exact, this means that $(R^p G)(F(I)) = 0$ for $p > 0$.</footnote>
References

[ABR08] J. Aransay, C. Ballarin, and J. Rubio. "A mechanized proof of the basic perturbation lemma". In: *J. Automat. Reason*. 40.4 (2008), pages 271–292. ISSN: 0168-7433,1573-0670. DOI: 10.1007/s10817-007-9094-x.

[Bei+18] A. A. Beilinson, J. Bernstein, P. Deligne, and O. Gabber. *Analyse et topologie sur les espaces singuliers. I : Faisceaux pervers*. Volume 100. Astérisque. Société Mathématique de France, Paris, 2018, 172 pages.

[Ber74] G. Bergman. "A note on abelian categories – translating element-chasing proofs, and exact embedding in abelian groups". 1974. URL: http://math.berkeley.edu/~gbergman/papers/unpub/elem-chase.pdf.

[Bor94] F. Borceux. *Handbook of categorical algebra*. 2. Volume 51. Encyclopedia of Mathematics and its Applications. Categories and structures. Cambridge University Press, Cambridge, 1994, xviii+443 pages. ISBN: 0-521-44179-X.

[Buz+22] K. Buzzard, C. Hughes, K. Lau, A. Livingston, R. Fernández Mir, and S. Morrison. "Schemes in Lean". In: *Exp. Math*. 31.2 (2022), pages 355–363. ISSN: 1058-6458,1944-950X. DOI: 10.1080/10586458.2021.1983489.

[Car19] M. Carneiro. *The Type Theory of Lean*. Master thesis. 2019. URL: https://github.com/digama0/lean-type-theory/releases.

[CE99] H. Cartan and S. Eilenberg. *Homological algebra*. Princeton Landmarks in Mathematics. With an appendix by David A. Buchsbaum, Reprint of the 1956 original. Princeton University Press, Princeton, NJ, 1999, xvi+390 pages. ISBN: 0-691-04991-2.

[CT22] J. Commelin and A. Topaz. *Completion of the Liquid Tensor Experiment*. 2022. URL: https://leanprover-community.github.io/blog/posts/lte-final/.

[Con00] B. Conrad. *Grothendieck duality and base change*. Volume 1750. Lecture Notes in Mathematics. Springer-Verlag, Berlin, 2000, vi+296 pages. ISBN: 3-540-41134-8. DOI: 10.1007/b75857.

[Del68] P. Deligne. "Théorème de Lefschetz et critères de dégénérescence de suites spectrales". In: *Inst. Hautes Études Sci. Publ. Math*. 35 (1968), pages 259–278. ISSN: 0073-8301,1618-1913. URL: http://www.numdam.org/item/PMIHES_1968_35_107_0.

<figure><img src="image_50.png" /></figure>
[Del74] P. Deligne. "La conjecture de Weil. I". In: *Inst. Hautes Études Sci. Publ. Math.* 43 (1974), pages 273-307. ISSN: 0073-8301, 1618-1913. URL: http://www.numdam.org/item?id=PMIHES_1974_43_273_0.

[DRB17] F. van Doorn, J. von Raumer, and U. Buchholtz. "Homotopy type theory in Lean". In: *Interactive theorem proving*. Volume 10499. Lecture Notes in Comput. Sci. Springer, Cham, 2017, pages 479-495. ISBN: 978-3-319-66107-0; 978-3-319-66106-3. DOI: 10.1007/978-3-319-66107-0.

[DSS] X. Dousson, F. Sergeraert, and Y. Siret. *The Kenzo program*. URL: http://www-fourier.ujf-grenoble.fr/~sergera/Kenzo/.

[GZ67] P. Gabriel and M. Zisman. *Calculus of fractions and homotopy theory*. Volume Band 35. Ergebnisse der Mathematik und ihrer Grenzgebiete [Results in Mathematics and Related Areas]. Springer-Verlag New York, Inc., New York, 1967, x+168 pages.

[Gro57] A. Grothendieck. "Sur quelques points d'algèbre homologique". In: *Tohoku Math. J.* (2) 9 (1957), pages 119-221. ISSN: 0040-8735, 2186-585X. DOI: 10.2748/tmj/1178244839.

[GMP24] B. Guillemet, A. Mahboubi, and M. Piquerez. *Machine-Checked Categorical Diagrammatic Reasoning*. 2024. arXiv: 2402.14485 [cs.LO]. URL: https://arxiv.org/abs/2402.14485.

[Har66] R. Hartshorne. *Residues and duality*. Volume No. 20. Lecture Notes in Mathematics. Lecture notes of a seminar on the work of A. Grothendieck, given at Harvard 1963/64, With an appendix by P. Deligne. Springer-Verlag, Berlin-New York, 1966, vii+423 pages.

[Him20] M. Himmel. "Diagram chasing in interactive theorem proving". Bachelorarbeit. Karlsruher Institut für Technologie, 2020. URL: https://pp.ipd.kit.edu/uploads/publikationen/himmel20bachelorarbeit.pdf.

[HR25] M. Himmel and J. Riou. *Theorems about abelian categories*. 2025. URL: https://leanprover-community.github.io/blog/posts/abelian-categories/.

[Hov01] M. Hovey. "Model category structures on chain complexes of sheaves". In: *Trans. Amer. Math. Soc.* 353.6 (2001), pages 2441-2457. ISSN: 0002-9947, 1088-6850. DOI: 10.1090/S0002-9947-01-02721-0.

[Ill90] L. Illusie. "Catégories dérivées et dualité: travaux de J.-L. Verdier". In: *Enseign. Math.* (2) 36.3-4 (1990), pages 369-391. ISSN: 0013-8584.

<figure><img src="image_51.png" /></figure>
[Jon+] A. J. de Jong et al. *The Stacks project*. URL: https://stacks.math.columbia.edu/.

[KM08] B. Kahn and G. Maltsiniotis. "Structures de dérivabilité". In: *Adv. Math.* 218.4 (2008), pages 1286–1318. ISSN: 0001-8708,1090-2082. DOI: 10.1016/j.aim.2008.03.010.

[LHF23] J. Limperg and A. Halkjær From. "Aesop: White-Box Best-First Proof Search for Lean". In: *CPP 2023: Proceedings of the 12th ACM SIGPLAN Internation Conference on Certified Programs and Proofs*. 2023, pages 253–266. DOI: https://doi.org/10.1145/3573105.3575671.

[Liv23] A. Livingston. "Group Cohomology in the Lean Community Library". In: *14th International Conference on Interactive Theorem Proving (ITP 2023)*. Edited by A. Naumowicz and R. Thiemann. Volume 268. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 22:1–22:17. ISBN: 978-3-95977-284-6. DOI: 10.4230/LIPIcs.ITP.2023.22.

[Mas52] W. S. Massey. "Exact couples in algebraic topology. I, II". In: *Ann. of Math. (2)* 56 (1952), pages 363–396. ISSN: 0003-486X. DOI: 10.2307/1969805.

[Mit64] B. Mitchell. "The full imbedding theorem". In: *Amer. J. Math.* 86.3 (1964), pages 619–637. ISSN: 0002-9327,1080-6377. DOI: 10.2307/2373027.

[Mon22] Y. Monbru. "Towards automatic diagram chasing". M1 report. École Normale Supérieure Paris-Saclay. 2022. URL: https://github.com/ymonbru/Diagram-chasing/blob/main/MONBRU_Yannis_Rapport.pdf.

[MU21] L. de Moura and S. Ullrich. "The Lean 4 Theorem Prover and Programming Language". In: *Automated Deduction – CADE 28*. Edited by A. Platzer and G. Sutcliffe. Cham: Springer International Publishing, 2021, pages 625–635. ISBN: 978-3-030-79876-5. URL: https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37.

[Mur22] B. Murphy. *Formalization of the Brouwer fixed-point theorem in Lean 3*. 2022. URL: https://github.com/Shamrock-Frost/BrouwerFixedPoint.

[Nee01] A. Neeman. *Triangulated categories*. Volume 148. Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2001, pages viii+449. ISBN: 0-691-08685-0; 0-691-08686-9. DOI: 10.1515/9781400837212.

<figure><img src="image_52.png" /></figure>
[Qui67] D. G. Quillen. *Homotopical algebra*. Volume No. 43. Lecture Notes in Mathematics. Springer-Verlag, Berlin-New York, 1967, iv+156 pp. (not consecutively paged).

[RS13] J. Rubio and F. Sergeraert. *Constructive Homological Algebra and Applications*. 2013. arXiv: 1208.3816 [math.KT]. URL: https://arxiv.org/abs/1208.3816.

[Sch21] P. Scholze. *Half a year of the Liquid tensor experiment: Amazing developments*. 2021. URL: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/.

[Ser51] J.-P. Serre. "Homologie singulière des espaces fibrés. Applications". In: *Ann. of Math*. (2) 54 (1951), pages 425-505. ISSN: 0003-486X. DOI: 10.2307/1969485.

[Sim06] C. Simpson. "Explaining Gabriel-Zisman localization to the computer". In: *J. Automat. Reason*. 36.3 (2006), pages 259-285. ISSN: 0168-7433,1573-0670. DOI: 10.1007/s10817-006-9038-x.

[Spa88] N. Spaltenstein. "Resolutions of unbounded complexes". In: *Compositio Math*. 65.2 (1988), pages 121-154. ISSN: 0010-437X,1570-5846. URL: http://www.numdam.org/item?id=CM_1988_65_2_121_0.

[Spa95] E. H. Spanier. *Algebraic topology*. Springer-Verlag, New York, 1995, xvi+528 pages. ISBN: 0-387-94426-5.

[The20] The mathlib community. "The Lean mathematical library". In: *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020*. 2020, pages 367-381. DOI: 10.1145/3372885.3373824.

[Sga] *Théorie des topos et cohomologie étale des schémas. Tome 1: Théorie des topos*. Volume Vol. 269. Lecture Notes in Mathematics. Séminaire de Géométrie Algébrique du Bois-Marie 1963-1964 (SGA 4), Dirigé par M. Artin, A. Grothendieck, et J. L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. Springer-Verlag, Berlin-New York, 1972, xix+525 pages.

[Ver77] J.-L. Verdier. "Catégories dérivées: quelques résultats (état 0)". In: *Cohomologie étale*. Volume 569. Lecture Notes in Math. Springer, Berlin, 1977, pages 262-311. ISBN: 3-540-08066-X; 0-387-08066-X.

[Ver96] J.-L. Verdier. "Des catégories dérivées des catégories abéliennes". In: *Astérisque* 239 (1996). With a preface by Luc Illusie, Edited and with a note by Georges Maltsiniotis, xii+253 pages. ISSN: 0303-1179,2492-5926.

<figure><img src="image_53.png" /></figure>
[WZ22] E. Wieser and J. Zhang. “Graded Rings in Lean’s Dependent Type Theory”. In: *Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings*. Edited by K. Buzzard and T. Kutsia. Volume 13467. Lecture Notes in Computer Science. Springer, 2022, pages 122–137. DOI: 10.1007/978-3-031-16681-5_8.

<figure><img src="image_54.png" /></figure>