Ext from a line bundle as coherent cohomology

Tensoring by an explicitly invertible module sheaf is an exact autoequivalence. Its derived Ext adjunction, followed by the linear unit-Ext/cohomology comparison, identifies

Extⁿ_{X.Modules}(L, N) ≃ₗ[k] Hⁿ(X, L⁻¹ ⊗ N).

For a coherent N, invertible tensor preserves finite presentation, so the cohomology target is canonically an object of Coh X. This is entirely an ambient-module-sheaf theorem: it does not identify Ext in Coh X with Ext in X.Modules, and therefore does not discharge the separate CoherentExtComparison obligation.

Main result

• LineBundleData.extLineLinearEquivCoherentH is the base-field-linear comparison for a coherent target.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.extLineLinearEquivCoherentH {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (L : LineBundleData X) (N : X.Modules) (hN : IsCoherent X N) (n : ℕ) : CategoryTheory.Abelian.Ext L.line N n ≃ₗ[k] ↑((Cohomology.linearCoherentH k X n).obj { obj := L.inverse.tensorObj N, property := ⋯ })

Ext from a line bundle is the cohomology of the inverse twist.

The first equivalence replaces L by L ⊗ 𝒪_X, the second is derived Ext transport across the exact tensor autoequivalence, and the third is the linear unit-Ext/cohomology comparison.

Equations

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