Acyclic objects and quasi-isomorphisms in the bounded homotopy category

Let C be an abelian category. This file defines the acyclic objects TauCeti.HomotopyCategory.Bounded.subcategoryAcyclic and the quasi-isomorphisms TauCeti.HomotopyCategory.Bounded.quasiIso of the homotopy category of bounded cochain complexes, by restriction along the inclusion into the homotopy category. A morphism is a quasi-isomorphism exactly when its cone is acyclic (TauCeti.HomotopyCategory.Bounded.quasiIso_eq_subcategoryAcyclic_trW), so the quasi-isomorphisms are compatible with the shift.

References

• Mathlib's Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean, which defines the corresponding notions for bounded below complexes.

@[reducible, inline]

abbrev TauCeti.HomotopyCategory.Bounded.subcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.ObjectProperty (Bounded C)

The property of objects of TauCeti.HomotopyCategory.Bounded C which are acyclic.

theorem TauCeti.HomotopyCategory.Bounded.mem_subcategoryAcyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : Bounded C) : subcategoryAcyclic C K ↔ HomotopyCategory.subcategoryAcyclic C K.obj

An object of the bounded homotopy category is acyclic exactly when it is acyclic in the homotopy category.

def TauCeti.HomotopyCategory.Bounded.quasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.MorphismProperty (Bounded C)

The quasi-isomorphisms in the homotopy category of bounded cochain complexes.

theorem TauCeti.HomotopyCategory.Bounded.quasiIso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : Bounded C} (f : K ⟶ L) : quasiIso C f ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f.hom

A morphism of bounded complexes is a quasi-isomorphism when it is one in the homotopy category.

theorem TauCeti.HomotopyCategory.Bounded.quasiIso_eq_subcategoryAcyclic_trW (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : quasiIso C = (subcategoryAcyclic C).trW

A morphism of bounded complexes is a quasi-isomorphism exactly when its cone is acyclic.

instance TauCeti.HomotopyCategory.Bounded.instIsCompatibleWithShiftQuasiIsoInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : (quasiIso C).IsCompatibleWithShift ℤ