Torsion Theories for Abelian Categories

Stream: Is there code for X?

[Blake Farman]

I'm looking for categorical torsion theories (à la nLab : torsion theory). I've searched for the usual terms, but haven't turned up anything aside from Mathlib.CategoryTheory.Abelian.SerreClass. I wanted to check in here to see if I'm just not guessing the right names, or if there's known work in progress before attempting to build out new infrastructure.

[Joël Riou]

We do not have anything apart from SerreClass (and the various related typeclasses and definitions in the folder CategoryTheory/ObjectProperty/).

[Blake Farman]

Thanks for the confirmation