Theorems · Theorem · category theory

HomologicalComplex.isIso_quotient_map_iff_homotopyEquivalences

∀ {ι : Type u_3} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {K L : HomologicalComplex V c} (f : K ⟶ L),
  CategoryTheory.IsIso ((HomotopyCategory.quotient V c).map f) ↔ HomologicalComplex.homotopyEquivalences V c f

Defined in

Mathlib.Algebra.Homology.HomotopyCategory

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive