Commit 2026-03-02 23:05 98be3dce

View on Github →

feat(Algebra/Homology): compatibilities for homology functors (#35938) We add compatibility lemmas for the comparison of the homology functors on the categories of cochain complexes, the homotopy category or the derived category.

Estimated changes

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

added theorem DerivedCategory.homologyFunctorFactors_hom_naturality

added theorem DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj

added theorem DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj

added theorem DerivedCategory.shiftMap_homologyFunctor_map_Q

added theorem DerivedCategory.shiftMap_homologyFunctor_map_Qh

added theorem DerivedCategory.shift_homologyFunctor

Modified Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

Modified Mathlib/Algebra/Homology/Localization.lean

added theorem HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj

added theorem HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj