Commit 2025-12-05 20:27 51a7cdbc
View on Github →feat(Algebra/Homology): extensions of bifunctors to complexes preserve homotopies (#32383)
Given a TotalComplexShape c₁ c₂ c, a functor F : C₁ ⥤ C₂ ⥤ D, we show in this PR that up to homotopy the morphism mapBifunctorMap f₁ f₂ F c only depends on the homotopy classes of the morphism f₁ in HomologicalComplex C c₁ and of the morphism f₂ in HomologicalComplex C c₂.
(The case of f₁ was already done, the case of f₂ is obtained in this PR by symmetry.)