Homotopy.map_eq_of_inverts_homotopyEquivalences

theorem Homotopy.map_eq_of_inverts_homotopyEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F G : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel] {φ₀ φ₁ : F ⟶ G}, Homotopy φ₀ φ₁ → (∀ (j : ι), ∃ i, c.Rel i j) → ∀ [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)] [inst_4 : HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))] {D : Type u_3} [inst_5 : CategoryTheory.Category.{u_5, u_3} D] (H : CategoryTheory.Functor (HomologicalComplex C c) D), (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H → H.map φ₀ = H.map φ₁

This theorem states that given two homological complexes `F` and `G` in a category `C` with a complex shape `c`, if there exists a homotopy between two morphisms `φ₀` and `φ₁` from `F` to `G`, and for every index `j` in the complex shape, there exists some index `i` such that `i` is related to `j` by the relation `c.Rel`, then for any category `D` and any functor `H` from the category of homological complexes on `C` and `c` to `D`, if `H` inverts homotopy equivalences, then the map of `φ₀` through `H` is equal to the map of `φ₁` through `H`. In simpler terms, if a functor inverts homotopy equivalences, it preserves the property of homotopy, i.e., it maps homotopic maps to the same map. This is a property of functors that preserve homotopy equivalences.

More concisely: If `F` and `G` are homological complexes in category `C` with complex shape `c`, `φ₀` and `φ₁` are homotopic morphisms from `F` to `G`, and `H` is a functor from the category of homological complexes on `C` and `c` to `D` that inverts homotopy equivalences, then `H(φ₀) = H(φ₁)`.