← All papers
Formalization of derived categories in Lean/mathlib
cs.LO
Jan 1, 2025 · v1
TL;DR
Formalizes derived categories, triangulated categories, and localization in Lean 4 mathlib.
Abstract
This paper presents the formalization of derived categories and their basic properties in the Lean 4 proof assistant as part of the mathlib library. The construction covers the localization of categories at a class of morphisms, triangulated categories, and the derived category of an abelian category via its homotopy category and quasi-isomorphisms.
Problem
Derived categories are fundamental objects in homological algebra and algebraic geometry, but their construction and basic properties had not been formalized in a proof assistant as part of a general-purpose mathematical library.
Approach
The authors formalize derived categories and their basic properties in Lean 4 as part of the mathlib library. The construction covers localization of categories at a class of morphisms, triangulated categories, and the derived category of an abelian category via its homotopy category and quasi-isomorphisms.
Results
The formalization is integrated into mathlib, providing a reusable foundation for further work in homological algebra within Lean 4.