An ideal sheaf on a locally Noetherian scheme is of finite presentation

The sheaf of modules I.toModules of an ideal sheaf I restricts, over a basic open D(r) of an affine open U, to the localization I(U)_r = I(D(r)) (Mathlib's IdealSheafData.map_ideal_basicOpen): Scheme.IdealSheafData.isLocalizedModule_toModules_resₗ. Its restriction to Spec Γ(X, U) is therefore the sheaf associated to I(U) (Mathlib's isIso_fromTildeΓ_iff_isLocalizing), and when X is locally Noetherian I(U) is finitely presented, so I.toModules is of finite presentation, hence quasi-coherent and of finite type (Scheme.IdealSheafData.isFinitePresentation_toModules).

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_toModulesSectionsEquiv_smul {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (c : ↑(X.presheaf.obj (Opposite.op ↑U))) (s : ↑(I.toModules.presheaf.obj (Opposite.op ↑U))) : ↑((I.toModulesSectionsEquiv U) (c • s)) = c * ↑((I.toModulesSectionsEquiv U) s)

theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocalizedModule_toModules_resₗ {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (r : ↑(X.presheaf.obj (Opposite.op ↑U))) : IsLocalizedModule (Submonoid.powers r) (I.toModules.resₗ ⋯)

Over a basic open D(r) of an affine open U, the sections of I.toModules are the localization of those over U: I(D(r)) = I(U)_r.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isIso_fromTildeΓ_toModules {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.IsIso (I.toModules.restrict hU.fromSpec).fromTildeΓ

Over an affine open U, the restriction of I.toModules to Spec Γ(X, U) is the sheaf associated to its global sections: the restrictions to the basic opens are localizations (isLocalizedModule_toModules_resₗ).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isFinitePresentation_toModules {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] : SheafOfModules.IsFinitePresentation I.toModules

An ideal sheaf on a locally Noetherian scheme is of finite presentation as a sheaf of modules: over each affine open U its restriction to Spec Γ(X, U) is the sheaf associated to I(U), a finitely presented module over the Noetherian ring Γ(X, U).