Joël Riou - Formalization of derived categories in Lean/mathlib

afm:13609 - Annals of Formalized Mathematics, July 15, 2025, Volume 1 - https://doi.org/10.46298/afm.13609
Formalization of derived categories in Lean/mathlibArticle

Authors: Joël Riou ORCID1


This paper outlines the formalization of derived categories in the mathematical library of the proof assistant Lean 4. The derived category D(C) of any abelian category C is formalized as the localization of the category of unbounded cochain complexes with respect to the class of quasi-isomorphisms, and it is endowed with a triangulated structure.

https://doi.org/10.46298/afm.13609
Source: HAL:hal-04546712v5
Volume: Volume 1
Published on: July 15, 2025
Accepted on: February 11, 2025
Submitted on: May 17, 2024
Keywords: MSC 2020: 18G80, 18G15, 18G40, 18E35, 68V20, [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [en] Derived category, Homological algebra, Spectral sequence
Licence: Attribution 4.0 International (CC BY 4.0)

Share and export

Consultation statistics

This page has been seen 612 times.
This article's PDF has been downloaded 812 times.