Sections of degree-zero homology through the heart

For any scheme and any scheme-derived object, maps from the structure sheaf into its pure degree-zero truncation are the top sections of its actual Mathlib degree-zero homology sheaf. No affineness, quasicoherence or boundedness hypothesis is needed for this pointwise comparison.

Main definitions

This file introduces no carrier, class, or instance.

Main results

• AlgebraicGeometry.Cohomology.homTruncH0SectionsAddEquiv identifies the additive Hom group into the pure truncation with top sections of homology.

Implementation notes

The generic single-homology/pure-truncation isomorphism transports the target. Full faithfulness of the single functor then reduces the Hom group to sheaf morphisms, and the unit-to-top-sections equivalence evaluates those maps.

References

The generic comparison is in DerivedCategory.singleH0TruncIso; the sections map is AlgebraicGeometry.Scheme.Modules.unitHomTopLinearEquiv.

Tags

derived category, homology, global sections, scheme

noncomputable def AlgebraicGeometry.Cohomology.homTruncH0SectionsAddEquiv (X : Scheme) (M : DerivedCategory.SchemeDerivedCategory X) : ((DerivedCategory.singleFunctor X.Modules 0).obj (Scheme.Modules.unit X) ⟶ (DerivedCategory.TStructure.t.truncGE 0).obj ((DerivedCategory.TStructure.t.truncLT 1).obj M)) ≃+ ↑(((DerivedCategory.homologyFunctor X.Modules 0).obj M).presheaf.obj (Opposite.op ⊤))

Maps from the structure sheaf into the pure degree-zero truncation of an arbitrary scheme-derived object are additively equivalent to the top sections of its Mathlib degree-zero homology sheaf. This is pointwise and makes no ambient derived-global-sections or naturality assertion.

Equations

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