Formal owner boundaries for Theorem 5.3

This module records the reusable categorical consequences of Theorem 5.3 of arXiv:1902.08184v4 without claiming the scheme-level base-change theorems.

Main definitions

• inRange packages the lower- and upper-truncation conditions used by the bounded-range formulas.
• PreservesFilteredColimitTruncations is owned by the categorical t-structure module; its PreservesColimit binders remain direct owner inputs.

Main results

• inclusion_isTExact and aisle_eq_coprodClosure reuse the canonical IndExtensionData consequences.
• The exactness transport lemmas expose one-sided and two-sided hypotheses separately, so a caller cannot accidentally strengthen (4a) or (4b).
• inRange_iff_of_components and local_inRange_iff_of_components compose explicit lower- and upper-truncation comparison formulas; they do not package a geometric descent theorem as a carrier.

Implementation notes

Theorem 5.3(3), the flat/fpqc formulas, and (5.3)--(5.4) are geometric owner boundaries in this repository. The functor, local t-structure, comparison formula, finite-amplitude, and S-locality hypotheses must be supplied by the owning geometry layer. This file only composes those inputs with the canonical t-structure API.

References

• BLMNPS, arXiv:1902.08184v4, Lemma 5.1 and Theorem 5.3.

Tags

Theorem53, base-change, t-structure, filtered-colimit, owner-boundary

Lemma 5.1: reuse the canonical Ind-extension

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.inclusion_isTExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {P : CategoryTheory.ObjectProperty C} [P.IsTriangulated] (small : CategoryTheory.Triangulated.TStructure P.FullSubcategory) (large : CategoryTheory.Triangulated.TStructure C) (extension : CategoryTheory.Triangulated.TStructure.IndExtensionData P small large) : P.ι.IsTExact small large

The inclusion t-exactness consequence already proved by IndExtensionData.

The extension data is the theorem output for the categorical layer; no second bridge carrier is needed to expose this consequence at the family owner.

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.aisle_eq_coprodClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {P : CategoryTheory.ObjectProperty C} [P.IsTriangulated] (small : CategoryTheory.Triangulated.TStructure P.FullSubcategory) (large : CategoryTheory.Triangulated.TStructure C) (extension : CategoryTheory.Triangulated.TStructure.IndExtensionData P small large) : large.le 0 = (CategoryTheory.Triangulated.TStructure.boundedAisle P small).coprodClosure

The coproduct-and-extension aisle comparison supplied by the Ind extension.

(5.1)/(5.2): bounded-range owner formulas

def AlgebraicGeometry.DerivedCategory.Families.Theorem53.inRange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) : Prop

Membership in the inclusive bounded interval [a,b] of a t-structure.

Equations

• AlgebraicGeometry.DerivedCategory.Families.Theorem53.inRange t X a b = (t.IsGE X a ∧ t.IsLE X b)

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.inRange_iff_of_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {t : CategoryTheory.Triangulated.TStructure C} {I : Type w'} {D : I → Type u'} [(i : I) → CategoryTheory.Category.{v', u'} (D i)] [∀ (i : I), CategoryTheory.Limits.HasZeroObject (D i)] [(i : I) → CategoryTheory.HasShift (D i) ℤ] [(i : I) → CategoryTheory.Preadditive (D i)] [∀ (i : I) (n : ℤ), (CategoryTheory.shiftFunctor (D i) n).Additive] [(i : I) → CategoryTheory.Pretriangulated (D i)] (restriction : (i : I) → CategoryTheory.Functor C (D i)) (localTStructure : (i : I) → CategoryTheory.Triangulated.TStructure (D i)) (isGE_iff : ∀ (X : C) (a : ℤ), t.IsGE X a ↔ ∀ (i : I), (localTStructure i).IsGE ((restriction i).obj X) a) (isLE_iff : ∀ (X : C) (b : ℤ), t.IsLE X b ↔ ∀ (i : I), (localTStructure i).IsLE ((restriction i).obj X) b) (X : C) (a b : ℤ) : inRange t X a b ↔ ∀ (i : I), inRange (localTStructure i) ((restriction i).obj X) a b

Compose source-shaped lower- and upper-truncation descent formulas.

The restriction functors and local t-structures are explicit arguments. The two component formulas are the external flat/fpqc owner theorems, not fields hidden inside a new descent carrier.

(3), (4a)--(4d): exactness owner boundaries

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.rightTExact_isLE_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] {t : CategoryTheory.Triangulated.TStructure C} {t' : CategoryTheory.Triangulated.TStructure D} (F : CategoryTheory.Functor C D) (hF : F.IsRightTExact t t') (X : C) (n : ℤ) [t.IsLE X n] : t'.IsLE (F.obj X) n

Transport coconnective membership from an explicit right t-exact functor.

Instantiate F with the actual tensor/projection operation at its geometry owner; the categorical layer does not pretend that an arbitrary functor is the tensor operation from Theorem 5.3(3).

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.leftTExact_isGE_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] {t : CategoryTheory.Triangulated.TStructure C} {t' : CategoryTheory.Triangulated.TStructure D} (F : CategoryTheory.Functor C D) (hF : F.IsLeftTExact t t') (X : C) (n : ℤ) [t.IsGE X n] : t'.IsGE (F.obj X) n

Transport connective membership from an explicit left t-exact functor.

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.tExact_isRange_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] {t : CategoryTheory.Triangulated.TStructure C} {t' : CategoryTheory.Triangulated.TStructure D} (F : CategoryTheory.Functor C D) (hF : F.IsTExact t t') (X : C) (a b : ℤ) [t.IsGE X a] [t.IsLE X b] : inRange t' (F.obj X) a b

Transport a bounded-range membership statement from a genuinely t-exact functor.

This is the shape for clauses whose source statement uses both halves; the one-sided clauses use rightTExact_isLE_map or leftTExact_isGE_map instead. Both conclusions are returned together so the two-sided hypothesis is used by the formal proof.

(5.3)/(5.4): local comparison owner boundary

theorem AlgebraicGeometry.DerivedCategory.Families.Theorem53.local_inRange_iff_of_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {t₁ t₂ : CategoryTheory.Triangulated.TStructure C} (isGE_iff : ∀ (X : C) (a : ℤ), t₁.IsGE X a ↔ t₂.IsGE X a) (isLE_iff : ∀ (X : C) (b : ℤ), t₁.IsLE X b ↔ t₂.IsLE X b) (X : C) (a b : ℤ) : inRange t₁ X a b ↔ inRange t₂ X a b

Compose separate lower- and upper-truncation comparison formulas.

The finite-amplitude, S-locality, and local pushforward arguments that produce the two formulas remain explicit at the geometry owner. In particular, the caller can instantiate the comparison formulas with the affine-local maps from (5.3)--(5.4), while this theorem performs only the formal conjunction composition.