Projective resolutions of bounded complexes

In an abelian category with enough projectives, every object of the bounded derived category is represented by a bounded above complex of projective objects.

The objects of the derived category represented by bounded above complexes of projectives form a triangulated subcategory (DerivedCategory.boundedAboveProjective): a morphism between two of them lifts to a chain map, since bounded above complexes of projectives are K-projective, and its mapping cone is again a bounded above complex of projectives. It contains every object placed in degree zero, through a projective resolution of that object. The bounded homotopy category is generated by such objects (TauCeti.HomotopyCategory.Bounded.prop_quotient_obj), so it contains the bounded derived category.

A bounded complex of projectives is K-projective, so in the bounded homotopy category it has no nonzero morphisms to acyclic complexes, and the localization K^b(C) ⥤ D^b(C) is bijective on morphisms out of it.

Main definitions

• DerivedCategory.boundedAboveProjective: the objects of the derived category isomorphic to a bounded above complex of projective objects.

Main results

• DerivedCategory.boundedAboveProjective_of_bounded: in an abelian category with enough projectives, every object of the bounded derived category is represented by a bounded above complex of projective objects.
• DerivedCategory.exists_projective_isGE_isStrictlyLE_of_bounded: such a complex can moreover be chosen with cohomology bounded below.
• DerivedCategory.Bounded.exists_bounded_projective_iff_exists_projective_Qh_obj_iso: an object of the bounded derived category is represented by a bounded complex of projectives if and only if it is the image of one from the bounded homotopy category.
• TauCeti.DerivedCategory.Bounded.leftOrthogonal_quotient_obj_of_projective: a bounded complex of projectives is left orthogonal to the acyclic objects of the bounded homotopy category.
• TauCeti.DerivedCategory.Bounded.Qh_map_bijective_of_projective: the localization K^b(C) ⥤ D^b(C) is bijective on morphisms out of a bounded complex of projectives.

def DerivedCategory.boundedAboveProjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.ObjectProperty (DerivedCategory C)

The objects of the derived category isomorphic to a bounded above complex of projective objects.

theorem DerivedCategory.boundedAboveProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) : boundedAboveProjective C X ↔ ∃ (K : CochainComplex C ℤ) (d : ℤ), K.IsStrictlyLE d ∧ (∀ (n : ℤ), CategoryTheory.Projective (K.X n)) ∧ Nonempty (Q.obj K ≅ X)

instance DerivedCategory.instIsClosedUnderIsomorphismsBoundedAboveProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).IsClosedUnderIsomorphisms

instance DerivedCategory.instContainsZeroBoundedAboveProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).ContainsZero

instance DerivedCategory.instIsStableUnderShiftBoundedAboveProjectiveInt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).IsStableUnderShift ℤ

instance DerivedCategory.instIsTriangulatedClosed₃BoundedAboveProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).IsTriangulatedClosed₃

instance DerivedCategory.instIsTriangulatedClosed₂BoundedAboveProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).IsTriangulatedClosed₂

instance DerivedCategory.instIsTriangulatedBoundedAboveProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedAboveProjective C).IsTriangulated

theorem DerivedCategory.boundedAboveProjective_singleFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (X : C) : boundedAboveProjective C ((singleFunctor C 0).obj X)

An object placed in degree zero is represented by its projective resolution.

theorem DerivedCategory.boundedAboveProjective_of_bounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (X : Bounded C) : boundedAboveProjective C (Bounded.ι.obj X)

Every object of the bounded derived category is represented by a bounded above complex of projective objects, in an abelian category with enough projectives.

theorem DerivedCategory.exists_projective_isGE_isStrictlyLE_of_bounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (X : Bounded C) : ∃ (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ), K.IsGE a ∧ K.IsStrictlyLE b ∧ (∀ (n : ℤ), CategoryTheory.Projective (K.X n)) ∧ Nonempty (Q.obj K ≅ Bounded.ι.obj X)

In an abelian category with enough projectives, every object X of the bounded derived category is represented by a complex K of projective objects which is strictly ≤ b and has no cohomology in degrees < a, for some a and b.

theorem DerivedCategory.Bounded.exists_bounded_projective_iff_exists_projective_Qh_obj_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Bounded C) : (∃ (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ), K.IsStrictlyGE a ∧ K.IsStrictlyLE b ∧ (∀ (n : ℤ), CategoryTheory.Projective (K.X n)) ∧ Nonempty (Q.obj K ≅ ι.obj X)) ↔ ∃ (K : CochainComplex.Bounded C), (∀ (n : ℤ), CategoryTheory.Projective (K.obj.X n)) ∧ Nonempty ((TauCeti.DerivedCategory.Bounded.Qh C).obj ((TauCeti.HomotopyCategory.Bounded.quotient C).obj K) ≅ X)

An object of the bounded derived category is represented by a bounded complex K of projective objects if and only if it is the image of such a complex, as an object of the bounded homotopy category.

theorem TauCeti.DerivedCategory.Bounded.leftOrthogonal_quotient_obj_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : CochainComplex.Bounded C) (hK : ∀ (n : ℤ), CategoryTheory.Projective (K.obj.X n)) : (HomotopyCategory.Bounded.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.Bounded.quotient C).obj K)

A bounded complex of projective objects is left orthogonal, in the bounded homotopy category, to the acyclic complexes: it is K-projective.

theorem TauCeti.DerivedCategory.Bounded.Qh_map_bijective_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex.Bounded C) (hK : ∀ (n : ℤ), CategoryTheory.Projective (K.obj.X n)) (L : HomotopyCategory.Bounded C) : Function.Bijective (Qh C).map

The localization K^b(C) ⥤ D^b(C) is bijective on morphisms out of a bounded complex of projective objects.