Generators in triangulated categories

We define the notions of strong and classical generators in (pre)triangulated categories. This is not to be confused with ObjectProperty.IsStrongGenerator defined in CategoryTheory/Generator.

Main definitions

• ObjectProperty.triangEnvelopeIter P n: The object property of all objects reachable from P by shifts, binary products, retracts and at most n extensions.
• ObjectProperty.triangEnvelope P: The triangulated envelope of P, i.e., the object property of all objects reachable from P by shifts, binary products, retracts and extensions. This is the smallest triangulated object property closed under retracts that contains P, see ObjectProperty.triangEnvelope_le_iff.
• ObjectProperty.IsStrongTriangulatedGenerator P: P is a strong triangulated generator if there exists n such that every object is in P.triangEnvelopeIter n.
• ObjectProperty.IsClassicalTriangulatedGenerator P: P is a classical triangulated generator if every object is in P.triangEnvelope.

Main results

• ObjectProperty.triangEnvelope_le_iff: The universal property of P.triangEnvelope: it is the smallest triangulated object property closed under retracts that contains P.
• ObjectProperty.IsStrongTriangulatedGenerator.isClassicalTriangulatedGenerator: A strong triangulated generator is a classical triangulated generator.

TODO

• Prove that if C has a strong generator and P is a classical generator, then P is a strong generator (stacks 0FXA).

References

• Bondal and Van den Bergh, Generators and representability of functors in commutative and noncommutative geometry
• Stacks 09SJ

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.triangEnvelopeIter {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : ObjectProperty C

All objects that can be reached by shifts, binary products, retracts and at most n extensions from objects in P.

Equations

• P.triangEnvelopeIter n = ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure

@[simp]

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_zero {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_succ {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : P.triangEnvelopeIter (n + 1) = ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_succ' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] (n : ℕ) : P.triangEnvelopeIter (n + 1) = ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_add {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] {n m n' : ℕ} (h : n = n' + 1 := by lia) : P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n').extensionProduct (P.triangEnvelopeIter m)).retractClosure

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_add' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] {n m m' : ℕ} (h : m = m' + 1 := by lia) : P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m')).retractClosure

theorem CategoryTheory.ObjectProperty.monotone_triangEnvelopeIter {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (hPQ : P ≤ Q) (n : ℕ) : P.triangEnvelopeIter n ≤ Q.triangEnvelopeIter n

theorem CategoryTheory.ObjectProperty.monotone'_triangEnvelopeIter {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {n m : ℕ} (h : n ≤ m := by lia) : P.triangEnvelopeIter n ≤ P.triangEnvelopeIter m

theorem CategoryTheory.ObjectProperty.le_triangEnvelopeIter {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : P ≤ P.triangEnvelopeIter n

def CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

An object property P is called a strong triangulated generator, if every object can be reached from objects in P by shifts, binary products, retracts and at most n extensions, for some fixed n.

Equations

• P.IsStrongTriangulatedGenerator = ∃ (n : ℕ), P.triangEnvelopeIter n = ⊤

theorem CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.IsStrongTriangulatedGenerator ↔ ∃ (n : ℕ), P.triangEnvelopeIter n = ⊤

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

All objects that can be reached by shifts, binary products, retracts and extensions from objects in P. This is the smallest triangulated object property closed under retracts that contains P, see ObjectProperty.triangEnvelope_le_iff.

Equations

• P.triangEnvelope = ⨆ (n : ℕ), P.triangEnvelopeIter n

theorem CategoryTheory.ObjectProperty.prop_triangEnvelope_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (X : C) : P.triangEnvelope X ↔ ∃ (n : ℕ), P.triangEnvelopeIter n X

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_le_triangEnvelope {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : P.triangEnvelopeIter n ≤ P.triangEnvelope

theorem CategoryTheory.ObjectProperty.le_triangEnvelope {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P ≤ P.triangEnvelope

instance CategoryTheory.ObjectProperty.instNonemptyTriangEnvelope {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.Nonempty] : P.triangEnvelope.Nonempty

theorem CategoryTheory.ObjectProperty.monotone_triangEnvelope {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.triangEnvelope ≤ Q.triangEnvelope

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsTriangEnvelope {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.triangEnvelope.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftTriangEnvelopeInt {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.triangEnvelope.IsStableUnderShift ℤ

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂TriangEnvelopeOfIsTriangulated {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] : P.triangEnvelope.IsTriangulatedClosed₂

instance CategoryTheory.ObjectProperty.instIsTriangulatedTriangEnvelopeOfNonemptyOfIsTriangulated {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.Nonempty] [IsTriangulated C] : P.triangEnvelope.IsTriangulated

theorem CategoryTheory.ObjectProperty.triangEnvelope_le_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {Q : ObjectProperty C} [Q.IsStableUnderRetracts] [Q.IsTriangulated] : P.triangEnvelope ≤ Q ↔ P ≤ Q

def CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

An object property P is called a classical generator, if every object can be reached from objects in P by shifts, binary products, retracts and extensions.

Equations

• P.IsClassicalTriangulatedGenerator = (P.triangEnvelope = ⊤)

theorem CategoryTheory.ObjectProperty.isClassicalTriangulatedGenerator_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.IsClassicalTriangulatedGenerator ↔ P.triangEnvelope = ⊤

theorem CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator.isClassicalTriangulatedGenerator {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (h : P.IsStrongTriangulatedGenerator) : P.IsClassicalTriangulatedGenerator