Commit 2024-06-09 22:38 d4e36bbf

View on Github →

feat: the homology sequence of a distinguished triangle in the derived category (#13664) In this PR, we define homologyFunctor C n : DerivedCategory C ⥤ C, show they are homological functors and construct the long exact sequences associated to distinguished triangles in the derived category.

Estimated changes

Modified Mathlib.lean

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

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

added theorem DerivedCategory.HomologySequence.comp_δ

added theorem DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff

added theorem DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff

added theorem DerivedCategory.HomologySequence.exact₁

added theorem DerivedCategory.HomologySequence.exact₂

added theorem DerivedCategory.HomologySequence.exact₃

added theorem DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff

added theorem DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff

added theorem DerivedCategory.HomologySequence.δ_comp

Modified Mathlib/CategoryTheory/Localization/Triangulated.lean

added theorem CategoryTheory.Functor.distTriang_iff

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

added theorem CategoryTheory.Functor.isHomological_of_localization