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]
:
The triangulated subcategory of HomotopyCategory C (ComplexShape.up ℤ) consisting
of acyclic complexes.
Equations
Instances For
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 ℤ)
:
theorem
HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
: