Formalization of derived categories in Lean/mathlib

DOI10.46298/AFM.13609MaRDI QIDQ6867741zbMATH OpenFDO

Authors Joël Riou

Publication date 28 January 2026

Published in Annals of Formalized Mathematics. AFM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/AFM.13609

zbMATH Keywords

derived categoryhomological algebraspectral sequence

Mathematics Subject Classification ID

Localization of categories, calculus of fractions (18E35) Ext and Tor, generalizations, Künneth formula (category-theoretic aspects) (18G15) Spectral sequences, hypercohomology (18G40) Derived categories, triangulated categories (18G80) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A mechanized proof of the basic perturbation lemma
• Catégories dérivées et dualité, travaux de J.-L. Verdier. (Derived categories and duality, papers of J.-L. Verdier)
• Derivability structures
• Exact couples in algebraic topology. I.-V
• Explaining Gabriel-Zisman localization to the computer
• Graded rings in Lean's dependent type theory
• Grothendieck duality and base change
• Group cohomology in the Lean community library
• Homologie singulière des espaces fibrés. Applications
• Homotopical algebra
• scientific article; zbMATH DE number 4036043 (Why is no real title available?)
• scientific article; zbMATH DE number 3632726 (Why is no real title available?)
• scientific article; zbMATH DE number 692330 (Why is no real title available?)
• scientific article; zbMATH DE number 715014 (Why is no real title available?)
• scientific article; zbMATH DE number 1024391 (Why is no real title available?)
• scientific article; zbMATH DE number 1390914 (Why is no real title available?)
• scientific article; zbMATH DE number 3297895 (Why is no real title available?)
• scientific article; zbMATH DE number 3385032 (Why is no real title available?)
• Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings
• Machine-checked categorical diagrammatic reasoning
• Model category structures on chain complexes of sheaves
• Perverse sheaves. Proceedings of the colloquium ``Analysis and topology on singular spaces, Luminy, France, July 6--10, 1981. Part I
• Residues and duality. Lecture notes of a seminar on the work of A. Grothendieck, given at Havard 1963/64. Appendix: Cohomology with supports and the construction of the \(f^!\) functor by P. Deligne
• Schemes in Lean
• The Full Imbedding Theorem
• The Lean 4 theorem prover and programming language
• Théoreme de Lefschetz et critères de dégénérescence de suites spectrales
• Triangulated categories

Cited in

(1)

• Generalised class groups in dihedral and fake \(\mathbb{Z}_p\)-extensions

Describes a project that uses

Uses Software

• Formalization of derived categories in Lean/mathlib

This page was built for publication: Formalization of derived categories in Lean/mathlib

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6867741)