HomotopyCategory.eq_of_homotopy

theorem HomotopyCategory.eq_of_homotopy : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D), Homotopy f g → (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g

The theorem `HomotopyCategory.eq_of_homotopy` states that for any types `ι` and `V`, with `V` a category that is preadditive, for any complex shape `c`, and for any homological complexes `C` and `D` in this category, if there exist morphisms `f` and `g` from `C` to `D` that are homotopic, then the images of `f` and `g` under the quotient functor from complexes to the homotopy category are equal. In other words, homotopic morphisms in the category of complexes get mapped to the same morphism in the homotopy category.

More concisely: Given a preadditive category `V`, any complex shape `c`, and homological complexes `C` and `D` in `V`, if there exist homotopic morphisms `f` and `g` from `C` to `D`, then their images under the quotient functor to the homotopy category are equal.