The categorical core of Polishchuk's inducing theorem #
This file assembles Steps 1--4 of Theorem A.17 in arXiv:2607.28411v1 after the compactly generated large t-structures have been constructed.
The result constructs a bounded t-structure on the selected source
subcategory and proves the recognition formulas (A.3) and (A.4). It does not
assume those formulas or boundedness. The only large-category t-structure
input on the source is the concrete output of Theorem A.13: a TStructure
together with its proved compact-generation formula.
The selected source subcategory comes in three shapes. induce takes the
preimage F⁻¹ Q of a bounded target subcategory, hypothesis (iv) of Theorem
A.17 built in, and proves truncation stability from (iv). induceLarge
takes any triangulated P with truncation stability supplied (Definition
A.7) and recognizes (A.3) and (A.4) against the large target t-structure
itself, with no target subcategory; boundedness comes from
P ⊆ F⁻¹(tD-bounded). induceOfLE is induceLarge read inside a bounded
Q with P ⊆ F⁻¹ Q, the shape Slicing.InducedTStructures consumes, and
induce is its case P = F⁻¹ Q; conversely, once D is triangulated,
induceLarge is induceOfLE at Q = tD.bounded through Mathlib's instances
on TStructure.bounded. No geometric instance of induceOfLE with
P ≠ F⁻¹ Q is claimed.
Theorem 2.8 of arXiv:2607.28411v1 for an infinite extension ℓ/k is in the
large shape: π_* sends no nonzero coherent object into Dᵇ(Coh X), so
P ⊆ F⁻¹ Q fails for Q = Dᵇ(Coh X), and the paper recognizes 𝒫_ℓ
against the Ind-extension on Dqc(X). induceLarge is the Theorem A.17
half of that, one phase at a time; reading the phases into a slicing, the
Corollary A.23 half, is the open item in Phase/Transfer/Inducing.lean.
Scheme realization, bounded-coherent/perfect identification, and S-locality are intentionally absent. They are the geometric layer of SF7.3.
The bounded categorical output of A.17 on a source subcategory P, with
formulas (A.3) and (A.4) stated against the large target t-structure: the
shape in which Theorem 2.8(1) of arXiv:2607.28411v1 recognizes the
base-changed slicing, where F = π_* lands in Dqc(X). The tD-bounded
objects do form a bounded target subcategory (Mathlib's
TStructure.onBounded); what is unavailable there is one carrying the
slicing that contains the image of Dᵇ(Coh X_ℓ).
- tStructure : TStructure P.FullSubcategory
The induced t-structure on the selected source subcategory.
- isBounded : self.tStructure.IsBounded
Step 4: the induced t-structure is bounded.
Formula (A.3), in every degree, against the large target.
Formula (A.4), in every degree, against the large target.
Instances For
The bounded categorical output of A.17 on a source subcategory P ≤ F⁻¹ Q,
with formulas (A.3) and (A.4) stated against the restricted target
t-structure.
- tStructure : TStructure P.FullSubcategory
The induced t-structure on the selected source subcategory.
- isBounded : self.tStructure.IsBounded
Step 4: the induced t-structure is bounded.
- isLE_iff (X : P.FullSubcategory) (n : ℤ) : self.tStructure.IsLE X n ↔ (Q.tStructure tD).IsLE ((ObjectProperty.liftOfLE F hle).obj X) n
Formula (A.3), in every degree.
- isGE_iff (X : P.FullSubcategory) (n : ℤ) : self.tStructure.IsGE X n ↔ (Q.tStructure tD).IsGE ((ObjectProperty.liftOfLE F hle).obj X) n
Formula (A.4), in every degree.
Instances For
InducedTStructureDataLarge read inside a bounded target subcategory
Q ⊇ F(P): the recognition formulas restated through Q.tStructure_isLE_iff
and isGE_iff. The converse restatement holds too, so the two structures
carry the same content once hle is available.
Equations
- d.toInducedTStructureData hle = { tStructure := d.tStructure, isBounded := ⋯, isLE_iff := ⋯, isGE_iff := ⋯ }
Instances For
Theorem A.17, categorical Steps 1--4, with recognition against the large
target t-structure and no target subcategory. Hypothesis (iv) of A.17 is
replaced by truncation stability of P (htrunc, Definition A.7 and Remark
A.8 of arXiv:2607.28411v1) and by hbdd, that F sends P into the
tD-bounded objects; zero reflection is needed on P only. This is the
shape Theorem 2.8(1) needs for the base change π : X_ℓ → X along an
arbitrary field extension: P = Dᵇ(Coh X_ℓ), F = π_* into Dqc(X), tD
the Ind-extension τ̂'_φ -- the Theorem A.17 half of 2.8(1), one phase at a
time. The Corollary A.23 half, reading the phases into a slicing, is open
(Phase/Transfer/Inducing.lean).
Equations
- CategoryTheory.Triangulated.Polishchuk.induceLarge adj P htrunc hF hD hC hmonad hzero hbdd = { tStructure := P.tStructure tC, isBounded := ⋯, isLE_iff := ⋯, isGE_iff := ⋯ }
Instances For
Theorem A.17, categorical Steps 1--4, on a triangulated P ≤ F⁻¹ Q:
induceLarge restated inside Q, boundedness of Q supplying the
bounded-image containment through hle. Hypothesis (iv) of A.17 is used by
the paper only to show the source t-structure restricts to the selected
subcategory; here that conclusion is the hypothesis htrunc, which for
P = F⁻¹ Q is ObjectProperty.hasInducedTStructure_of_preimage (induce).
Zero reflection is needed on P only. This is the shape
Slicing.InducedTStructures consumes, with the slicing on Q; it is not the
shape of Theorem 2.8 for an infinite extension ℓ/k, where hle fails for
Q = Dᵇ(Coh X) and induceLarge applies instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Theorem A.17, categorical Steps 1--4, on the preimage F⁻¹ Q.
The target large t-structure is compactly generated by G; the source large
t-structure is the A.13 output generated by the left-adjoint image of G.
The monad hypothesis proves t-exactness. Detection of the selected
subcategories proves truncation stability, zero reflection proves both
recognition formulas, and boundedness descends from the restricted target.
Zero reflection is assumed only on objects whose image lies in the selected
target subcategory Q -- the object-property form of A.17's
conservativity-on-bounded-objects hypothesis. Until 2026-08-18 it was
demanded on the whole source category, which was sound but strictly stronger
than the source theorem and a materially harder obligation for the scheme
realization (adversarial review, finding P2-11).
Equations
- CategoryTheory.Triangulated.Polishchuk.induce adj hF hD hC hmonad hzero hbounded = CategoryTheory.Triangulated.Polishchuk.induceOfLE adj (Q.inverseImage F) ⋯ ⋯ hF hD hC hmonad hzero hbounded
Instances For
The categorical A.17 constructor with the source t-structure assembled directly from the A.13 approximation triangles.
Compactness of the source generators is derived from the adjunction and target compactness. Thus the only source existence input is the honest Brown- representability approximation output, not a pre-existing t-structure or its compact-generation equality.
Equations
- CategoryTheory.Triangulated.Polishchuk.induceOfApproximation adj hF hD happrox hmonad hzero hbounded = CategoryTheory.Triangulated.Polishchuk.induce adj hF hD ⋯ hmonad hzero hbounded
Instances For
The categorical A.17 constructor using the repository-owned Brown tower.
The source compact generators are the left-adjoint images of the target generators. Their compactness follows from the adjunction and coproduct preservation. The remaining size and shift-closure assumptions are stated explicitly, so no approximation-map or global inducing theorem is accepted from the caller.
Equations
- CategoryTheory.Triangulated.Polishchuk.induceOfBrown adj hF hD hshift hmonad hzero hbounded = CategoryTheory.Triangulated.Polishchuk.induceOfApproximation adj hF hD ⋯ hmonad hzero hbounded
Instances For
The categorical A.17 constructor from Brown-style universal maps.
The source approximation triangles and the proof that their cones are right
orthogonal are both constructed internally. The remaining representability
input is precisely the existence of universal maps with the two Hom controls
recorded by TStructure.ApproximationMap.
Equations
- One or more equations did not get rendered due to their size.