Finite global presentations give finitely presented sheaves

SheafOfModules.Presentation.quasicoherentData turns a global presentation into quasicoherent data on the trivial cover. This file records that the data is finite when the presentation is, and hence that a sheaf of modules with a finite global presentation is of finite presentation.

Together with presentationOfIsCokernelFree, this is what concrete constructions need: anything exhibited as the cokernel of a map between finitely generated free sheaves is of finite presentation, hence coherent on a locally noetherian scheme.

The one non-obvious step

Presentation.isFinite_map is stated for a functor into sheaves of modules over a second sheaf of rings S on a second site J'. Applying it here without pinning S leaves J' a metavariable, and Lean then tries to synthesise HasSheafify J' AddCommGrpCat against that metavariable and fails outright rather than postponing. Supplying (S := R.over x) makes J' ground and everything resolves.

The failure this produces is thoroughly misleading: it reports a missing HasSheafify (J.over x) AddCommGrpCat even though [∀ X, HasSheafify (J.over X) AddCommGrpCat] is in scope and prints identically under pp.universes. It is not a universe problem, not a variable-inclusion problem, and not a limitation on ∀-quantified instance hypotheses — those all check out in isolation.

Main results

• Presentation.isFinitePresentation_quasicoherentData
• IsFinitePresentation.of_presentation

Destined for Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean.

Note for callers

Applying of_presentation at a concrete presentation is fiddlier than it looks, and the symptom is always a universe defaulted to 0. Both this theorem and Mathlib's Presentation.IsFinite carry universe parameters that a goal phrased in other terms — say Scheme.Modules.IsCoherent … — does not pin, and Lean then elaborates them at .{0, 0, 0} and reports a type mismatch at Type 1 rather than an ambiguity. (M := …) does not fix it, because the universes bind before M; Presentation.IsFinite.{u, u, u} does. Expect to annotate.

instance SheafOfModules.Presentation.isFinitePresentation_quasicoherentData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) [P.IsFinite] : P.quasicoherentData.IsFinitePresentation

Quasicoherent data built from a finite global presentation is finite.

quasicoherentData covers by the terminal object alone and sets each local presentation to P.map (pushforward (𝟙 _)) _, so this is Presentation.isFinite_map.

theorem SheafOfModules.IsFinitePresentation.of_presentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) [P.IsFinite] : M.IsFinitePresentation

A sheaf of modules with a finite global presentation is of finite presentation.