Compact objects form a thick triangulated subcategory #

ObjectProperty.compactObjects.{0} in a pretriangulated category is closed under isomorphisms and shifts (CompactObject.lean, FiniteSupport.lean); this file adds retracts, the zero object, and cones, so that it is a triangulated object property stable under retracts, and every triangulated envelope of compact objects consists of compact objects (ObjectProperty.triangEnvelope_le_compactObjects).

Everything is proved through the direct-sum comparison directSumToHom K X : ⨁ Hom(K, Xᵢ) → Hom(K, ∐ X), whose bijectivity for every Type-indexed coproduct is compactness (isCompactObject_iff_bijective_directSumToHom). Retracts are a two-out-of-three argument on that map; cones are the five lemma applied to the rows ⨁ Hom(-, Xᵢ) and Hom(-, ∐ X) along a distinguished triangle, both exact by Triangle.yoneda_exact₂ and Triangle.yoneda_exact₃, the first summandwise.

The geometric consumer is the compact/perfect comparison on Dqc(X) (#723): the perfect locus is the essential image of the thick envelope of finite locally free sheaves, so it consists of compact objects as soon as those sheaves are compact.

Main results #

IsCompactObject.of_retract, IsCompactObject.of_isZero, IsCompactObject.of_distTriang₃.
directSumPrecomp_exact — exactness of ⨁ Hom(-, Xᵢ) from exactness of each Hom(-, Xᵢ).
the instances IsStableUnderRetracts, ContainsZero, IsStableUnderShift ℤ, IsTriangulatedClosed₂, IsTriangulatedClosed₃, IsTriangulated on compactObjects.{0}.
ObjectProperty.triangEnvelope_le_compactObjects.

source

theorem CategoryTheory.IsCompactObject.of_retract {C : Type u} [Category.{v, u} C] [Preadditive C] {K L : C} (h : Retract K L) (hL : IsCompactObject L) :

IsCompactObject K

A retract of a compact object is compact.

source

theorem CategoryTheory.IsCompactObject.of_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : Limits.IsZero K) :

IsCompactObject K

A zero object is compact.

source

instance CategoryTheory.ObjectProperty.compactObjects.isStableUnderRetracts {C : Type u} [Category.{v, u} C] [Preadditive C] :

compactObjects.IsStableUnderRetracts

source

theorem CategoryTheory.directSumPrecomp_exact {C : Type u} [Category.{v, u} C] [Preadditive C] {ι : Type} [DecidableEq ι] (X : ι → C) {A B Y : C} (f : A ⟶ B) (g : B ⟶ Y) (hzero : CategoryStruct.comp f g = 0) (hex : ∀ (i : ι) (b : B ⟶ X i), CategoryStruct.comp f b = 0 → ∃ (a : Y ⟶ X i), b = CategoryStruct.comp g a) (x : DirectSum ι fun (i : ι) => B ⟶ X i) :

(directSumPrecomp X f) x = 0 ↔ ∃ (y : DirectSum ι fun (i : ι) => Y ⟶ X i), (directSumPrecomp X g) y = x

Exactness of ⨁ Hom(-, Xᵢ) at B along A ⟶ B ⟶ Y follows from exactness of each Hom(-, Xᵢ): a summandwise lift assembled on the finite support.

source

theorem CategoryTheory.IsCompactObject.of_distTriang₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : IsCompactObject T.obj₁) (h₂ : IsCompactObject T.obj₂) :

IsCompactObject T.obj₃

Cone closure. The third object of a distinguished triangle whose first two objects are compact is compact: the five lemma for the rows ⨁ Hom(-, Xᵢ) and Hom(-, ∐ X) along the triangle and its rotation.

source