S-local slicings over a family of base changes

The family-level S-local t-structure quantifier belongs to the Families layer. This file adds the phase-level analogue in the geometric stability layer, where the slicing and phase-truncation APIs are used. The target slicing, t-exactness, and phase comparison remain explicit owner data: this module does not manufacture geometric restriction or generation theorems from affineness.

structure CategoryTheory.Triangulated.Slicing.Restriction {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] (s : Slicing C) (F : Functor C D) : Type u₂

A slicing restriction along a functor.

The target slicing and its t-exactness are kept together. The phase compatibility field is stronger than preservation of semistability alone: it is the exact phase-level comparison needed by a local slicing, while the t-exactness field is the bridge to the t-structure API.

• slicing : Slicing D

  The slicing on the target category.

• isTExact : F.IsTExact (toTStructure C s) (toTStructure D self.slicing)

  The ambient functor is t-exact for the t-structures owned by the two slicings.

• phase_iff (φ : ℝ) (X : C) : self.slicing.P φ (F.obj X) ↔ s.P φ X

  The target phase slices are detected by the source phase slices.

theorem CategoryTheory.Triangulated.Slicing.Restriction.slicing_eq_of_phase_iff {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {s : Slicing C} {F : Functor C D} (r₁ r₂ : s.Restriction F) (h : ∀ (φ : ℝ) (Y : D), r₁.slicing.P φ Y ↔ r₂.slicing.P φ Y) : r₁.slicing = r₂.slicing

Equality of target slicings from equality of all phase predicates.

def CategoryTheory.Triangulated.Slicing.Restriction.toTStructureRestriction {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {s : Slicing C} {F : Functor C D} (r : s.Restriction F) : (toTStructure C s).Restriction F

The t-structure restriction carried by a slicing restriction.

Equations

• r.toTStructureRestriction = { tStructure := CategoryTheory.Triangulated.Slicing.toTStructure D r.slicing, isTExact := ⋯ }

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.SLocalSlicingData {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} (R : X.OpenRestrictionFamily P DS) (s : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)) : Type (u + 1)

S-local slicing: every quasi-compact open carries a slicing whose phase predicates and associated t-structure are compatible with restriction. The target slicings are chosen because downstream phase arguments need the actual owner data, not only a proposition that some slicing exists.

• restriction (U : S.Opens) (hU : CompactSpace ↥↑U) : s.Restriction (R.restriction U hU)

  The restricted slicing on each quasi-compact open of the base, as owner data. IsSLocalSlicing below is the propositional shadow of this field.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.IsSLocalSlicing {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} (R : X.OpenRestrictionFamily P DS) (s : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)) : Prop

Propositional shadow of SLocalSlicingData.

Equations

• R.IsSLocalSlicing s = ∀ (U : S.Opens) (hU : CompactSpace ↥↑U), Nonempty (s.Restriction (R.restriction U hU))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.SLocalSlicingData.isSLocal {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} {R : X.OpenRestrictionFamily P DS} {s : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)} (L : R.SLocalSlicingData s) : R.IsSLocalSlicing s

Chosen slicing restrictions witness the propositional S-local condition.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.SLocalSlicingData.toSLocalData {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} {R : X.OpenRestrictionFamily P DS} {s : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)} (L : R.SLocalSlicingData s) : R.SLocalData (CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s)

Forget the phase data to obtain the associated S-local t-structure.

Equations

• L.toSLocalData = { restriction := fun (U : S.Opens) (hU : CompactSpace ↥↑U) => (L.restriction U hU).toTStructureRestriction }

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.SLocalSlicingData.restriction_eq_of_phase_iff {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} {R : X.OpenRestrictionFamily P DS} {s : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)} (_L : R.SLocalSlicingData s) (U : S.Opens) (hU : CompactSpace ↥↑U) {r₁ r₂ : s.Restriction (R.restriction U hU)} (h : ∀ (φ : ℝ) (Y : (R.data U hU).QuasicoherentCategory P), r₁.slicing.P φ Y ↔ r₂.slicing.P φ Y) : r₁.slicing = r₂.slicing

Slicing restrictions agree once their complete phase predicates agree. The phase comparison is left explicit because image-generation of a target category is geometric, not a consequence of t-exactness alone.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.TwoDistinctAffineSLocalTStructures {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} (R : X.OpenRestrictionFamily P DS) (s₁ s₂ : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)) : Type (u + 1)

An affine-base package containing two distinct S-local t-structures.

Affineness alone does not create K-flat families or t-exactness. The two chosen slicing-locality witnesses and the distinctness proof are therefore explicit inputs to the adapter.

• affineBase : IsAffine S
• first : R.SLocalData (CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₁)

  S-local data for the t-structure underlying the first slicing.

• second : R.SLocalData (CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₂)

  S-local data for the t-structure underlying the second slicing.

• distinct : CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₁ ≠ CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₂

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.OpenRestrictionFamily.TwoDistinctAffineSLocalTStructures.ofSlicingData {S : Scheme} {X : SchemeBaseChange S} {P : CategoryTheory.ObjectProperty X.SourceDqc} [P.ContainsZero] {DS : X.KFlatBaseChangeData (identityBaseChange S)} {R : X.OpenRestrictionFamily P DS} (hAffine : IsAffine S) {s₁ s₂ : CategoryTheory.Triangulated.Slicing (DS.QuasicoherentCategory P)} (L₁ : R.SLocalSlicingData s₁) (L₂ : R.SLocalSlicingData s₂) (hne : CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₁ ≠ CategoryTheory.Triangulated.Slicing.toTStructure (DS.QuasicoherentCategory P) s₂) : R.TwoDistinctAffineSLocalTStructures s₁ s₂

Build the affine package from two actual slicing-locality witnesses.

Equations

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