Rouquier dimension

CategoryTheory.Triangulated.rouquierDim C is the infimum of the generation times from singleton object properties to the whole category. Thus the infimum ranges over individual objects, not arbitrary object properties. It is a scalar definition and does not choose a distinguished object attaining the infimum. Since a category with a zero object is nonempty and ℕ∞ is well ordered, a minimizing object does exist existentially; the finite-witness results below state their witnesses separately.

The indexing has no offset from Rouquier's ⟨G⟩_{n+1} convention: CategoryTheory.ObjectProperty.triangEnvelopeIter_zero identifies stage zero with the shifts, finite binary products, and retracts of G, which is ⟨G⟩₁; CategoryTheory.ObjectProperty.triangEnvelopeIter_succ adds one extension at the next stage. The equation CategoryTheory.ObjectProperty.triangEnvelopeIter_add is a conditional decomposition of envelope stages under [IsTriangulated C]. It is not a generation-time composition or subadditivity law. The generic multiplicative composition theorem is proved beside Mathlib's generator API in CategoryTheory/Triangulated/Generators/Composition.lean; its +1 generation-time consequence is in Dimension/Composition.lean. The additive generation-time inequality is false.

Main definitions

• CategoryTheory.Triangulated.rouquierDim C: the infimum of generation times over singleton object properties.

Main results

• CategoryTheory.Triangulated.rouquierDim_le_coe_iff: a finite bound is witnessed by one object whose envelope reaches the whole category at that stage.
• CategoryTheory.Triangulated.rouquierDim_ne_top_iff_exists_strong and CategoryTheory.Triangulated.exists_isClassicalTriangulatedGenerator_of_rouquierDim_ne_top: finite Rouquier dimension is equivalent to strong generation and implies classical generation.
• CategoryTheory.Triangulated.rouquierDim_eq_zero_iff: dimension zero is generation using shifts, finite binary products, and retracts, without extension steps.

Implementation notes

The category's zero object makes the index type nonempty. Since ℕ∞ is well ordered, the infimum is attained by some object, although the scalar definition does not select that object. The finite-bound and strong-generator theorems extract a witness when one is needed.

References

• Raphaël Rouquier, Dimensions of triangulated categories.

Tags

Rouquier dimension, triangulated category, strong generator, classical generator

noncomputable def CategoryTheory.Triangulated.rouquierDim (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : ℕ∞

The scalar invariant leaves the minimizing object out of the API; the zero-object hypothesis makes the index nonempty, so the infimum is attained in ℕ∞.

Equations

• CategoryTheory.Triangulated.rouquierDim C = ⨅ (G : C), (CategoryTheory.ObjectProperty.singleton G).generationTime ⊤

theorem CategoryTheory.Triangulated.rouquierDim_le_coe_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (n : ℕ) : rouquierDim C ≤ ↑n ↔ ∃ (G : C), (ObjectProperty.singleton G).triangEnvelopeIter n = ⊤

The zero object makes the indexing type nonempty, so the ℕ∞ infimum attains its value; this equivalence extracts a witness at the requested finite stage.

theorem CategoryTheory.Triangulated.rouquierDim_ne_top_iff_exists_strong (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : rouquierDim C ≠ ⊤ ↔ ∃ (G : C), (ObjectProperty.singleton G).IsStrongTriangulatedGenerator

Well-ordering of ℕ∞ makes the infimum attainable; the generation-time bridge identifies a finite value with strong generation.

theorem CategoryTheory.Triangulated.exists_isClassicalTriangulatedGenerator_of_rouquierDim_ne_top (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (h : rouquierDim C ≠ ⊤) : ∃ (G : C), (ObjectProperty.singleton G).IsClassicalTriangulatedGenerator

Mathlib's strong-to-classical implication turns the strong generator from the finite-dimension characterization into a classical generator.

theorem CategoryTheory.Triangulated.rouquierDim_eq_zero_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : rouquierDim C = 0 ↔ ∃ (G : C), (ObjectProperty.singleton G).triangEnvelopeIter 0 = ⊤

Rouquier dimension is zero exactly when one object's zeroth envelope is the whole category. By CategoryTheory.ObjectProperty.triangEnvelopeIter_zero, this is generation using only shifts, finite binary products, and retracts, without extension steps.