Generation invariants under triangulated functors

Main results

• CategoryTheory.ObjectProperty.generationTime_map_le compares generation times of image properties.
• CategoryTheory.ObjectProperty.generationTime_map_eq_of_equiv states generation-time invariance under a triangulated equivalence.
• CategoryTheory.Triangulated.rouquierDim_le_of_retract_coverage proves dimension monotonicity when every target object is a retract of a functor image.
• CategoryTheory.Triangulated.rouquierDim_le_of_essSurj specializes that bound to essentially surjective functors.
• CategoryTheory.Triangulated.rouquierDim_eq_of_equiv states Rouquier-dimension invariance under a triangulated equivalence.

Implementation notes

These results use the forward envelope transport in CategoryTheory.ObjectProperty.triangEnvelopeIter_map_le. Rouquier dimension is indexed by single objects, so target-wide results require retract coverage of the target; essential surjectivity supplies this premise. Equivalence results use Mathlib's construction of a triangulated quasi-inverse: its shift compatibility and exactness follow from the adjunction associated to the equivalence.

References

• Raphaël Rouquier, Dimensions of triangulated categories.
• Mathlib.CategoryTheory.Triangulated.Generators for the envelope tower.

Tags

generation time, Rouquier dimension, triangulated category, exact functor

theorem CategoryTheory.ObjectProperty.generationTime_map_le {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (P Q : ObjectProperty C) : (P.map F).generationTime (Q.map F) ≤ P.generationTime Q

Generation time does not increase after applying a triangulated functor to both properties. No essential-surjectivity hypothesis is needed because the target property is the essential image of the source property.

theorem CategoryTheory.ObjectProperty.generationTime_map_eq_of_equiv {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.functor.IsTriangulated] (P Q : ObjectProperty C) : (P.map E.functor).generationTime (Q.map E.functor) = P.generationTime Q

Generation time is invariant under a triangulated equivalence. The image properties are essential images under E.functor; because envelope stages are invariant under isomorphism, they have the same generation time as their source properties. The triangulated structure on the quasi-inverse is supplied by Mathlib's equivalence adjunction.

theorem CategoryTheory.Triangulated.rouquierDim_le_of_retract_coverage {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (hCover : ∀ (Y : D), ∃ (X : C), Nonempty (Retract Y (F.obj X))) : rouquierDim D ≤ rouquierDim C

Rouquier dimension is monotone under a triangulated functor whose image is retract-dense: every target object is a retract of some image.

theorem CategoryTheory.Triangulated.rouquierDim_le_of_essSurj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.EssSurj] : rouquierDim D ≤ rouquierDim C

Rouquier dimension cannot increase under an essentially-surjective triangulated functor. Essential surjectivity supplies the retract-coverage premise of CategoryTheory.Triangulated.rouquierDim_le_of_retract_coverage.

theorem CategoryTheory.Triangulated.rouquierDim_eq_of_equiv {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.functor.IsTriangulated] : rouquierDim C = rouquierDim D

A triangulated equivalence preserves Rouquier dimension. Mathlib supplies the compatible shift structure and triangulated structure on the quasi-inverse from the equivalence adjunction.