Commit 2026-10-20 23:05 e1b2403b

feat(CategoryTheory/Abelian/TorsionTheory): Introduce torsion theory for abelian categories (#36744) Introduces torsion theories on an abelian category: a pair of object properties T and F that are each other's left and right orthogonals. Adds Abelian.TorsionTheory, the typeclasses IsTorsionClass / IsTorsionFreeClass (on the model of Functor.IsLeftAdjoint, so closure properties come by instance search), the torsion theories generated and cogenerated by a property, transport along op/unop, and Dickson's theorem isTorsionClass_iff: in a well-powered abelian category with coproducts, a class is a torsion class iff it is closed under quotients, extensions and coproducts. The torsion-free version follows by passing to Cᵒᵖ.