Tensoring the exact sequence of a closed subscheme

For an ideal sheaf I and a finite locally free module sheaf E, tensoring the ideal sequence with E gives the short exact sequence

0 → E ⊗ I → E ⊗ 𝒪_X → E ⊗ i_*𝒪_{V(I)} → 0.

The target retains the scheme structure of the closed subscheme, including nilpotents. This sequence is used to prescribe restrictions of global sections, and in particular jets along nonreduced effective divisors. No finiteness or regularity of the closed subscheme is needed.

The exactness follows from dualizability: tensoring with a finite locally free sheaf is both a left and a right adjoint.

References

• R. Hartshorne, Algebraic Geometry, II, Section 5, and IV, Section 3.

theorem AlgebraicGeometry.Scheme.IdealSheafData.shortExact_tensor_toPushforwardSubscheme {X : Scheme} (I : X.IdealSheafData) (E : X.Modules) [SheafOfModules.IsLocallyFree E] [SheafOfModules.IsFiniteType E] : ({ X₁ := I.sheaf, X₂ := SheafOfModules.unit X.ringCatSheaf, X₃ := (Modules.pushforward I.subschemeι).obj (SheafOfModules.unit I.subscheme.ringCatSheaf), f := I.sheafι, g := SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι), zero := ⋯ }.map (CategoryTheory.MonoidalCategory.tensorLeft E)).ShortExact

Tensoring the ideal sequence of a closed subscheme with a finite locally free sheaf preserves short exactness.

theorem AlgebraicGeometry.Scheme.IdealSheafData.surjective_tensorRestriction_of_subsingleton_cohomology_one {X : Scheme} (I : X.IdealSheafData) (E : X.Modules) [SheafOfModules.IsLocallyFree E] [SheafOfModules.IsFiniteType E] (hvan : Subsingleton (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj E I.sheaf) 1)) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor E).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft E (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι)))) ⊤))

Sections of a finite locally free sheaf restrict surjectively to a closed subscheme if first cohomology of its tensor product with the ideal sheaf vanishes.