The ideal sheaf as a sheaf of modules

Mathlib's Scheme.IdealSheafData records an ideal sheaf I ⊆ 𝒪_X through its ideals I(U) ⊆ Γ(X, U) on the affine opens U only. This file turns it into an 𝒪_X-submodule of the structure sheaf. Over an arbitrary open U, its sections are the regular functions on U that vanish on the closed subscheme V(I), that is, the kernel of the restriction Γ(X, U) ⟶ Γ(V(I), U ∩ V(I)) along the closed immersion I.subschemeι. Over an affine open this kernel is the ideal I(U) (Mathlib's Scheme.IdealSheafData.ker_subschemeι_app). Vanishing on V(I) is a local condition, so these ideals form a submodule of the sheaf 𝒪_X.

Main declarations

• Scheme.IdealSheafData.sections I U: the ideal of sections of I over an open U, with mem_sections_iff and sections_eq_ideal describing it on arbitrary and on affine opens;
• Scheme.IdealSheafData.submodule I: the submodule I ⊆ 𝒪_X of the sheaf of modules 𝒪_X;
• Scheme.IdealSheafData.sheaf I: the ideal sheaf as an 𝒪_X-module, with its inclusion Scheme.IdealSheafData.sheafι I : I ⟶ 𝒪_X, which is injective on sections (sheafι_app_injective) with image sections I U over U (range_sheafι_app), and Scheme.IdealSheafData.sectionMk building a section of I from an element of sections I U.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.9: the ideal sheaf of a closed subscheme is a quasi-coherent sheaf of ideals.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sections {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : Ideal ↑(X.presheaf.obj (Opposite.op U))

The sections over an open U of the ideal sheaf I: the regular functions on U vanishing on the closed subscheme cut out by I, i.e. the kernel of Γ(X, U) ⟶ Γ(V(I), U ∩ V(I)). Over an affine open U this is the ideal I.ideal U (sections_eq_ideal).

Equations

• I.sections U = RingHom.ker (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app I.subschemeι U))

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

A section lies in I exactly when it restricts to zero on the closed subscheme V(I).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sections_eq_ideal {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.sections ↑U = I.ideal U

Over an affine open, the sections of the ideal sheaf are the ideal it records there.

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_mem_sections {X : Scheme} (I : X.IdealSheafData) {U V : X.Opens} (i : V ⟶ U) {s : ↑(X.presheaf.obj (Opposite.op U))} (hs : s ∈ I.sections U) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) s ∈ I.sections V

Sections of the ideal sheaf restrict to sections of the ideal sheaf.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_sections_of_forall_exists {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} {s : ↑(X.presheaf.obj (Opposite.op U))} (hs : ∀ x ∈ U, ∃ (V : X.Opens) (i : V ⟶ U), x ∈ V ∧ (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) s ∈ I.sections V) : s ∈ I.sections U

Membership in the ideal sheaf is local: a section whose restrictions to the members of an open cover of U lie in I lies in I.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.submodule {X : Scheme} (I : X.IdealSheafData) : (SheafOfModules.unit X.ringCatSheaf).Submodule

The ideal sheaf I ⊆ 𝒪_X as a submodule of the sheaf of modules 𝒪_X.

Equations

• I.submodule = { obj := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) => I.sections (Opposite.unop U), map := ⋯, isSheaf := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.submodule_obj {X : Scheme} (I : X.IdealSheafData) (U : X.Opensᵒᵖ) : I.submodule.obj U = I.sections (Opposite.unop U)

The component of the submodule I ⊆ 𝒪_X at an open is sections I.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sheaf {X : Scheme} (I : X.IdealSheafData) : X.Modules

The ideal sheaf I ⊆ 𝒪_X as an 𝒪_X-module.

Equations

• I.sheaf = I.submodule.toSheafOfModules

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sheafι {X : Scheme} (I : X.IdealSheafData) : I.sheaf ⟶ SheafOfModules.unit X.ringCatSheaf

The inclusion I ⟶ 𝒪_X of the ideal sheaf into the structure sheaf.

Equations

• I.sheafι = I.submodule.ι

instance AlgebraicGeometry.Scheme.IdealSheafData.instMonoModulesSheafι {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.Mono I.sheafι

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sectionMk {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (hs : s ∈ I.sections U) : ↑(I.sheaf.presheaf.obj (Opposite.op U))

A regular function lying in sections I U, as a section of the ideal sheaf over U.

Equations

• I.sectionMk s hs = ⟨s, hs⟩

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_sectionMk {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (hs : s ∈ I.sections U) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) (I.sectionMk s hs) = s

Including a section built from a regular function recovers that function.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_map {X : Scheme} (I : X.IdealSheafData) {U V : X.Opens} (i : V ⟶ U) (t : ↑(I.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι V)) ((CategoryTheory.ConcreteCategory.hom (I.sheaf.presheaf.map i.op)) t) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) ((CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) t)

The inclusion I ⟶ 𝒪_X commutes with restriction to a smaller open.

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_mem {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) (t : ↑(I.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) t ∈ I.sections U

The inclusion I ⟶ 𝒪_X sends a section of the ideal sheaf over U into sections I U.

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_injective {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U))

The inclusion of the ideal sheaf into 𝒪_X is injective on sections.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_sheafι_app {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) = ↑(I.sections U)

The image of the sections of the ideal sheaf in Γ(X, U) is sections I U.