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 1

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: Derived category,Homological algebra,Spectral sequence,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]
Licence: Attribution 4.0 International (CC BY 4.0)

Share and export