Quasi-coherent cohomology of termwise quasi-coherent complexes

The homology sheaves of a complex whose terms are quasi-coherent are quasi-coherent on any scheme. This gives a concrete source of objects in the honest Dqc locus of the derived category of all module sheaves.

Main definitions

This file introduces no new carrier, class, or instance.

Main results

• AlgebraicGeometry.DerivedCategory.Dqc.quasicoherentCohomology_of_termwiseQuasicoherent supplies the Dqc membership proof for an unbounded termwise quasi-coherent complex.

Implementation notes

The generic termwise theorem uses kernel and cokernel closure to obtain homology membership, then transports it through derived homology. The quasi-coherent object property supplies those closure instances here.

References

DerivedCategory.cohomologyIn_Q_obj_of_termwise is the generic proof; SheafOfModules.isQuasicoherent specializes its property argument.

Tags

scheme, quasi-coherent sheaves, derived category, homology

theorem AlgebraicGeometry.DerivedCategory.Dqc.quasicoherentCohomology_of_termwiseQuasicoherent (X : Scheme) (K : CochainComplex X.Modules ℤ) (hK : ∀ (n : ℤ), SheafOfModules.IsQuasicoherent (K.X n)) : schemeQuasicoherentCohomology X ((SchemeDerivedCategory.Q X).obj K)

Apply the generic termwise homology-closure theorem to the quasi-coherent object property on module sheaves.