Localizing and colocalizing closures in a pretriangulated category

Let P be a class of objects of a pretriangulated category C. Its localizing closure is the smallest isomorphism-closed triangulated subcategory of C containing P and closed under coproducts indexed by types in the hom universe of C; it is the infimum of all such subcategories. Dually, the colocalizing closure is the smallest isomorphism-closed triangulated subcategory containing P and closed under such products.

A triangulated subcategory closed under countable coproducts is closed under direct summands, by the Eilenberg swindle CategoryTheory.Retract.biprodSigmaIso: if X is a retract of Y, then X ⊞ Y^(ℕ) ≅ Y^(ℕ), and the split triangle X ⟶ X ⊞ Y^(ℕ) ⟶ Y^(ℕ) ⟶ X⟦1⟧ puts X in the subcategory. The dual statement for products follows by passing to the opposite category. Consequently, when C has countable coproducts (respectively products), the thick closure P.triangEnvelope is contained in the localizing (respectively colocalizing) closure.

For curved DG modules, with P the class of totalizations of short exact sequences, these are Positselski's absolutely acyclic (P.triangEnvelope), coacyclic (P.localizingClosure) and contraacyclic (P.colocalizingClosure) objects, and the two inclusions are those inducing the comparison functors from the absolute derived category to the coderived and contraderived categories.

Main definitions

• CategoryTheory.ObjectProperty.localizingClosure: the localizing closure of P.
• CategoryTheory.ObjectProperty.colocalizingClosure: the colocalizing closure of P.

Main results

• CategoryTheory.ObjectProperty.isStableUnderRetracts_of_isClosedUnderCoproducts_nat: an isomorphism-closed property closed under countable coproducts and satisfying IsTriangulatedClosed₁ (for instance a triangulated subcategory) is closed under retracts.
• CategoryTheory.ObjectProperty.isStableUnderRetracts_of_isClosedUnderProducts_nat: the dual statement for countable products, assuming IsTriangulatedClosed₃.
• CategoryTheory.ObjectProperty.localizingClosure_le_iff, CategoryTheory.ObjectProperty.colocalizingClosure_le_iff: the universal properties.
• CategoryTheory.ObjectProperty.triangEnvelope_le_localizingClosure, CategoryTheory.ObjectProperty.triangEnvelope_le_colocalizingClosure: the thick closure is contained in the localizing and in the colocalizing closure.

References

• A. Neeman, Triangulated categories, Annals of Mathematics Studies 148, Princeton University Press (2001), Proposition 1.6.8 and Definition 3.2.6.
• L. Positselski, Differential graded Koszul duality: an introductory survey, Bull. Lond. Math. Soc. 55 (2023), 1553–1640, Section 7.6.

theorem CategoryTheory.ObjectProperty.isStableUnderRetracts_of_isClosedUnderCoproducts_nat {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [P.IsTriangulatedClosed₁] [Limits.HasCoproductsOfShape ℕ C] [P.IsClosedUnderColimitsOfShape (Discrete ℕ)] : P.IsStableUnderRetracts

An isomorphism-closed property closed under countable coproducts, and such that the first object of a distinguished triangle satisfies it whenever the other two do, is closed under retracts (Eilenberg swindle). This applies in particular to triangulated subcategories.

theorem CategoryTheory.ObjectProperty.isStableUnderRetracts_of_isClosedUnderProducts_nat {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [P.IsTriangulatedClosed₃] [Limits.HasProductsOfShape ℕ C] [P.IsClosedUnderLimitsOfShape (Discrete ℕ)] : P.IsStableUnderRetracts

An isomorphism-closed property closed under countable products, and such that the third object of a distinguished triangle satisfies it whenever the other two do, is closed under retracts. This applies in particular to triangulated subcategories.

def CategoryTheory.ObjectProperty.localizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : ObjectProperty C

The localizing closure of P: the smallest isomorphism-closed triangulated subcategory containing P and closed under coproducts indexed by types in Type v, defined as the infimum of all such subcategories.

theorem CategoryTheory.ObjectProperty.prop_localizingClosure_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (X : C) : P.localizingClosure X ↔ ∀ (Q : ObjectProperty C), P ≤ Q → Q.IsTriangulated → Q.IsClosedUnderIsomorphisms → (∀ (J : Type v), Q.IsClosedUnderColimitsOfShape (Discrete J)) → Q X

An object lies in the localizing closure of P exactly when it lies in every isomorphism-closed triangulated subcategory containing P and closed under coproducts indexed by Type v.

theorem CategoryTheory.ObjectProperty.le_localizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P ≤ P.localizingClosure

theorem CategoryTheory.ObjectProperty.localizingClosure_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type v), Q.IsClosedUnderColimitsOfShape (Discrete J)] (h : P ≤ Q) : P.localizingClosure ≤ Q

theorem CategoryTheory.ObjectProperty.localizingClosure_le_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {Q : ObjectProperty C} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type v), Q.IsClosedUnderColimitsOfShape (Discrete J)] : P.localizingClosure ≤ Q ↔ P ≤ Q

The universal property of the localizing closure.

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.localizingClosure.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsTriangulatedLocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.localizingClosure.IsTriangulated

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeLocalizingClosureDiscrete {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (J : Type v) : P.localizingClosure.IsClosedUnderColimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsLocalizingClosureOfHasCoproductsOfShapeNat {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [Limits.HasCoproductsOfShape ℕ C] : P.localizingClosure.IsStableUnderRetracts

theorem CategoryTheory.ObjectProperty.triangEnvelope_le_localizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [Limits.HasCoproductsOfShape ℕ C] : P.triangEnvelope ≤ P.localizingClosure

When C has countable coproducts, the thick closure of P is contained in its localizing closure.

theorem CategoryTheory.ObjectProperty.monotone_localizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.localizingClosure ≤ Q.localizingClosure

def CategoryTheory.ObjectProperty.colocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : ObjectProperty C

The colocalizing closure of P: the smallest isomorphism-closed triangulated subcategory containing P and closed under products indexed by types in Type v, defined as the infimum of all such subcategories.

theorem CategoryTheory.ObjectProperty.prop_colocalizingClosure_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (X : C) : P.colocalizingClosure X ↔ ∀ (Q : ObjectProperty C), P ≤ Q → Q.IsTriangulated → Q.IsClosedUnderIsomorphisms → (∀ (J : Type v), Q.IsClosedUnderLimitsOfShape (Discrete J)) → Q X

An object lies in the colocalizing closure of P exactly when it lies in every isomorphism-closed triangulated subcategory containing P and closed under products indexed by Type v.

theorem CategoryTheory.ObjectProperty.le_colocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P ≤ P.colocalizingClosure

theorem CategoryTheory.ObjectProperty.colocalizingClosure_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type v), Q.IsClosedUnderLimitsOfShape (Discrete J)] (h : P ≤ Q) : P.colocalizingClosure ≤ Q

theorem CategoryTheory.ObjectProperty.colocalizingClosure_le_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {Q : ObjectProperty C} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type v), Q.IsClosedUnderLimitsOfShape (Discrete J)] : P.colocalizingClosure ≤ Q ↔ P ≤ Q

The universal property of the colocalizing closure.

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.colocalizingClosure.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsTriangulatedColocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.colocalizingClosure.IsTriangulated

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeColocalizingClosureDiscrete {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (J : Type v) : P.colocalizingClosure.IsClosedUnderLimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsColocalizingClosureOfHasProductsOfShapeNat {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [Limits.HasProductsOfShape ℕ C] : P.colocalizingClosure.IsStableUnderRetracts

theorem CategoryTheory.ObjectProperty.triangEnvelope_le_colocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [Limits.HasProductsOfShape ℕ C] : P.triangEnvelope ≤ P.colocalizingClosure

When C has countable products, the thick closure of P is contained in its colocalizing closure.

theorem CategoryTheory.ObjectProperty.monotone_colocalizingClosure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.colocalizingClosure ≤ Q.colocalizingClosure