Coherent sheaves on an affine scheme

Layer B, stage 1. The affine comparison between coherent sheaves on Spec R and finitely presented R-modules.

Main results

• AlgebraicGeometry.isFinitePresentation_tilde — M^~ is of finite presentation whenever M is a finitely presented R-module;
• AlgebraicGeometry.isCoherent_tilde — the same statement phrased with Scheme.Modules.IsCoherent, which is what Coh (Spec R) is carved out of;
• AlgebraicGeometry.isCoherent_tilde_of_finite — over a noetherian ring the hypothesis weakens to finite generation;
• AlgebraicGeometry.moduleFinite_globalSections_of_isFiniteType — finite-type quasi-coherent sheaves have finite global sections on an affine noetherian scheme;
• AlgebraicGeometry.moduleFinitePresentation_globalSections_of_isCoherent — coherent sheaves have finitely presented global sections.
• AlgebraicGeometry.Coh.affineEquivalence — coherent sheaves on Spec R are equivalent to finitely generated R-modules when R is noetherian.

Proof strategy

Mathlib already does the mathematics. AlgebraicGeometry.presentationTilde turns a generating set s for M together with a generating set t for the kernel of R^s → M into a global SheafOfModules.Presentation (tilde M), and that is exactly the data recorded by Module.FinitePresentation. So the content here is only that the presentation is finite — Presentation.IsFinite is finiteness of the two index types, and presentationTilde builds them out of s and t themselves — after which SheafOfModules.IsFinitePresentation.of_presentation applies.

Two elaboration hazards

Both cost more time than the mathematics, and both are recorded here so the next caller does not rediscover them.

1. Universes do not propagate from the goal. Presentation.IsFinite and of_presentation carry universe parameters that bind before their explicit arguments, so a goal phrased as Scheme.Modules.IsCoherent … does not pin them; Lean defaults them to 0 and reports a type mismatch at Type 1 rather than an ambiguity. Annotating .{u, u, u} at the use site is what fixes it — (M := …) does not, because the universes bind first. This is the gotcha already recorded in Algebra/Category/ModuleCat/Sheaf/Presentation.lean.
2. Anonymous constructors do not see the expected type here. refine ⟨⟨?_⟩, ?_⟩ against a ground Presentation.IsFinite … goal still elaborates at universe 0, and refine Presentation.IsFinite.mk ?_ ?_ gets stuck synthesising WEqualsLocallyBijective ?J AddCommGrpCat because the head is elaborated before the goal is unified. constructor unifies with the goal first and goes through.

The Finset/Set mismatch that an earlier investigation predicted — FinitePresentation gives s : Finset M while presentationTilde wants s : Set M and t : Set (↥s →₀ R) — does not in fact bite: the coercion is accepted as written.

The converse finiteness results use the affine comparison and localisation patching developed in AlgebraicGeometry.Modules.Affine.Finiteness.

Affine equivalence

The object-level finiteness results restrict Mathlib's tilde ⊣ Γ adjunction to FGModuleCat R and Coh (Spec R). The restricted unit is inherited from Mathlib's tilde comparison, while the restricted counit is an isomorphism by the affine comparison theorem Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent. Thus the restricted adjunction is an equivalence.

The global-sections functor Coh.affineGlobalSections itself does not need noetherianity: finite presentation already implies finite global sections on an affine scheme. The noetherian hypothesis first appears on FGModuleCat.affineTilde, where it upgrades a finite module to a finitely presented module, and consequently on the adjunction and equivalence.

References

• Stacks, Tag 01IA — quasi-coherent modules on an affine scheme

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

M^~ is of finite presentation when M is.

The presentation is Mathlib's presentationTilde, whose generator and relation index types are the two generating sets supplied by Module.FinitePresentation; finiteness of the presentation is therefore finiteness of those sets.

theorem AlgebraicGeometry.isCoherent_tilde {R : CommRingCat} (M : ModuleCat ↑R) [Module.FinitePresentation ↑R ↑M] : Scheme.Modules.IsCoherent (Spec R) (tilde M)

M^~ is coherent when M is finitely presented.

This is isFinitePresentation_tilde phrased through Scheme.Modules.IsCoherent, which is the predicate Coh (Spec R) is carved out of.

theorem AlgebraicGeometry.isCoherent_tilde_of_finite {R : CommRingCat} [IsNoetherianRing ↑R] (M : ModuleCat ↑R) [Module.Finite ↑R ↑M] : Scheme.Modules.IsCoherent (Spec R) (tilde M)

Over a noetherian ring, M^~ is coherent as soon as M is finitely generated.

Module.finitePresentation_of_finite is where IsNoetherianRing earns its place: finite generation alone is not enough in general, because the relations need not be finitely generated.

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

A quasi-coherent finite-type module sheaf on an affine noetherian scheme has finitely generated global sections. The underlying finite-generation theorem does not need the noetherian hypothesis; it is retained here because this is the public corollary consumed by the noetherian affine equivalence.

theorem AlgebraicGeometry.moduleFinitePresentation_globalSections_of_isCoherent {R : CommRingCat} [IsNoetherianRing ↑R] (M : (Spec R).Modules) (hM : Scheme.Modules.IsCoherent (Spec R) M) : Module.FinitePresentation ↑R ↑(moduleSpecΓFunctor.obj M)

A coherent module sheaf on an affine noetherian scheme has finitely presented global sections.

noncomputable def AlgebraicGeometry.Coh.affineGlobalSections (R : CommRingCat) : CategoryTheory.Functor (Coh (Spec R)) (FGModuleCat ↑R)

Global sections restrict from coherent sheaves on Spec R to finitely generated R-modules. No noetherian hypothesis is needed in this direction.

Equations

• AlgebraicGeometry.Coh.affineGlobalSections R = (ModuleCat.isFG ↑R).lift ((AlgebraicGeometry.Coh.ι (AlgebraicGeometry.Spec R)).comp AlgebraicGeometry.moduleSpecΓFunctor) ⋯

noncomputable def AlgebraicGeometry.FGModuleCat.affineTilde {R : CommRingCat} [IsNoetherianRing ↑R] : CategoryTheory.Functor (FGModuleCat ↑R) (Coh (Spec R))

Over a noetherian ring, tilde restricts from finitely generated modules to coherent sheaves on the affine spectrum.

Equations

• AlgebraicGeometry.FGModuleCat.affineTilde = (AlgebraicGeometry.Spec R).coherent.lift ((ModuleCat.isFG ↑R).ι.comp (AlgebraicGeometry.tilde.functor R)) ⋯

noncomputable def AlgebraicGeometry.Coh.affineAdjunction {R : CommRingCat} [IsNoetherianRing ↑R] : FGModuleCat.affineTilde ⊣ affineGlobalSections R

Mathlib's tilde-global-sections adjunction restricted to finitely generated modules and coherent sheaves on an affine noetherian scheme.

Equations

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

noncomputable def AlgebraicGeometry.Coh.affineEquivalence {R : CommRingCat} [IsNoetherianRing ↑R] : Coh (Spec R) ≌ FGModuleCat ↑R

For a noetherian ring R, coherent sheaves on Spec R are equivalent to finitely generated R-modules. The forward functor is global sections and the inverse is tilde.

Equations

• AlgebraicGeometry.Coh.affineEquivalence = AlgebraicGeometry.Coh.affineAdjunction.toEquivalence.symm

@[simp]

theorem AlgebraicGeometry.Coh.affineEquivalence_functor {R : CommRingCat} [IsNoetherianRing ↑R] : affineEquivalence.functor = affineGlobalSections R

@[simp]

theorem AlgebraicGeometry.Coh.affineEquivalence_inverse {R : CommRingCat} [IsNoetherianRing ↑R] : affineEquivalence.inverse = FGModuleCat.affineTilde