Theorems · Theorem · category theory

HomotopyCategory.inverseImage_quotient_isomorphisms

∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι),
  (CategoryTheory.MorphismProperty.isomorphisms (HomotopyCategory V c)).inverseImage (HomotopyCategory.quotient V c) =
    HomologicalComplex.homotopyEquivalences V c

Defined in

Mathlib.Algebra.Homology.HomotopyCategory

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive