Bounded-below affine Hom comparison #

For a bounded-below object with quasi-coherent cohomology on an affine scheme, maps from the structure sheaf are determined by the degree-zero truncation. This is a step toward an affine hypercohomology comparison.

Main definitions #

This file introduces no carrier, class, or instance.

Main results #

AlgebraicGeometry.Cohomology.affineHomToDegreeZeroTruncAddEquiv gives the additive Hom comparison under an explicit lower cohomological bound.
AlgebraicGeometry.Cohomology.affineHomH0SectionsAddEquiv identifies those maps with top sections of Mathlib's degree-zero homology object.

Implementation notes #

The generic t-structure comparison requires two negative Hom groups to vanish. Both vanish by the existing bounded affine theorem, applied to the negative truncation and its shift. The Dqc property is preserved by truncation and shift. The arbitrary-scheme sections comparison supplies the final step through the generic heart-to-homology isomorphism and unit-to-top-sections equivalence.

References #

AlgebraicGeometry.Cohomology.hom_unit_eq_zero_of_isGE_of_isLE_neg is the bounded affine vanishing input; Mathlib's t-structure truncation and shift laws supply the remaining bounds.

Tags #

affine scheme, quasi-coherent cohomology, derived category, hypercohomology

source

noncomputable def AlgebraicGeometry.Cohomology.affineHomToDegreeZeroTruncAddEquiv {R : CommRingCat} {M : DerivedCategory.SchemeDerivedCategory (Spec R)} (hM : DerivedCategory.Dqc.schemeQuasicoherentCohomology (Spec R) M) (a : ℤ) [DerivedCategory.TStructure.t.IsGE M a] :

((DerivedCategory.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ M) ≃+ ((DerivedCategory.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ (DerivedCategory.TStructure.t.truncGE 0).obj ((DerivedCategory.TStructure.t.truncLT 1).obj M))

On an affine scheme, bounded-below quasi-coherent cohomology makes the structure-sheaf Hom group insensitive to the negative part of the upper truncation. The target is the degree-zero heart object, without asserting a comparison to global sections or ambient derived global sections.

Equations

AlgebraicGeometry.Cohomology.affineHomToDegreeZeroTruncAddEquiv hM a = DerivedCategory.TStructure.t.homToDegreeZeroTruncAddEquiv ⋯ ⋯

Instances For

source

noncomputable def AlgebraicGeometry.Cohomology.affineHomH0SectionsAddEquiv {R : CommRingCat} {M : DerivedCategory.SchemeDerivedCategory (Spec R)} (hM : DerivedCategory.Dqc.schemeQuasicoherentCohomology (Spec R) M) (a : ℤ) [DerivedCategory.TStructure.t.IsGE M a] :

((DerivedCategory.singleFunctor (Spec R).Modules 0).obj (Scheme.Modules.unit (Spec R)) ⟶ M) ≃+ ↑(((DerivedCategory.homologyFunctor (Spec R).Modules 0).obj M).presheaf.obj (Opposite.op ⊤))

For a bounded-below Dqc object on an affine scheme, maps from the structure sheaf are additive-equivalent to top sections of its degree-zero homology sheaf. This is a pointwise comparison, without a derived-global- sections or naturality assertion.