Documentation

TauCeti.Algebra.Homology.DerivedCategory.Perfect

Perfect objects are bounded complexes of projectives #

Let C be an abelian category with enough projectives. An object of the bounded derived category is perfect, that is, lies in the thick subcategory generated by the projective objects in degree zero, if and only if it is represented by a bounded complex of projective objects.

One direction is TauCeti.DerivedCategory.Bounded.perfect_Qh_obj_quotient_obj. For the other, a perfect object X has no morphisms to W[-n] for W in C and n small enough, since the projective objects in degree zero have this property and it is inherited by the thick subcategory they generate. Represent X by a bounded above complex K of projectives, and let m be so small that K is exact below m and X has no morphisms to objects of C placed in degree m - 1. The canonical truncation K.truncGE m is quasi-isomorphic to K, its terms are those of K above m, and its term in degree m is K.opcycles m, the cokernel of d : K^{m-1} ⟶ K^m. The chain map K ⟶ (K.opcycles (m - 1))[1 - m] given by the projection is zero in the derived category, hence null-homotopic since K is K-projective, and the null-homotopy splits off K.opcycles m as a retract of K^m (CochainComplex.retractOpcyclesOfHomotopy). So K.truncGE m is a bounded complex of projective objects.

The same truncation shows that in finite global dimension every object of the bounded derived category is represented by a bounded complex of projectives. If every object of C has projective dimension < d and K is exact below a, then along the short exact sequences 0 ⟶ Zʲ ⟶ Kʲ ⟶ Zʲ⁺¹ ⟶ 0 the cycles Zᵐ⁺¹ are a d-th syzygy of Zᵐ⁺¹⁺ᵈ for m far below a, hence projective, and K.opcycles m ≅ Zᵐ⁺¹.

Main results #

source
theorem DerivedCategory.singleFunctor_hom_eq_zero_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {Q : C} [CategoryTheory.Projective Q] {m n : ℤ} (hmn : m < n) {Y : C} (f : (singleFunctor C n).obj Q ⟶ (singleFunctor C m).obj Y) :
f = 0

A projective object placed in degree n has no nonzero morphisms to an object placed in a lower degree m < n: Mathlib's from_singleFunctor_obj_eq_zero_of_projective, transported along singleFunctorIsoCompQ.

source
theorem DerivedCategory.exists_homSingle_eq_zero_of_perfect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X : Bounded C} (hX : TauCeti.DerivedCategory.Bounded.perfect C X) :
∃ (n₀ : ℤ), ∀ n ≤ n₀, ∀ (W : C) (f : Bounded.ι.obj X ⟶ (singleFunctor C n).obj W), f = 0

Perfect objects have bounded morphisms to objects of C: a perfect object of the bounded derived category has no nonzero morphisms to W[-n] for W in C and n small enough.

source
theorem DerivedCategory.exists_singleHom_eq_zero_of_perfect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.HasExt C] {K : Bounded C} (hK : TauCeti.DerivedCategory.Bounded.perfect C K) :
∃ (n₀ : ℤ), ∀ n ≥ n₀, ∀ (X : C), (∀ (i : ℕ), (CategoryTheory.isProjective C).extLeftOrthogonal (i + 1) X) → ∀ (f : (singleFunctor C n).obj X ⟶ Bounded.ι.obj K), f = 0

Perfect objects receive no morphisms from Ext-orthogonal objects in high degrees: for a perfect object K of the bounded derived category there is n₀ such that every morphism to K from an object of C without higher extensions by projectives, placed in a degree n ≥ n₀, vanishes.

source
theorem DerivedCategory.exists_bounded_projective_of_projective_opcycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K : CochainComplex C ℤ} {m b : ℤ} (hmb : m ≤ b) [K.IsStrictlyLE b] [K.IsGE m] (hK : ∀ (n : ℤ), CategoryTheory.Projective (K.X n)) [CategoryTheory.Projective (HomologicalComplex.opcycles K m)] :
∃ (L : CochainComplex C ℤ) (a : ℤ) (b : ℤ), L.IsStrictlyGE a ∧ L.IsStrictlyLE b ∧ (∀ (n : ℤ), CategoryTheory.Projective (L.X n)) ∧ Nonempty (Q.obj L ≅ Q.obj K)

Let K be a complex of projective objects which is strictly ≤ b and has no cohomology in degrees < m, for some m ≤ b. If the cokernel K.opcycles m of the differential into degree m is projective, then K is isomorphic in the derived category to a bounded complex of projective objects (namely its canonical truncation K.truncGE m).

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

Perfect objects are bounded complexes of projectives: in an abelian category with enough projectives, a perfect object of the bounded derived category is represented by a bounded complex of projective objects.

source
theorem DerivedCategory.exists_bounded_projective_of_hasProjectiveDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (d : ℕ) (hd : ∀ (Y : C), CategoryTheory.HasProjectiveDimensionLT Y d) (X : Bounded C) :
∃ (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ), K.IsStrictlyGE a ∧ K.IsStrictlyLE b ∧ (∀ (n : ℤ), CategoryTheory.Projective (K.X n)) ∧ Nonempty (Q.obj K ≅ Bounded.ι.obj X)

Bounded complexes of projectives in finite global dimension: in an abelian category with enough projectives in which every object has projective dimension < d, every object of the bounded derived category is represented by a bounded complex of projective objects.

source
theorem DerivedCategory.Bounded.perfect_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (X : Bounded C) :
TauCeti.DerivedCategory.Bounded.perfect C 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)

Perfect objects are the bounded complexes of projectives: in an abelian category with enough projectives, an object of the bounded derived category is perfect if and only if it is the image of a bounded complex of projective objects.

source
theorem DerivedCategory.Bounded.exists_projective_Qh_obj_iso_of_hasProjectiveDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughProjectives C] (d : ℕ) (hd : ∀ (Y : C), CategoryTheory.HasProjectiveDimensionLT Y d) (X : Bounded C) :
∃ (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)

Bounded complexes of projectives in finite global dimension: in an abelian category with enough projectives in which every object has projective dimension < d, every object of the bounded derived category is the image of a bounded complex of projective objects.