The exact sequence of a closed subscheme

Let I ⊆ 𝒪_X be an ideal sheaf on a scheme X, cutting out the closed subscheme ι : V(I) ⟶ X. Restricting regular functions to V(I) is the morphism of 𝒪_X-modules 𝒪_X ⟶ ι_* 𝒪_{V(I)}, whose kernel is I by definition of the sections of I. It is an epimorphism because on every affine open U the restriction Γ(X, U) ⟶ Γ(V(I), U ∩ V(I)) is the quotient map by I(U). This gives the short exact sequence of 𝒪_X-modules

0 ⟶ I ⟶ 𝒪_X ⟶ ι_* 𝒪_{V(I)} ⟶ 0,

through which the cohomology of I is compared with the cohomology of 𝒪_X and of the closed subscheme V(I). Since ι is affine, ι_* 𝒪_{V(I)} is quasi-coherent, and hence so is the kernel I of a morphism between quasi-coherent sheaves.

Main declarations

• Scheme.IdealSheafData.shortExact_toPushforwardSubscheme: the sequence I ⟶ 𝒪_X ⟶ ι_* 𝒪_{V(I)} is short exact.
• Scheme.IdealSheafData.isQuasicoherent_sheaf: the ideal sheaf I is quasi-coherent.

References

• R. Hartshorne, Algebraic Geometry, Section II.5: the ideal sheaf 𝓘_Y of a closed subscheme Y is the kernel of 𝒪_X ⟶ i_* 𝒪_Y, which is surjective (Proposition II.5.9).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_eq_zero_iff {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} {s : ↑(X.presheaf.obj (Opposite.op U))} : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι)) U)) s = 0 ↔ s ∈ I.sections U

A section of 𝒪_X restricts to zero on V(I) exactly when it is a section of I, stated in the sections of ι_* 𝒪_{V(I)}, whose zero is not reducibly the zero of Γ(V(I), ι⁻¹ U).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_toPushforwardSubscheme {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.CategoryStruct.comp I.sheafι (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι)) = 0

Regular functions in I vanish on V(I).

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_toPushforwardSubscheme_assoc {X : Scheme} (I : X.IdealSheafData) {Z : X.Modules} (h : (Modules.pushforward I.subschemeι).obj (SheafOfModules.unit I.subscheme.ringCatSheaf) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp I.sheafι (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι))) h = CategoryTheory.CategoryStruct.comp 0 h

Regular functions in I vanish on V(I).

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.isLimitKernelForkSheafι {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι I.sheafι ⋯)

I is the kernel of the restriction 𝒪_X ⟶ ι_* 𝒪_{V(I)}.

instance AlgebraicGeometry.Scheme.IdealSheafData.epi_toPushforwardSubscheme {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.Epi (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom I.subschemeι))

The restriction 𝒪_X ⟶ ι_* 𝒪_{V(I)} is an epimorphism: on an affine open it is the quotient map Γ(X, U) ⟶ Γ(X, U) ⧸ I(U), and affine opens form a basis.

theorem AlgebraicGeometry.Scheme.IdealSheafData.shortExact_toPushforwardSubscheme {X : Scheme} (I : X.IdealSheafData) : { 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 := ⋯ }.ShortExact

The exact sequence of a closed subscheme 0 ⟶ I ⟶ 𝒪_X ⟶ ι_* 𝒪_{V(I)} ⟶ 0.

instance AlgebraicGeometry.Scheme.IdealSheafData.isQuasicoherent_sheaf {X : Scheme} (I : X.IdealSheafData) : SheafOfModules.IsQuasicoherent I.sheaf

An ideal sheaf is quasi-coherent: it is the kernel of the morphism 𝒪_X ⟶ ι_* 𝒪_{V(I)} between quasi-coherent sheaves, the target being quasi-coherent as ι is affine.