Splitting the intrinsic bounded-coherent locus

Dqc.schemeBoundedCoherentCohomology X is a conjunction: ambient boundedness of the underlying complex, and finite presentation of every cohomology sheaf. Dqc.lean writes both conjuncts into one definition. This file names the second on its own and records the resulting decomposition.

The split is worth making because the two halves are preserved for different reasons. Boundedness of F.obj E follows formally from a cohomological amplitude bound on F, with no finiteness hypothesis anywhere; finite presentation of the cohomology sheaves of F.obj E follows from no amplitude bound at all and is a genuine geometric input. Naming the conjuncts separately lets a consumer discharge the first and assume only the second.

When finite-presentation module sheaves are closed under kernels and cokernels, they form a weak Serre class; a locally Noetherian scheme supplies these two closure conditions. Both halves then cut out triangulated subcategories of Dqc(X), as does their intersection. This gives the intrinsic bounded-coherent locus the triangulated structure needed to restrict later base-change constructions; it does not construct a base-changed t-structure.

def AlgebraicGeometry.DerivedCategory.Dqc.schemeFinitePresentationCohomology (X : Scheme) : CategoryTheory.ObjectProperty (SchemeQuasicoherentDerivedCategory X)

Finite presentation of every cohomology sheaf of an object of Dqc(X). This is the coherence half of schemeBoundedCoherentCohomology; on its own it asserts nothing about boundedness.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology_iff (X : Scheme) (E : SchemeQuasicoherentDerivedCategory X) : schemeBoundedCoherentCohomology X E ↔ schemeBoundedQuasicoherent X E ∧ schemeFinitePresentationCohomology X E

Membership in the intrinsic bounded-coherent locus is ambient boundedness together with finite presentation of every cohomology sheaf.

theorem AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology_eq_inf (X : Scheme) : schemeBoundedCoherentCohomology X = schemeBoundedQuasicoherent X ⊓ schemeFinitePresentationCohomology X

The intrinsic bounded-coherent locus is the meet of its two conjuncts.

theorem AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology_le_finitePresentationCohomology (X : Scheme) : schemeBoundedCoherentCohomology X ≤ schemeFinitePresentationCohomology X

Bounded coherent cohomology implies coherence of every cohomology sheaf.

instance AlgebraicGeometry.DerivedCategory.Dqc.instIsClosedUnderIsomorphismsSchemeQuasicoherentDerivedCategorySchemeFinitePresentationCohomology (X : Scheme) : (schemeFinitePresentationCohomology X).IsClosedUnderIsomorphisms

instance AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedQuasicoherent_isTriangulated (X : Scheme) : (schemeBoundedQuasicoherent X).IsTriangulated

Ambient cohomological boundedness is triangulated after restriction to Dqc(X), without a Noetherian hypothesis.

instance AlgebraicGeometry.DerivedCategory.Dqc.schemeFinitePresentationCohomology_isTriangulated (X : Scheme) [X.coherent.IsClosedUnderKernels] [X.coherent.IsClosedUnderCokernels] : (schemeFinitePresentationCohomology X).IsTriangulated

Kernel and cokernel closure of coherent module sheaves complete their unconditional weak-Serre properties, so coherent cohomology is triangulated on Dqc(X). Locally Noetherian schemes supply these two hypotheses.

instance AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology_isTriangulated (X : Scheme) [(schemeFinitePresentationCohomology X).IsTriangulated] : (schemeBoundedCoherentCohomology X).IsTriangulated

The intrinsic bounded-coherent locus is triangulated whenever the coherent-cohomology half is triangulated, in particular on a locally Noetherian scheme. This is a prerequisite for restricting a t-structure to that locus, not a proof that its truncations preserve coherent cohomology.