Functor transport for triangulated generators

Main results

• CategoryTheory.ObjectProperty.triangEnvelopeIter_map_obj_of_le transports a stage when generators satisfy an arbitrary target property.
• CategoryTheory.ObjectProperty.triangEnvelopeIter_map_obj and CategoryTheory.ObjectProperty.triangEnvelopeIter_map_le specialize transport to CategoryTheory.ObjectProperty.map.
• CategoryTheory.Triangulated.singleton_triangEnvelopeIter_map_obj transports the tower generated by a single object.
• CategoryTheory.Triangulated.singleton_triangEnvelopeIter_top_of_retract_coverage preserves a fixed strong-generation stage under retract coverage.
• CategoryTheory.Triangulated.isStrongTriangulatedGenerator_map_of_retract_coverage transports a strong generator when every target object is a retract of a functor image.
• CategoryTheory.Triangulated.exists_isStrongTriangulatedGenerator_iff_of_equiv records invariance of strong generation under a triangulated equivalence.

Implementation notes

A stage induction transports shifts, binary products, retracts, and distinguished triangles separately, in the order used by Mathlib's envelope tower. The arbitrary target property lets callers specialize directly to a singleton without first identifying its essential-image property. The pointwise theorem asserts only forward transport: the reverse inclusion can fail because a target envelope can contain objects outside the functor's essential image.

The source and target need only be pretriangulated with the structures required by CategoryTheory.ObjectProperty.triangEnvelopeIter. The functor hypotheses are exactly [F.CommShift ℤ] [F.IsTriangulated]; Mathlib derives additivity and preservation of binary products. No octahedral IsTriangulated structure on either ambient category is required.

References

• Mathlib's CategoryTheory.ObjectProperty.triangEnvelopeIter is defined in Mathlib.CategoryTheory.Triangulated.Generators.
• Rouquier, Dimensions of triangulated categories.

Tags

triangulated category, exact functor, generation, strong generator

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_map_obj_of_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 : ObjectProperty C) (Q : ObjectProperty D) (h : ∀ (X : C), P X → Q (F.obj X)) (X : C) (n : ℕ) (hX : P.triangEnvelopeIter n X) : Q.triangEnvelopeIter n (F.obj X)

Induct on the envelope stage, transporting shifts, binary products, retracts, and distinguished triangles separately. The arbitrary target property lets callers specialize directly to a singleton without first identifying its essential-image property.

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_map_obj {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 : ObjectProperty C) (n : ℕ) {X : C} (hX : P.triangEnvelopeIter n X) : (P.map F).triangEnvelopeIter n (F.obj X)

An exact functor carries every object in stage n of the source envelope into stage n generated by the essential-image property in the target. This is a forward pointwise statement; it does not assert that every object in the target stage lifts to the source.

theorem CategoryTheory.ObjectProperty.triangEnvelopeIter_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 : ObjectProperty C) (n : ℕ) : (P.triangEnvelopeIter n).map F ≤ (P.map F).triangEnvelopeIter n

The object-property form of CategoryTheory.ObjectProperty.triangEnvelopeIter_map_obj, for CategoryTheory.ObjectProperty.map applied to F. The direction is forward; the reverse inclusion fails for a general functor.

theorem CategoryTheory.Triangulated.singleton_triangEnvelopeIter_map_obj {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] (G : C) (n : ℕ) {X : C} (hX : (ObjectProperty.singleton G).triangEnvelopeIter n X) : (ObjectProperty.singleton (F.obj G)).triangEnvelopeIter n (F.obj X)

Stage membership generated by a single object transports to the stage generated by its image.

theorem CategoryTheory.Triangulated.singleton_triangEnvelopeIter_top_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))) (G : C) (n : ℕ) (hn : (ObjectProperty.singleton G).triangEnvelopeIter n = ⊤) : (ObjectProperty.singleton (F.obj G)).triangEnvelopeIter n = ⊤

A fixed envelope stage generated by one object remains the whole target when every target object is a retract of an image. The stage index is preserved.

theorem CategoryTheory.Triangulated.isStrongTriangulatedGenerator_map_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))) (G : C) (hG : (ObjectProperty.singleton G).IsStrongTriangulatedGenerator) : (ObjectProperty.singleton (F.obj G)).IsStrongTriangulatedGenerator

A triangulated functor carries a strong generator to a strong generator whenever every target object is a retract of an object in its image. Essential surjectivity supplies this retract coverage, but the explicit premise also applies to functors whose image is only retract-dense.

theorem CategoryTheory.Triangulated.exists_isStrongTriangulatedGenerator_iff_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] : (∃ (G : C), (ObjectProperty.singleton G).IsStrongTriangulatedGenerator) ↔ ∃ (H : D), (ObjectProperty.singleton H).IsStrongTriangulatedGenerator

Strong generation is invariant under a triangulated equivalence. The inverse's compatible shift structure and exactness follow from the equivalence adjunction in Mathlib.