Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.BaseChangeTStructureRestriction

Conditional restriction of a target t-structure to bounded-coherent Dqc #

TargetBoundedTStructure supplies a t-structure on the target quasicoherent derived category and identifies its bounded locus with ambient cohomological boundedness. On a locally Noetherian target, finite presentation of cohomology is triangulated. Consequently, if nonpositive truncations of bounded-coherent objects retain finite-presentation cohomology, then the t-structure restricts to the intrinsic bounded-coherent full subcategory, and the restriction is bounded. The complementary truncation condition follows from the truncation triangle; it is not a second geometric premise.

Neither the supplied t-structure nor the finite-presentation preservation premise is constructed here. In particular, TargetBoundedTStructure is not identified with a paper-defined base-changed t-structure.

source
theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetBoundedTStructure.hasInducedBoundedCoherent {S : Scheme} {X T : SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left (X ⨯ T))] (τ : X.TargetBoundedTStructure T) (hfpLE : ∀ (E : X.TargetDqc T), Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) E → ∀ (n : ℤ), Dqc.schemeFinitePresentationCohomology (CategoryTheory.Over.left (X ⨯ T)) ((τ.tStructure.truncLE n).obj E)) :
(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T))).HasInducedTStructure τ.tStructure

One-sided finite-presentation preservation suffices for the target t-structure to induce a t-structure on bounded-coherent Dqc.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetBoundedTStructure.boundedCoherentTStructure {S : Scheme} {X T : SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left (X ⨯ T))] (τ : X.TargetBoundedTStructure T) (hfpLE : ∀ (E : X.TargetDqc T), Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) E → ∀ (n : ℤ), Dqc.schemeFinitePresentationCohomology (CategoryTheory.Over.left (X ⨯ T)) ((τ.tStructure.truncLE n).obj E)) :
CategoryTheory.Triangulated.TStructure (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T)))

The t-structure induced by τ on the intrinsic bounded-coherent Dqc category, conditional on finite-presentation preservation by truncation.

Equations
Instances For
    source
    theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetBoundedTStructure.boundedCoherentTStructureIsBounded {S : Scheme} {X T : SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left (X ⨯ T))] (τ : X.TargetBoundedTStructure T) (hfpLE : ∀ (E : X.TargetDqc T), Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) E → ∀ (n : ℤ), Dqc.schemeFinitePresentationCohomology (CategoryTheory.Over.left (X ⨯ T)) ((τ.tStructure.truncLE n).obj E)) :
    (τ.boundedCoherentTStructure hfpLE).IsBounded

    The induced bounded-coherent t-structure is bounded. This does not construct τ or prove the truncation-coherence premise.

    source
    theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetBoundedTStructure.boundedCoherentTStructureIsLE {S : Scheme} {X T : SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left (X ⨯ T))] (τ : X.TargetBoundedTStructure T) (hfpLE : ∀ (E : X.TargetDqc T), Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) E → ∀ (n : ℤ), Dqc.schemeFinitePresentationCohomology (CategoryTheory.Over.left (X ⨯ T)) ((τ.tStructure.truncLE n).obj E)) (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T))) (n : ℤ) :
    (τ.boundedCoherentTStructure hfpLE).IsLE E n ↔ τ.tStructure.IsLE E.obj n

    The nonpositive half of the named restriction is inherited from τ.

    source
    theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetBoundedTStructure.boundedCoherentTStructureIsGE {S : Scheme} {X T : SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left (X ⨯ T))] (τ : X.TargetBoundedTStructure T) (hfpLE : ∀ (E : X.TargetDqc T), Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) E → ∀ (n : ℤ), Dqc.schemeFinitePresentationCohomology (CategoryTheory.Over.left (X ⨯ T)) ((τ.tStructure.truncLE n).obj E)) (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T))) (n : ℤ) :
    (τ.boundedCoherentTStructure hfpLE).IsGE E n ↔ τ.tStructure.IsGE E.obj n

    The nonnegative half of the named restriction is inherited from τ.