Commit 2025-09-01 08:25 d230a16f

View on Github →

feat(Algebra/Homology): the canonical t-structure on the derived category (#27395)

Estimated changes

Modified Mathlib.lean

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

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

added def DerivedCategory.TStructure.t

added theorem DerivedCategory.exists_iso_Q_obj_of_isGE

added theorem DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE

added theorem DerivedCategory.exists_iso_Q_obj_of_isLE

added theorem DerivedCategory.isGE_Q_obj_iff

added theorem DerivedCategory.isGE_iff

added theorem DerivedCategory.isLE_Q_obj_iff

added theorem DerivedCategory.isLE_iff

added theorem DerivedCategory.isZero_of_isGE

added theorem DerivedCategory.isZero_of_isLE

Modified Mathlib/Algebra/Homology/Embedding/CochainComplex.lean

added theorem CochainComplex.g_shortComplexTruncLEX₃ToTruncGE

added theorem CochainComplex.shortComplexTruncLE_shortExact

Modified Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean

added theorem CategoryTheory.Triangulated.TStructure.isGE_of_iso

added theorem CategoryTheory.Triangulated.TStructure.isLE_of_iso