Restricting t-structures detected by a t-exact functor #
This file formalizes Steps 2--4 of Polishchuk's Theorem A.17 from arXiv:2607.28411v1. If a t-exact functor detects membership in chosen bounded subcategories, then restriction of the target t-structure forces restriction of the source t-structure. If the functor also reflects zero objects, the two halves of the restricted source t-structure are recognized exactly on the target; these are formulas (A.3) and (A.4). Boundedness of the restricted source t-structure then follows from boundedness of the images, which is Step 4.
The theorem is independent of schemes and of the compact-generation argument that constructs the large source t-structure in Step 1.
The functor and adjunction restrictions this file used to own -- liftOfLE,
preimageLift, inverseImageLift, liftToInverseImage, and the two
Adjunction.restrictInverseImage* -- mention no t-structure and now live at
their carrier's path, CategoryTheory/ObjectProperty/Lift.lean,
which this file imports.
Main results #
ObjectProperty.hasInducedTStructure_of_preimage: Step 2, restriction of the source t-structure from detection of the two subcategories.ObjectProperty.isLE_iff_isLE_map,isGE_iff_isGE_map: Step 3, formulas (A.3) and (A.4) against the large target t-structure, with no target subcategory, the shape Theorem 2.8(1) recognizes the base-changed slicing in.tStructure_isLE_iff_map_of_leandtStructure_isGE_iff_map_of_lerestate them insideQforP ≤ F⁻¹ Q, andtStructure_isLE_iff_map,tStructure_isGE_iff_mapare their two-way detection cases.ObjectProperty.tStructure_isBounded_of_le_bounded_inverseImage: Step 4 in that shape, together withtStructure_isBounded_iff_le_bounded, the form in which a bounded target subcategory supplies its hypothesis.
References #
- arXiv:2607.28411v1, Theorem A.17 (Steps 2--4) and Proposition 3.8.
Step 2 of A.17: restriction of the target t-structure and detection of the two bounded subcategories imply restriction of the source t-structure.
The proof compares truncations using Functor.mapTruncLEIso and
Functor.mapTruncGEIso. Thus the conclusion is derived from t-exactness and
bounded-subcategory detection; it is not included among the premises.
Formula (A.3) against the large target t-structure, with no target
subcategory: the content of Step 3 of Theorem A.17, in the shape Theorem 2.8(1)
of arXiv:2607.28411v1 recognizes the base-changed slicing. Right t-exactness
gives →; for ←, F (τ^{≥ n+1} X) ≅ τ'^{≥ n+1} (F X) = 0 by t-exactness,
τ^{≥ n+1} X ∈ P by P.HasInducedTStructure t, and zero reflection at that
truncation finishes. That is why truncation stability of P and zero
reflection on P are exactly the hypotheses.
Formula (A.3) on the restricted categories, for P ≤ F⁻¹ Q: the large
target statement isLE_iff_isLE_map, restated inside Q. hle enters only
in that restatement.
Formula (A.3) on the restricted categories.
Zero reflection is required only on objects of P, matching A.17's
conservativity-on-bounded-objects hypothesis: the proof applies hzero at a
truncation of an object of P, and truncations stay in P by the induced
t-structure. A caller with global conservativity weakens it pointwise.
Formula (A.4) against the large target t-structure, as
isLE_iff_isLE_map.
The induced t-structure on Q is bounded exactly when Q consists of
t'-bounded objects, the form in which Step 4 of Theorem A.17 consumes a
bounded target subcategory.
Step 4 of Theorem A.17 with no target subcategory: if F sends P into
the t'-bounded objects, the induced t-structure on P is bounded.
Formula (A.4) on the restricted categories, for P ≤ F⁻¹ Q, as
tStructure_isLE_iff_map_of_le.
Formula (A.4) on the restricted categories.
As in tStructure_isLE_iff_map, zero reflection is required only on objects
of P.