Commit 2026-06-23 08:28 a83a1c30

View on Github →

feat(Algebra/Homology): more on the functoriality of categories of homological complexes (#40895)

Estimated changes

Modified Mathlib/Algebra/Homology/Additive.lean

added def CategoryTheory.Functor.mapHomologicalComplexCompIso

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

added def CategoryTheory.Functor.mapHomotopyCategoryCompIso

added def CategoryTheory.Functor.preimageHomotopy

added theorem HomologicalComplex.isIso_quotient_map_iff_homotopyEquivalences