An ideal sheaf as a sheaf of modules #

Mathlib's ideal sheaves (X.IdealSheafData) are given by their ideals I(U) ⊆ Γ(X, U) over the affine opens U; Mathlib's sheaves of modules are X.Modules. The ideal sheaf I as a sheaf of 𝒪_X-modules is the subsheaf I.toModules of 𝒪_X whose sections over an open W are the functions whose restriction to every affine open U ⊆ W lies in I(U); over an affine open U these are exactly the elements of I(U) (Scheme.IdealSheafData.isLocallyMem_iff). The sheaf condition is the locality of membership in I(U): a function on an affine open U whose restrictions to the members of an open cover of U lie in the ideals of those members lies in I(U) (Scheme.IdealSheafData.mem_ideal_of_locally_mem), since I of a basic open D(g) of U is the localization of I(U) at g.

source

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_ideal_of_locally_mem {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (s : ↑(X.presheaf.obj (Opposite.op ↑U))) (h : ∀ x ∈ ↑U, ∃ (V : X.Opens), x ∈ V ∧ ∀ (U' : ↑X.affineOpens) (hU' : ↑U' ≤ ↑U), ↑U' ≤ V → (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hU').op)) s ∈ I.ideal U') :

s ∈ I.ideal U

Membership in I(U) is local: a function on an affine open U lies in I(U) if every point of U has an open neighbourhood V such that the restriction of the function to every affine open inside V ∩ U lies in the ideal of that open.

source

def AlgebraicGeometry.Scheme.IdealSheafData.IsLocallyMem {X : Scheme} (I : X.IdealSheafData) (W : X.Opens) (s : ↑(X.presheaf.obj (Opposite.op W))) :

Prop

The condition defining the sections of the ideal sheaf I over an open W: the restriction to every affine open U ⊆ W lies in I(U).

Equations

I.IsLocallyMem W s = ∀ (U : ↑X.affineOpens) (hU : ↑U ≤ W), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hU).op)) s ∈ I.ideal U

Instances For

source

theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocallyMem_map {X : Scheme} (I : X.IdealSheafData) {W W' : X.Opens} (h : W' ≤ W) {s : ↑(X.presheaf.obj (Opposite.op W))} (hs : I.IsLocallyMem W s) :

I.IsLocallyMem W' ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) s)

source

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

(SheafOfModules.unit X.ringCatSheaf).val.Submodule

The submodules of sections of the ideal sheaf I inside 𝒪_X: over an open W, the functions whose restriction to every affine open U ⊆ W lies in I(U).

Equations

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

Instances For

source

theorem AlgebraicGeometry.Scheme.IdealSheafData.isSheaf_toSubmodule {X : Scheme} (I : X.IdealSheafData) :

CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥X) I.toSubmodule.toPresheafOfModules.presheaf

The sheaf condition of toSubmodule, from the locality of membership in I(U) (mem_ideal_of_locally_mem).

source

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

X.Modules

The ideal sheaf I as a sheaf of 𝒪_X-modules: the subsheaf of 𝒪_X of the functions whose restriction to every affine open U lies in I(U).

Equations