The compact-generator t-structure constructor

This file formalizes the final assembly in Theorem A.13 of arXiv:2607.28411v1. A shift-stable family of generators makes Coprod(G) shift-stable. Once Brown representability supplies an approximation triangle with left term in Coprod(G) and right term in its right orthogonal, the aisle constructor produces the compactly generated t-structure and formula (A.2).

The structure CompactGeneratorApproximation contains those approximation triangles, while ofApproximationMaps constructs them from Brown-style universal maps and proves the required orthogonality. This file isolates the assembly interface; CompactlyGenerated.Brown constructs the universal maps from compact generators under explicit universe-zero smallness, local-smallness, coproduct, compactness, and shift-closure hypotheses.

theorem CategoryTheory.ObjectProperty.coprodClosure_le_shift {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (hG : G ≤ G.shift 1) : G.coprodClosure ≤ G.coprodClosure.shift 1

If the generators are closed under [1], so is their coproduct-and-extension closure. This is Remark A.12(1) propagated through Coprod.

structure CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (G : ObjectProperty C) : Prop

The approximation output needed in the Brown-representability step of Theorem A.13.

• generator_shift : G ≤ G.shift 1

  The chosen generating family satisfies G[1] ⊆ G, in object-property form.

• exists_triangle (A : C) : ∃ (X : C) (Y : C) (_ : G.coprodClosure X) (_ : G.coprodClosure.rightOrthogonal Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

  Every object admits the approximation triangle constructed by Brown representability.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.ofApproximationMaps {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (hG : G ≤ G.shift 1) (happrox : ∀ (A : C), Nonempty (ApproximationMap G.coprodClosure A)) : CompactGeneratorApproximation G

Brown-style universal maps produce the approximation triangles required by Theorem A.13.

The cone and its right-orthogonality are constructed internally by AisleData.ofApproximationMaps; callers only provide the generator shift and the two Hom controls on the universal maps.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.aisleData {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) : AisleData G.coprodClosure

The approximation data make Coprod(G) an aisle.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.tStructure {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) : TStructure C

The t-structure assembled from the Brown-representability approximation triangles.

Equations

• h.tStructure = ⋯.tStructure

@[simp]

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.tStructure_le_zero {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) : h.tStructure.le 0 = G.coprodClosure

@[simp]

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.tStructure_ge_one {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) : h.tStructure.ge 1 = G.coprodClosure.rightOrthogonal

Formula (A.2): the degree-one coaisle is the right orthogonal of Coprod(G).

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.isCompactlyGeneratedBy {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) (hcompact : G ≤ ObjectProperty.compactObjects) : h.tStructure.IsCompactlyGeneratedBy G

The assembled t-structure is compactly generated by G once compactness of the generators is supplied.