Projections onto compactly generated aisles

The t-structure assembled from a compact-generator approximation has Coprod(G) as its zero aisle. This file turns its truncation functor into chosen right-projection data onto Coprod(G).

Right admissibility is automatic when G is triangulated. Preservation of small coproducts is deliberately stated in terms of the corresponding truncation functor: this is the precise continuity input needed later for base-change decompositions, and is not a formal consequence of an arbitrary t-structure.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.rightProjectionData {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (h : CompactGeneratorApproximation G) : G.coprodClosure.RightProjectionData

The chosen right projection onto the coproduct-and-extension closure of the generators.

Equations

• h.rightProjectionData = (h.tStructure.aisleRightProjectionData 0).ofEq ⋯

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.coprodClosure_isRightAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (h : CompactGeneratorApproximation G) [G.IsTriangulated] : G.coprodClosure.IsRightAdmissible

A coproduct closure of triangulated generators is right admissible once the compact-generator approximation has been constructed.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.rightProjectionData_preservesSmallCoproducts {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (h : CompactGeneratorApproximation G) (htrunc : (h.tStructure.truncLE 0).PreservesSmallCoproducts) : h.rightProjectionData.ambientProjection.PreservesSmallCoproducts

Continuity of zero truncation transfers to the chosen ambient projection onto Coprod(G).