Vanishing of maps from a single object into D^{≤ -1} #
Let E : A and let P be a class of objects of A such that Ext^k(E, Y) = 0 for every
k ≥ 1 and every Y in P. Then there is no nonzero map from (singleFunctor A 0).obj E
into a bounded object of D^{≤ -1} whose cohomology objects lie in P. This is the
statement that the hypercohomology Hom(E, M[j]) of such an M is computed by
Hom(E, H^j M) alone, in the only case where the answer is zero; the proof is dévissage on
the amplitude along the truncation triangles.
The geometric instance is 𝒪_X on an affine scheme with P quasi-coherence, where the
hypothesis is affine vanishing through Ext^k(𝒪_X, F) ≃ H^k(F). That instance is the
bounded half of the compactness of 𝒪_X in Dqc(Spec R) (#723); the unbounded half needs
M ≅ holim τ≥-n M, which is not available at this Mathlib pin.
Main results #
DerivedCategory.hom_singleFunctor_eq_zero_of_ext_subsingleton— the single case.DerivedCategory.hom_eq_zero_of_isGE_of_isLE_neg_of_cohomologyIn— the dévissage.
No maps from single 0 E into single a Y for a < 0 and Y in P: such a map is a
class in Ext^{-a}(E, Y).
Dévissage. No maps from single 0 E into a bounded object of D^{≤ -1} whose
cohomology lies in P. Induction on the amplitude along the truncation triangles
τ_{< b} M → M → τ_{≥ b} M; the first term is concentrated in one degree and the third has
smaller amplitude.