Composition of triangulated envelope stages

This file extends Mathlib's existing CategoryTheory.ObjectProperty.triangEnvelopeIter tower. It proves a fixed-point property for its iterates, a composition law, transfer through an intermediate property, and the bounded object-property form of Stacks 0FXA.

Main definitions

This file introduces no definitions. It reuses Mathlib's CategoryTheory.ObjectProperty.triangEnvelopeIter, CategoryTheory.ObjectProperty.extensionProduct, CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator, and CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator.

Main results

• CategoryTheory.ObjectProperty.triangEnvelopeIter_zero_le: each iterate is fixed by stage zero.
• CategoryTheory.ObjectProperty.triangEnvelopeIter_compose: composes two finite stages.
• CategoryTheory.ObjectProperty.le_triangEnvelopeIter_of_le_triangEnvelopeIter: transfers a bound through an intermediate property.
• CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_of_strong_le_iter: bounded strong generation implies strong generation.
• CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_of_isClassical_of_singleton_strong: a classical generator containing a strong singleton is strong.

Implementation notes

The product-closure proof uses products of retracts and the product of two distinguished triangles. It keeps the existing closure operations and uses CategoryTheory.ObjectProperty.triangEnvelopeIter_succ, so the fixed-point lemma needs no triangulated-category hypothesis. The empty property has empty iterates; the nonempty branch supplies the zero object required by the finite-product closure argument.

References

• The Stacks Project, Section 13.36, Lemma 13.36.6, tag 0FXA.
• Mathlib.CategoryTheory.Triangulated.Generators
• Mathlib.CategoryTheory.Triangulated.Subcategory

Tags

triangulated category, envelope composition, strong generator, Stacks 0FXA

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

The zeroth envelope of an iterated envelope is contained in that stage. For a nonempty generator property its iterates contain zero; an empty property has empty iterates.

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_compose {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (P : ObjectProperty C) (m n : ℕ) : (P.triangEnvelopeIter m).triangEnvelopeIter n ≤ P.triangEnvelopeIter (m * n + m + n)

Composition of two finite generation stages has the multiplicative bound m * n + m + n. In Rouquier's indexing, where stage n is ⟨P⟩_(n+1), this is the composition law ⟨⟨P⟩_a⟩b ⊆ ⟨P⟩(a*b).

theorem CategoryTheory.ObjectProperty.le_triangEnvelopeIter_of_le_triangEnvelopeIter {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {P Q R : ObjectProperty C} {m n : ℕ} (hQP : Q ≤ P.triangEnvelopeIter m) (hRQ : R ≤ Q.triangEnvelopeIter n) : R ≤ P.triangEnvelopeIter (m * n + m + n)

Monotonicity replaces the intermediate property by the P-stage at m; the composition lemma then gives the stated bound.

theorem CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_of_strong_le_iter {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (P Q : ObjectProperty C) (k : ℕ) (hQ : Q.IsStrongTriangulatedGenerator) (hQP : Q ≤ P.triangEnvelopeIter k) : P.IsStrongTriangulatedGenerator

A uniformly bounded stage reduces strong generation to the composition lemma. The pointwise condition Q ≤ CategoryTheory.ObjectProperty.triangEnvelope P does not provide such a k: the stage may vary with the object of Q, so this argument does not establish the unrestricted object-property analogue.

theorem CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_of_isClassical_of_singleton_strong {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (P : ObjectProperty C) (G : C) (hP : P.IsClassicalTriangulatedGenerator) (hG : (singleton G).IsStrongTriangulatedGenerator) : P.IsStrongTriangulatedGenerator

The classical property places the singleton in one finite stage, so the bounded strong-generation theorem applies.