Finite presentation of modules and their associated sheaves

An R-module is finitely presented if and only if its associated sheaf on Spec R is finitely presented. More generally, the sections of a finitely presented sheaf over any affine open are a finitely presented module over its ring of functions. On an affine scheme, the sheaf admits a global presentation with finitely many generators and relations.

The forward implication uses Mathlib's presentationTilde, whose generating and relation families are precisely those of the module presentation. For the converse, finite local sheaf presentations can be refined to basic opens. A finite global presentation on an affine scheme gives a finite module presentation, and Mathlib's localization descent glues these finite presentations of modules. The analogous finite-type comparison supplies ambient cokernel closure for maps from quasicoherent sheaves of finite type to finitely presented sheaves. Over a Noetherian ring, ambient kernels of maps from quasicoherent sheaves of finite type to quasicoherent sheaves are also finitely presented. This supplies the affine algebraic description of coherent sheaves on locally Noetherian schemes without imposing a Noetherian hypothesis on the affine result.

The module-cokernel construction follows Mathlib's AlgebraicGeometry.isIso_fromTildeΓ_of_presentation, using the fully faithful tilde functor and its preservation of cokernels.

References

• The Stacks Project, Properties of Schemes, Section 28.17 (Tag 01PA), Lemma 28.17.2 (Tag 01PC).

instance TauCeti.AlgebraicGeometry.isFinite_presentationTilde {R : CommRingCat} (M : ModuleCat ↑R) (s : Set ↑M) (hs : Submodule.span (↑R) s = ⊤) (t : Set (↑s →₀ ↑R)) (ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker) [Finite ↑s] [Finite ↑t] : (AlgebraicGeometry.presentationTilde M s hs t ht).IsFinite

Finite generating and relation sets give a finite presentation of the associated sheaf.

instance TauCeti.AlgebraicGeometry.isFinitePresentation_tilde {R : CommRingCat} (M : ModuleCat ↑R) [Module.FinitePresentation ↑R ↑M] : SheafOfModules.IsFinitePresentation (AlgebraicGeometry.tilde M)

The sheaf associated with a finitely presented module is finitely presented.

theorem AlgebraicGeometry.Scheme.Modules.finitePresentation_moduleSpecΓ_of_presentation {R : CommRingCat} (M : (Spec R).Modules) (P : SheafOfModules.Presentation M) [P.IsFinite] : Module.FinitePresentation ↑R ↑(moduleSpecΓFunctor.obj M)

A finite global presentation on Spec R gives a finitely presented module of global sections over R.

theorem AlgebraicGeometry.Scheme.Modules.finitePresentation_sections_of_presentation {X : Scheme} (M : X.Modules) (U : X.Opens) (hU : IsAffineOpen U) (P : (SheafOfModules.over M U).Presentation) [P.IsFinite] : Module.FinitePresentation ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))

A finite presentation on the slice site of an affine open gives a finitely presented module of sections over that open.

theorem AlgebraicGeometry.Scheme.Modules.finitePresentation_sections_of_isAffineOpen {X : Scheme} (M : X.Modules) [SheafOfModules.IsFinitePresentation M] (U : X.Opens) (hU : IsAffineOpen U) : Module.FinitePresentation ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))

The sections of a finitely presented sheaf over an affine open form a finitely presented module over the ring of functions on that open.

theorem AlgebraicGeometry.Scheme.Modules.finitePresentation_globalSections_of_isAffine {X : Scheme} [IsAffine X] (M : X.Modules) [SheafOfModules.IsFinitePresentation M] : Module.FinitePresentation ↑(X.presheaf.obj (Opposite.op ⊤)) ↑(M.presheaf.obj (Opposite.op ⊤))

The global sections of a finitely presented sheaf on an affine scheme form a finitely presented module over its ring of global functions.

theorem AlgebraicGeometry.Scheme.Modules.finitePresentation_moduleSpecΓ {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsFinitePresentation M] : Module.FinitePresentation ↑R ↑(moduleSpecΓFunctor.obj M)

A finitely presented sheaf on Spec R has finitely presented global sections as an R-module.

@[simp]

theorem ModuleCat.isFinitePresentation_tilde_iff {R : CommRingCat} (M : ModuleCat ↑R) : SheafOfModules.IsFinitePresentation (AlgebraicGeometry.tilde M) ↔ Module.FinitePresentation ↑R ↑M

A module is finitely presented if and only if its associated sheaf on the spectrum is finitely presented.

theorem AlgebraicGeometry.Scheme.Modules.exists_isFinite_presentation_of_isAffine {X : Scheme} [IsAffine X] (M : X.Modules) [SheafOfModules.IsFinitePresentation M] : ∃ (P : SheafOfModules.Presentation M), P.IsFinite

A finitely presented sheaf on an affine scheme admits a global presentation with finitely many generators and finitely many relations.

theorem AlgebraicGeometry.Scheme.Modules.finite_moduleSpecΓ_of_generatingSections {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] (G : SheafOfModules.GeneratingSections M) [G.IsFiniteType] : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)

Finite global generators of a quasicoherent sheaf on Spec R give finite global sections.

theorem AlgebraicGeometry.Scheme.Modules.finite_sections_of_generatingSections {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (U : X.Opens) (hU : IsAffineOpen U) (G : (SheafOfModules.over M U).GeneratingSections) [G.IsFiniteType] : Module.Finite ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))

Finite generators over an affine open give a finite module of sections for a quasicoherent sheaf.

theorem AlgebraicGeometry.Scheme.Modules.finite_sections_of_isAffineOpen {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsFiniteType M] (U : X.Opens) (hU : IsAffineOpen U) : Module.Finite ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))

The sections of a quasicoherent sheaf of finite type over an affine open form a finite module over the ring of functions on that open.

theorem AlgebraicGeometry.Scheme.Modules.finite_moduleSpecΓ {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsFiniteType M] : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)

A quasicoherent sheaf of finite type on Spec R has finite global sections as an R-module.

instance AlgebraicGeometry.Scheme.Modules.isFinitePresentation_cokernel_spec {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsFiniteType M] [SheafOfModules.IsFinitePresentation N] : SheafOfModules.IsFinitePresentation (CategoryTheory.Limits.cokernel f)

The ambient cokernel of a morphism from a quasicoherent sheaf of finite type to a finitely presented sheaf on a spectrum is finitely presented, without a Noetherian hypothesis.

instance AlgebraicGeometry.Scheme.Modules.isFinitePresentation_kernel_spec {R : CommRingCat} {M N : (Spec R).Modules} [IsNoetherianRing ↑R] (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsFiniteType M] [SheafOfModules.IsQuasicoherent N] : SheafOfModules.IsFinitePresentation (CategoryTheory.Limits.kernel f)

Over a Noetherian ring, the ambient kernel of a morphism from a quasicoherent sheaf of finite type to a quasicoherent sheaf is finitely presented.