Theorems · Theorem · category theory

HomotopyCategory.isoOfHomotopyEquiv_hom

∀ {ι : 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 : HomotopyEquiv C D),
  (HomotopyCategory.isoOfHomotopyEquiv f).hom = (HomotopyCategory.quotient V c).map f.hom

Defined in

Mathlib.Algebra.Homology.HomotopyCategory

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive