Constructing a t-structure from an aisle

This file isolates the formal, non-representability part of the compact-generator existence theorem. An object property is an aisle when it is closed under the relevant shift and every object admits the required approximation triangle. Its right orthogonal is then the coaisle, and the two properties determine a t-structure.

For Theorem A.13 of arXiv:2607.28411v1, Brown representability constructs universal approximation maps. AisleData.ofApproximationMaps completes those maps to distinguished triangles and proves their cones are right orthogonal. This file then assembles the triangles into a t-structure, but does not postulate that compact generators alone produce the universal maps.

structure CategoryTheory.Triangulated.TStructure.ApproximationMap {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (U : ObjectProperty C) (A : C) : Type (max u v)

A universal map from an aisle candidate to an object.

The two Hom conditions are the exact amount of control needed to prove that the cone of hom is right orthogonal to U: surjectivity kills maps through the middle term, while injectivity after [1] kills their connecting maps. Brown representability constructs maps with these properties in the compact-generator application.

• left : C

  The approximating object.

• left_mem : U self.left

  The approximating object belongs to the aisle candidate.

• hom : self.left ⟶ A

  The universal approximation morphism.

• hom_surjective (Z : C) (hZ : U Z) : Function.Surjective fun (f : Z ⟶ self.left) => CategoryStruct.comp f self.hom

  Every map from an object of U to A factors through hom.

• shift_hom_injective (Z : C) (hZ : U Z) : Function.Injective fun (f : Z ⟶ (shiftFunctor C 1).obj self.left) => CategoryStruct.comp f ((shiftFunctor C 1).map self.hom)

  After shifting the approximation triangle, precomposition with hom[1] is injective on maps from objects of U.

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

The data that makes an object property an aisle.

The approximation triangle is the only genuinely existential part. In the compact-generator application it is supplied by Brown representability.

• shift : U ≤ U.shift 1

  Aisles are closed under the shift occurring in the nonpositive half of a t-structure.

• exists_triangle (A : C) : ∃ (X : C) (Y : C) (_ : U X) (_ : U.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 has an aisle/right-orthogonal approximation triangle.

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

Complete universal approximation maps to triangles and prove that their cones lie in the right orthogonal.

This is the exactness step between Brown representability's map-level output and the aisle constructor. In particular, callers no longer have to supply a chosen cone or assert its orthogonality.

theorem CategoryTheory.Triangulated.TStructure.AisleData.rightOrthogonal_le_shift {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {U : ObjectProperty C} (h : AisleData U) : U.rightOrthogonal ≤ U.rightOrthogonal.shift (-1)

The right orthogonal of an aisle is closed under the opposite shift.

noncomputable def CategoryTheory.Triangulated.TStructure.AisleData.tStructure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {U : ObjectProperty C} [U.IsClosedUnderIsomorphisms] (h : AisleData U) : TStructure C

An aisle and its right orthogonal determine a t-structure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.AisleData.tStructure_le_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {U : ObjectProperty C} [U.IsClosedUnderIsomorphisms] (h : AisleData U) : h.tStructure.le 0 = U

@[simp]

theorem CategoryTheory.Triangulated.TStructure.AisleData.tStructure_ge_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {U : ObjectProperty C} [U.IsClosedUnderIsomorphisms] (h : AisleData U) : h.tStructure.ge 1 = U.rightOrthogonal