The triangulated subcategory of acyclic complex in the homotopy category

In this file, we define the triangulated subcategory HomotopyCategory.subcategoryAcyclic C of the homotopy category of cochain complexes in an abelian category C. In the lemma HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W we obtain that the class of quasiisomorphisms HomotopyCategory.quasiIso C (ComplexShape.up ℤ) consists of morphisms whose cone belongs to the triangulated subcategory HomotopyCategory.subcategoryAcyclic C of acyclic complexes.

def HomotopyCategory.subcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

The triangulated subcategory of HomotopyCategory C (ComplexShape.up ℤ) consisting of acyclic complexes.

Equations

• HomotopyCategory.subcategoryAcyclic C = (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologicalKernel

instance HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : (subcategoryAcyclic C).IsTriangulated

instance HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : (subcategoryAcyclic C).IsClosedUnderIsomorphisms

theorem HomotopyCategory.mem_subcategoryAcyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : HomotopyCategory C (ComplexShape.up ℤ)) : subcategoryAcyclic C X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj X)

theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) : subcategoryAcyclic C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) : subcategoryAcyclic C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ HomologicalComplex.Acyclic K

theorem HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : quasiIso C (ComplexShape.up ℤ) = (subcategoryAcyclic C).trW