Compact objects in a triangulated category

Compact objects form a thick triangulated subcategory. The extension step is the five lemma applied to the compactness comparison maps and the long exact Hom sequence of a distinguished triangle. Closure under retracts is proved by observing that the comparison map for a retract is itself a retract in the arrow category.

instance CategoryTheory.AddCommGrpCat.hasCoproductsSucc : Limits.HasCoproducts AddCommGrpCat

Exact coproducts in additive commutative groups may be indexed in the universe immediately below the carrier universe.

instance CategoryTheory.AddCommGrpCat.ab4OfSizeSucc : AB4OfSize.{u, u + 1, u + 2} AddCommGrpCat

theorem CategoryTheory.IsCompactObject.shift {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (n : ℤ) : IsCompactObject ((shiftFunctor C n).obj K)

A shift of a compact object is compact in the same indexing universe.

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

In a distinguished triangle, the middle object is compact when the two outer objects are compact.

theorem CategoryTheory.IsCompactObject.zero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [Limits.HasCoproducts AddCommGrpCat] : IsCompactObject 0

A zero object is compact.

theorem CategoryTheory.IsCompactObject.of_retract_of_size {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasCoproducts AddCommGrpCat] {X Y : C} (r : Retract X Y) (hY : IsCompactObject Y) : IsCompactObject X

A retract of a compact object is compact.

instance CategoryTheory.ObjectProperty.compactObjects_isStableUnderRetracts {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasCoproducts AddCommGrpCat] : compactObjects.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.compactObjects_containsZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [Limits.HasCoproducts AddCommGrpCat] : compactObjects.ContainsZero

instance CategoryTheory.ObjectProperty.compactObjects_isStableUnderShift {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] : compactObjects.IsStableUnderShift ℤ

instance CategoryTheory.ObjectProperty.compactObjects_isTriangulatedClosed₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasCoproducts AddCommGrpCat] [AB4OfSize.{w, v, v + 1} AddCommGrpCat] : compactObjects.IsTriangulatedClosed₂

instance CategoryTheory.ObjectProperty.compactObjects_isTriangulated {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasCoproducts AddCommGrpCat] [AB4OfSize.{w, v, v + 1} AddCommGrpCat] : compactObjects.IsTriangulated