Ind-extended t-structures #
This file proves the categorical restriction argument in Lemma A.14 of
arXiv:2607.28411v1. An Ind-extension has a compactly generated large
t-structure, aisle Coprod(Dᵇ≤0), and restriction equal to the original
bounded t-structure.
The record is theorem output data, not a replacement for Neeman's theorem.
IndExtensionData.ofApproximation derives the large t-structure, aisle
formula, and compact generation from the A.13 output. The orthogonality
argument below proves the restriction statements internally; callers do not
supply them. A separate constructor allows a compact generating property
whose coproduct-and-extension closure agrees with Coprod(Dᵇ≤0), avoiding the
false assertion that every bounded coherent complex is compact.
The large-category image of the nonpositive objects in a t-structure on a full subcategory.
Equations
- CategoryTheory.Triangulated.TStructure.boundedAisle P t = (t.le 0).map P.ι
Instances For
An object in the degree-one coaisle of the small t-structure is right orthogonal, in the ambient category, to the coproduct-and-extension closure of the mapped small aisle. This is the orthogonality observation in the proof of Lemma A.14.
Only the generator case is proved here: the three closure cases are
ObjectProperty.coprodClosure_le's hypotheses, and each is an instance on
ObjectProperty.leftOrthogonal.
The mapped small aisle is contained in any large aisle whose degree-zero part is its coproduct-and-extension closure.
Degree zero of the large t-structure restricts to degree zero of the small t-structure.
Degree one of the large t-structure restricts to degree one of the small t-structure.
The image of a small aisle is closed under the shift required by the compact-generator Brown construction.
The degree-zero restriction equality propagates to every coconnective degree by shifting.
The degree-one restriction equality propagates to every connective degree by shifting.
The aisle equality constructs the induced t-structure on the selected full subcategory; truncation stability is a theorem, not caller data.
The precise output package of Lemma A.14.
largeAisle is clause (i), compactlyGenerated is clause (ii), and the two
restriction equivalences are clause (iii).
- small_isBounded : small.IsBounded
The original t-structure is bounded.
Clause (i): the large aisle is
Coprodof the bounded aisle.- compactlyGenerated : ∃ (G : ObjectProperty C), large.IsCompactlyGeneratedBy G
Clause (ii): the large t-structure is compactly generated.
- hasInduced : P.HasInducedTStructure large
The large t-structure restricts to the selected full subcategory.
Clause (iii), coconnective half, in every degree.
Clause (iii), connective half, in every degree.
Instances For
Formal restriction consequences #
The two degreewise equivalences in IndExtensionData are already the
restriction theorem needed by the Ind/filtered-colimit presentation. Keeping
the consequence here prevents downstream Theorem 5.3 code from rebuilding a
second restriction carrier or treating t-exactness as another geometric input.
The inclusion of the selected small category is t-exact for the large t-structure carried by an Ind extension.
Package the large t-structure as the existing one-functor restriction
record. The target is not a new t-structure carrier: it is the large
field already supplied to IndExtensionData.
Equations
- CategoryTheory.Triangulated.TStructure.IndExtensionData.restriction P small large h = { tStructure := large, isTExact := ⋯ }
Instances For
Assemble A.14 from a compact generating property whose Coprod closure
is the closure of the mapped bounded aisle.
This is the correct Neeman-style boundary: G consists of compact objects,
but the objects of Dᵇ≤0 themselves need not be compact. The A.13
approximation supplies the large t-structure. The aisle equality then proves
truncation stability and both restriction equivalences internally.
Specialization of ofCompactGenerators in which the mapped bounded
aisle itself consists of compact objects. This stronger hypothesis is useful
categorically, but is not imposed by the scheme-level A.14 constructor.
Construct the full A.14 output directly from the owned Brown tower and a Neeman-style compact generating property.
The only comparison input is the honest geometric statement that the compact generators and the mapped bounded aisle have the same coproduct-and-extension closure. Restriction is no longer supplied by the caller.