The bounded-coherent identification from the coherent Ext comparison

Dqc.lean states the identification Dᵇ(Coh X) ≌ Dᵇ_coh(Dqc X) as the explicit proposition BoundedCoherentDqcIdentification X, whose comparison field pins the equivalence to the concrete derived inclusion boundedCoherentDerivedToDqc X. This file reduces that proposition to a single statement about the abelian categories themselves:

CoherentExtComparison X: for coherent sheaves F G on X and every n, the map Ext^n_{Coh X}(F, G) → Ext^n_{X.Modules}(F, G) induced by Coh.ι X is a bijection.

Everything else is formal and is proved here, on any locally noetherian scheme:

• boundedCoherentDerivedToDqc_full_of_coherentExtComparison, boundedCoherentDerivedToDqc_faithful_of_coherentExtComparison: full faithfulness of the derived inclusion on Dᵇ(Coh X), by the amplitude dévissage Functor.mapDerivedCategory_map_bijective_of_bounded;
• boundedCoherentDerivedToDqc_essSurj_of_coherentExtComparison: essential surjectivity onto the intrinsic bounded-coherent locus, by the cone argument Functor.exists_bounded_iso_mapDerivedCategory_obj — the coherent approximation of quasi-coherent sheaves is not needed for this step;
• boundedCoherentDqcIdentificationOfCoherentExtComparison: the inhabitant of BoundedCoherentDqcIdentification X, with comparison := Iso.refl _.

What remains open

CoherentExtComparison X itself. Its target is Ext in all 𝒪_X-modules, not in quasi-coherent ones, and that is what makes it the genuine geometric content of the identification: the surjection-lifting criterion of Stacks 0FCL does not apply to Coh X ⊆ X.Modules (a coherent sheaf need not map onto a coherent quotient of an arbitrary module sheaf), so the classical route runs through D(QCoh X) ≌ D_qc(X) (Stacks 08DB) or the injectivity of quasi-coherent injectives in X.Modules (Hartshorne, Residues and Duality II.7.18). Neither is available at this Mathlib pin, and the affine case is not a shortcut: see the 2026-09-10 entry of docs/architecture/cutover-ledger.md.

Nothing here inhabits CoherentExtComparison; affine noetherian schemes satisfy it by Dqc/AffineIdentification.lean, through the Ext comparison from acyclic generators.

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

The coherent Ext comparison. The inclusion Coh.ι X : Coh X ⥤ X.Modules induces bijections Ext^n_{Coh X}(F, G) → Ext^n_{X.Modules}(F, G) for all coherent F, G and all n. This is the exact geometric content of the bounded-coherent identification; nothing in this file inhabits it.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.CoherentExtComparison X = ∀ (F G : AlgebraicGeometry.Coh X) (n : ℕ), Function.Bijective ⇑((AlgebraicGeometry.Coh.ι X).mapExtAddHom F G n)

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedInclusion_map_bijective {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) (E E' : SchemeBoundedCoherentDerivedCategory X) : Function.Bijective (DerivedCategory.Bounded.ι.comp (coherentDerivedInclusion X)).map

Under the Ext comparison, the derived inclusion Dᵇ(Coh X) ⥤ D(X.Modules) is bijective on every hom-set.

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedToDqc_full {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : (DerivedCategory.Bounded.ι.comp (coherentDerivedToDqc X)).Full

Under the Ext comparison, Dᵇ(Coh X) ⥤ Dqc(X) restricted to bounded objects is full.

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedToDqc_faithful {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : (DerivedCategory.Bounded.ι.comp (coherentDerivedToDqc X)).Faithful

Under the Ext comparison, Dᵇ(Coh X) ⥤ Dqc(X) restricted to bounded objects is faithful.

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedToDqc_full_of_coherentExtComparison {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : (boundedCoherentDerivedToDqc X).Full

Full faithfulness (#1070). Under the Ext comparison, the concrete functor Dᵇ(Coh X) ⥤ Dᵇ_coh(Dqc X) is full.

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedToDqc_faithful_of_coherentExtComparison {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : (boundedCoherentDerivedToDqc X).Faithful

Full faithfulness (#1070). Under the Ext comparison, the concrete functor Dᵇ(Coh X) ⥤ Dᵇ_coh(Dqc X) is faithful.

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedToDqc_essSurj_of_coherentExtComparison {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : (boundedCoherentDerivedToDqc X).EssSurj

Essential surjectivity (#1071). Under the Ext comparison, every object of the intrinsic bounded-coherent locus in Dqc(X) is isomorphic to the image of a bounded complex of coherent sheaves. The cohomology sheaves of such an object are coherent, so they lie in the essential image of Coh.ι X, and the generic cone argument applies.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDqcIdentificationOfCoherentExtComparison {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : BoundedCoherentDqcIdentification X

The bounded-coherent identification (#722), from the Ext comparison. The equivalence is boundedCoherentDerivedToDqc X itself, so the comparison field is the identity isomorphism: nothing but the concrete derived inclusion is used.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.hasBoundedCoherentDqcIdentification_of_coherentExtComparison {X : Scheme} [IsLocallyNoetherian X] (h : CoherentExtComparison X) : HasBoundedCoherentDqcIdentification X

The Ext comparison implies the explicit existence proposition consumed by Dqc/Comparison.lean.