Commit 2024-06-08 04:33 cce8437a

View on Github →

feat: the derived category of an abelian category (#11806) The derived category of an abelian category is defined and it is shown that it is a triangulated category.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

added def DerivedCategory.Q

added def DerivedCategory.Qh

added def DerivedCategory.quotientCompQhIso

added def DerivedCategory

added def HasDerivedCategory.standard

added theorem HomotopyCategory.mem_subcategoryAcyclic_iff

added theorem HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W

added theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt

added def HomotopyCategory.subcategoryAcyclic

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/CategoryTheory/Triangulated/Subcategory.lean

Modified docs/references.bib