The goal of this project is to develop a library for triangulated categories in Lean. It contains definitions and theorems coming from my personal research interest, namely Rouquier dimension, semi-orthogonal decompositions, and support data.
This project constitutes a large part of my PhD thesis.