Theorems · Theorem · category theory

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) (h : Homotopy f g),
  (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g

Defined in

Mathlib.Algebra.Homology.HomotopyCategory

Cited by

7 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive