Consuming the bounded-coherent and compact/perfect comparison hypotheses

Dqc.lean records two geometric identifications that are not available for an arbitrary scheme at the current Mathlib pin:

• Dᵇ(Coh X) with the bounded coherent-cohomology locus in Dqc(X);
• the perfect thick envelope with the compact objects of Dqc(X).

Those statements remain explicit propositions with no global inhabitants. This file is their consumer API: after a caller supplies the relevant evidence, it extracts a coherent representative and exposes the corresponding perfect/compact membership theorem. No instance is installed, so unsupported schemes cannot acquire either identification through typeclass search.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDqcIdentification (X : Scheme) [IsLocallyNoetherian X] (h : HasBoundedCoherentDqcIdentification X) : BoundedCoherentDqcIdentification X

Chosen bounded-coherent comparison data, extracted only from explicit evidence that the comparison exists.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDqcIdentification X h = Classical.choice h

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDerivedToDqc_essSurj (X : Scheme) [IsLocallyNoetherian X] (h : HasBoundedCoherentDqcIdentification X) : (boundedCoherentDerivedToDqc X).EssSurj

The concrete functor Dᵇ(Coh X) ⥤ Dᵇ_coh(Dqc X) is essentially surjective once the bounded-coherent identification is supplied.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentRepresentative (X : Scheme) [IsLocallyNoetherian X] (h : HasBoundedCoherentDqcIdentification X) (E : SchemeBoundedCoherentDqcCategory X) : SchemeBoundedCoherentDerivedCategory X

A chosen Dᵇ(Coh X) representative of a bounded coherent object of Dqc(X), conditional on the explicit comparison evidence.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentRepresentative X h E = (AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentDqcIdentification X h).equivalence.inverse.obj E

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentRepresentativeIso (X : Scheme) [IsLocallyNoetherian X] (h : HasBoundedCoherentDqcIdentification X) (E : SchemeBoundedCoherentDqcCategory X) : (boundedCoherentDerivedToDqc X).obj (boundedCoherentRepresentative X h E) ≅ E

The image of the chosen coherent representative is the original bounded coherent Dqc(X) object.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.schemePerfectInDqc_iff_isCompact (X : Scheme) [IsLocallyNoetherian X] (h : PerfectObjectsAreCompactInDqc X) (E : SchemeQuasicoherentDerivedCategory X) : schemePerfectInDqc X E ↔ CategoryTheory.IsCompactObject E

Under the explicit compact/perfect comparison, membership in the repository's perfect locus is exactly compactness in Dqc(X).