Commit 2024-03-24 11:48 ac118283
View on Github →feat(Algebra/Homology): the action of a bifunctor on homological complexes factors through homotopies (#10800)
Given a TotalComplexShape c₁ c₂ c, a functor F : C₁ ⥤ C₂ ⥤ D, we study the behavior with respect to homotopies or the functoriality of the action of F on homological complexes: if f₁ and f₁' are homotopic maps, then the maps mapBifunctorMap f₁ f₂ F c and mapBifunctorMap f₁' f₂ F c are also homotopic.