The quasi-coherent cohomology locus in a scheme-derived category

The ambient SchemeDerivedCategory X is the derived category of all 𝒪_X-module sheaves. The category conventionally denoted Dqc(X) is the full subcategory whose cohomology sheaves are quasi-coherent. This file makes that distinction part of the Lean type.

Dqc(X) is a triangulated subcategory, and this file proves it rather than assuming it (#721). The route does not need quasi-coherent sheaves to be an abelian subcategory of X.Modules — an earlier version of this docstring named that as the blocker. What is needed is only the weak Serre property: closure under kernels, cokernels and extensions, which Modules/Quasicoherent/Kernels.lean and Cohomology/Quasicoherent/Extensions.lean supply on an arbitrary scheme (#720). DerivedCategory.cohomologyIn turns that into closure under cones via the five-term long exact homology sequence, so Pretriangulated on the locus and triangulatedness of the inclusion both follow from Mathlib.

Comparison statements a later geometric realization must still prove — the bounded-coherent identification and the compact/perfect comparison — remain propositions with no unsupported inhabitant. Dqc/Comparison.lean turns them into representatives and membership theorems only when a consumer passes the evidence explicitly, so unsupported geometric cases are still not silently identified with the all-sheaf derived category.

The canonical zero object is different: it follows from the triangulated full subcategory structure already proved here, so this root constructs it for an arbitrary scheme. Moduli consumers reuse that object and add their own locus membership proofs.

Declarations in this file and the affine realization subtree use the geometry-owned namespace AlgebraicGeometry.DerivedCategory.Dqc.

def AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology (X : Scheme) : CategoryTheory.ObjectProperty (SchemeDerivedCategory X)

An object of the all-module-sheaf derived category has quasi-coherent cohomology when every one of its canonical cohomology sheaves is quasi-coherent.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology X E = ∀ (n : ℤ), SheafOfModules.isQuasicoherent X.ringCatSheaf ((DerivedCategory.homologyFunctor X.Modules n).obj E)

instance AlgebraicGeometry.DerivedCategory.Dqc.instIsClosedUnderIsomorphismsSchemeDerivedCategorySchemeQuasicoherentCohomology (X : Scheme) : (schemeQuasicoherentCohomology X).IsClosedUnderIsomorphisms

instance AlgebraicGeometry.DerivedCategory.Dqc.instIsTriangulatedSchemeDerivedCategorySchemeQuasicoherentCohomology (X : Scheme) : (schemeQuasicoherentCohomology X).IsTriangulated

Dqc(X) is a triangulated subcategory of the all-sheaf derived category (#721).

Quasi-coherence is a weak Serre subcategory of X.Modules — closed under kernels, cokernels and extensions, and containing zero — on an arbitrary scheme, with no noetherian or quasi-compactness hypothesis. That is exactly the input DerivedCategory.cohomologyIn_isTriangulated asks for, and it is why closure under cones holds without quasi-coherent sheaves forming an abelian subcategory: the five-term homology sequence pays for the missing subobject and quotient closure.

Note that quasi-coherence is not a Serre class here — a subsheaf of a quasi-coherent sheaf need not be quasi-coherent — so IsSerreClass and Mathlib's three-term prop_X₂_of_exact are unavailable, and nothing below uses them.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory (X : Scheme) : Type (u + 1)

The honest Dqc(X) object class: the full subcategory of the derived category of all module sheaves cut out by quasi-coherent cohomology.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology X).FullSubcategory

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.ι (X : Scheme) : CategoryTheory.Functor (SchemeQuasicoherentDerivedCategory X) (SchemeDerivedCategory X)

The inclusion of the quasi-coherent cohomology locus into the derived category of all module sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.ι X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology X).ι

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.ι_isTriangulated (X : Scheme) : (ι X).IsTriangulated

The inclusion Dqc(X) ⥤ D(X.Modules) is a triangulated functor. This is a Mathlib instance once the object property is a triangulated subcategory; it is recorded here because it is what Dqc(X) has to have for "compact object in Dqc(X)" to be a statement one may make. (Pretriangulated is data, not a proposition, so it is left as the Mathlib instance rather than restated here.)

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero (X : Scheme) : SchemeQuasicoherentDerivedCategory X

The canonical zero object of Dqc(X), owned by the Dqc root rather than by any particular geometric consumer.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X = 0

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero_isZero (X : Scheme) : CategoryTheory.Limits.IsZero (zero X)

The canonical Dqc(X) zero is a zero object in the full subcategory.

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero_obj_isZero (X : Scheme) : CategoryTheory.Limits.IsZero (zero X).obj

Forgetting the canonical Dqc(X) zero to the all-sheaf derived category still gives a zero object.

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.quasicoherent_isClosedUnderIsomorphisms (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderIsomorphisms

The abelian-side inputs to Dqc(X)'s coproduct structure (#721, third bullet).

Quasi-coherence is closed under ι-indexed coproducts on an arbitrary scheme (Modules/Quasicoherent/Coproducts.lean), and X.Modules has those coproducts. Closure under isomorphism is Mathlib's and is recorded alongside it. The derived-category half, that SchemeDerivedCategory X has coproducts and every Hⁿ preserves them, is DerivedCategory.hasCoproductsOfShape and DerivedCategory.homologyFunctor_preservesCoproductsOfShape at X.Modules, whose coproducts are exact (Scheme.Modules.hasExactColimitsOfShape).

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.quasicoherent_isClosedUnderCoproducts (X : Scheme) (ι : Type u) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.sigma_mem (X : Scheme) {ι : Type u} (E : ι → SchemeDerivedCategory X) (hE : ∀ (i : ι), schemeQuasicoherentCohomology X (E i)) : schemeQuasicoherentCohomology X (∐ E)

Dqc(X) is closed under coproducts (#721, third bullet, closure clause).

SchemeDerivedCategory X has coproducts indexed by any type in the universe of X, and every Hⁿ preserves them, because coproducts in X.Modules are exact; both are found by instance search, so closure needs no hypothesis beyond membership of the summands.

One piece of plumbing here is deliberate and cost real time to find. The @ and the named quasicoherent_isClosedUnderCoproducts are needed because Instance search cannot find that instance through this application even though quasicoherent_isClosedUnderCoproducts two declarations above finds it by inferInstance: unifying A := X.Modules routes the category through Scheme.Modules.instCategory, and the goal it then poses no longer matches the instance's own head. Supplying it by name is not a workaround for an unproved fact — it is the same instance, named.

instance AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.isClosedUnderColimitsOfShape_discrete (X : Scheme) (ι : Type u) : (schemeQuasicoherentCohomology X).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)

Dqc(X) is closed under coproducts as an object property, so Mathlib gives SchemeQuasicoherentDerivedCategory X its coproducts and makes ι create them.

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.ι_preservesCoproductsOfShape (X : Scheme) (ι : Type u) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) (SchemeQuasicoherentDerivedCategory.ι X)

The inclusion Dqc(X) ⥤ D(X.Modules) preserves coproducts (#721, third bullet, second clause). A Mathlib instance once the object property is closed under them; recorded here, as ι_isTriangulated is, because it is the acceptance criterion of #721.

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.ι_reflectsCoproductsOfShape (X : Scheme) (ι : Type u) : CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete ι) (SchemeQuasicoherentDerivedCategory.ι X)

The inclusion Dqc(X) ⥤ D(X.Modules) reflects coproducts, which is what a realization functor into the locus needs and which preservation alone does not give.

Preservation says the image of a coproduct is a coproduct, and that is the statement a consumer of Dqc(X) wants. A functor landing in Dqc(X) needs the converse direction: knowing that its composite with ι preserves coproducts, conclude that it does. Reflection is exactly that step, and it holds here because the closure above makes ι create these colimits — the coproduct of a family in Dqc(X) is their coproduct in the all-sheaf derived category, carrying its membership proof. Creation carries data rather than being a proposition, so it stays a local term inside this proof; reflection is the proposition it implies.

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.mem_iff (X : Scheme) (E : SchemeDerivedCategory X) : schemeQuasicoherentCohomology X E ↔ ∀ (n : ℤ), SheafOfModules.isQuasicoherent X.ringCatSheaf ((DerivedCategory.homologyFunctor X.Modules n).obj E)

Membership in Dqc(X) is exactly quasi-coherence of every cohomology sheaf.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.coherentDerivedInclusion (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemeCoherentDerivedCategory X) (SchemeDerivedCategory X)

The exact inclusion of coherent sheaves induces a concrete functor from their unbounded derived category to the all-module-sheaf derived category.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.coherentDerivedInclusion X = (AlgebraicGeometry.Coh.ι X).mapDerivedCategory

theorem AlgebraicGeometry.DerivedCategory.Dqc.coherentDerivedInclusion_mem_dqc (X : Scheme) [IsLocallyNoetherian X] (E : SchemeCoherentDerivedCategory X) : schemeQuasicoherentCohomology X ((coherentDerivedInclusion X).obj E)

The derived coherent-sheaf inclusion has quasi-coherent cohomology in every degree. This is proved by exactness of Coh.ι, not postulated as a geometric realization.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.coherentDerivedToDqc (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemeCoherentDerivedCategory X) (SchemeQuasicoherentDerivedCategory X)

The genuine lift of the coherent derived category into the quasi-coherent-cohomology locus.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.coherentDerivedToDqcCompInclusion (X : Scheme) [IsLocallyNoetherian X] : (coherentDerivedToDqc X).comp (SchemeQuasicoherentDerivedCategory.ι X) ≅ coherentDerivedInclusion X

Forgetting the quasi-coherent-cohomology proof recovers the derived coherent-sheaf inclusion definitionally.

Equations

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

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

Bounded objects in the honest Dqc(X) locus are detected by the canonical t-structure of the ambient all-sheaf derived category.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedQuasicoherent X E = DerivedCategory.TStructure.t.bounded E.obj

instance AlgebraicGeometry.DerivedCategory.Dqc.instIsClosedUnderIsomorphismsSchemeQuasicoherentDerivedCategorySchemeBoundedQuasicoherent (X : Scheme) : (schemeBoundedQuasicoherent X).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedQuasicoherentDerivedCategory (X : Scheme) : Type (u + 1)

The bounded part of Dqc(X), defined by ambient cohomological boundedness.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedQuasicoherentDerivedCategory X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedQuasicoherent X).FullSubcategory

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedQuasicoherentDerivedCategory.ι (X : Scheme) : CategoryTheory.Functor (SchemeBoundedQuasicoherentDerivedCategory X) (SchemeQuasicoherentDerivedCategory X)

The inclusion of bounded quasi-coherent complexes into Dqc(X).

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedQuasicoherentDerivedCategory.ι X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedQuasicoherent X).ι

theorem AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedQuasicoherentDerivedCategory.mem_iff (X : Scheme) (E : SchemeQuasicoherentDerivedCategory X) : schemeBoundedQuasicoherent X E ↔ DerivedCategory.TStructure.t.bounded E.obj

Boundedness is detected after the two honest inclusions into the ambient derived category.

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

The intrinsic bounded-coherent locus in Dqc(X): ambient boundedness and finite presentation of every cohomology sheaf. On a locally Noetherian scheme this is the expected objectwise description of Dᵇ(Coh X).

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.instIsClosedUnderIsomorphismsSchemeQuasicoherentDerivedCategorySchemeBoundedCoherentCohomology (X : Scheme) : (schemeBoundedCoherentCohomology X).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedCoherentDqcCategory (X : Scheme) : Type (u + 1)

The full subcategory of Dqc(X) with bounded coherent cohomology.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedCoherentDqcCategory X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology X).FullSubcategory

theorem AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology_le_bounded (X : Scheme) : schemeBoundedCoherentCohomology X ≤ schemeBoundedQuasicoherent X

Bounded coherent cohomology implies ambient boundedness.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedToDqc (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemeBoundedCoherentDerivedCategory X) (SchemeBoundedCoherentDqcCategory X)

The bounded coherent category maps concretely into the intrinsic bounded-coherent locus in Dqc(X).

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedCoherentDqcCategory.ι (X : Scheme) : CategoryTheory.Functor (SchemeBoundedCoherentDqcCategory X) (SchemeQuasicoherentDerivedCategory X)

Forget bounded-coherent cohomology to the ambient Dqc(X) locus.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedCoherentDqcCategory.ι X = (AlgebraicGeometry.DerivedCategory.Dqc.schemeBoundedCoherentCohomology X).ι

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.perfectDerivedToDqc (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemePerfectDerivedCategory X) (SchemeBoundedCoherentDqcCategory X)

The perfect thick envelope maps through bounded coherent complexes into the bounded coherent Dqc locus.

Equations

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

def AlgebraicGeometry.DerivedCategory.Dqc.schemePerfectInDqc (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.ObjectProperty (SchemeQuasicoherentDerivedCategory X)

Perfect objects inside Dqc(X), defined without circular use of compactness as the essential image of the repository's finite-locally-free thick envelope.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.perfectDerivedToDqc_obj_mem_schemePerfectInDqc (X : Scheme) [IsLocallyNoetherian X] (E : SchemePerfectDerivedCategory X) : schemePerfectInDqc X ((SchemeBoundedCoherentDqcCategory.ι X).obj ((perfectDerivedToDqc X).obj E))

Every object of the coherent-derived perfect category maps into the perfect essential image in Dqc(X). This is the canonical absolute-perfect comparison and requires no bounded-coherent equivalence hypothesis.

structure AlgebraicGeometry.DerivedCategory.Dqc.BoundedCoherentDqcIdentification (X : Scheme) [IsLocallyNoetherian X] : Type (u + 1)

The exact missing general-scheme identification behind the standard notation Dᵇ(Coh X) ⊂ Dqc(X). The comparison field forces the equivalence to be the concrete derived inclusion constructed above. No unsupported scheme is marked as satisfying this proposition.

• equivalence : SchemeBoundedCoherentDerivedCategory X ≌ SchemeBoundedCoherentDqcCategory X

  The bounded coherent derived category is equivalent to the intrinsic bounded coherent cohomology locus.

• comparison : self.equivalence.functor ≅ boundedCoherentDerivedToDqc X

  The equivalence is the concrete exact derived inclusion.

def AlgebraicGeometry.DerivedCategory.Dqc.HasBoundedCoherentDqcIdentification (X : Scheme) [IsLocallyNoetherian X] : Prop

Existence of the general-scheme bounded-coherent identification, kept as an explicit proposition rather than a typeclass instance.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.HasBoundedCoherentDqcIdentification X = Nonempty (AlgebraicGeometry.DerivedCategory.Dqc.BoundedCoherentDqcIdentification X)

def AlgebraicGeometry.DerivedCategory.Dqc.PerfectObjectsAreCompactInDqc (X : Scheme) [IsLocallyNoetherian X] : Prop

The exact compact/perfect comparison still required by the scheme-level A.14 realization. This file supplies no unsupported inhabitant; Dqc(X) now has its coproducts, and what remains is compact generation by perfect complexes (RΓ commuting with coproducts), a separate obligation.

This is not Neeman's compact-equals-perfect theorem, and IsLocallyNoetherian is not enough to inhabit it. Two gaps, both about the left-hand side. Neeman's theorem identifies the compact objects of Dqc(X) with the perfect complexes, those locally quasi-isomorphic to a bounded complex of finite locally free sheaves, for X quasi-compact and separated. The left side here is schemePerfectInDqc, the essential image of the absolute thick envelope of finite locally free sheaves (schemePerfect, DerivedCategory/Coherent.lean), and that envelope is all of Perf(X) only when X has the resolution property. So an inhabitant must carry quasi-compactness, separatedness, and the resolution property; none of the three is in this signature, and the repository has no vocabulary for the third. The .{0} is a third narrowing: it tests compactness against Type-indexed coproducts only.

Left at this generality on purpose — it names the comparison the realization needs without inventing a resolution-property class before a consumer exists for one. Do not cite it as the literature's theorem, and do not inhabit it without first adding the hypotheses.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.PerfectObjectsAreCompactInDqc X = (AlgebraicGeometry.DerivedCategory.Dqc.schemePerfectInDqc X = CategoryTheory.ObjectProperty.compactObjects)