Finiteness from the affine comparison

The affine comparison identifies a quasi-coherent module on Spec R with the tilde of its global sections. This file supplies the finiteness consequences needed by coherent sheaves: a finite family of generators on an affine scheme gives finite global sections, and finiteness can then be checked on a finite basic-open cover.

Main results

• Scheme.Modules.exists_basicOpen_finiteGenerating_cover refines finite-type data to basic opens whose defining elements span the unit ideal;
• Scheme.Modules.moduleFinite_globalSections_of_isFiniteType patches the resulting finite localized modules;
• Scheme.Modules.moduleFinite_globalSections specializes the result to finite presentation.

theorem AlgebraicGeometry.Scheme.Modules.instHasBinaryProductsOverOpensCarrierCarrierCommRingCatSpec_derivedAlgGeo_1 {R : CommRingCat} (U : TopologicalSpace.Opens ↥(Spec R)) : CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over U)

noncomputable def AlgebraicGeometry.Scheme.Modules.GeneratingSections.restrictBasicOpen {R : CommRingCat} (M : (Spec R).Modules) (g : ↑R) (σ : (SheafOfModules.over M (PrimeSpectrum.basicOpen g)).GeneratingSections) : SheafOfModules.GeneratingSections (M.restrict (basicOpenSpecMap g))

Generating sections on D(g) transport to generating sections on Spec R[1/g].

Equations

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

instance AlgebraicGeometry.Scheme.Modules.GeneratingSections.isFiniteType_restrictBasicOpen {R : CommRingCat} (M : (Spec R).Modules) (g : ↑R) (σ : (SheafOfModules.over M (PrimeSpectrum.basicOpen g)).GeneratingSections) [σ.IsFiniteType] : (restrictBasicOpen M g σ).IsFiniteType

Restriction from a basic open to its affine spectrum preserves finite generation.

noncomputable def AlgebraicGeometry.Scheme.Modules.QuasicoherentData.restrictBasicOpen {R : CommRingCat} (M : (Spec R).Modules) (g : ↑R) (q : SheafOfModules.QuasicoherentData M) : SheafOfModules.QuasicoherentData (M.restrict (basicOpenSpecMap g))

Quasi-coherent presentation data transports from Spec R to the affine scheme corresponding to D(g). Keeping this transport behind an opaque definition prevents later callers from repeatedly normalizing the two nested site equivalences.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_restrictBasicOpen_of_quasicoherentData {R : CommRingCat} (M : (Spec R).Modules) (g : ↑R) (q : SheafOfModules.QuasicoherentData M) : CategoryTheory.IsIso (M.restrict (basicOpenSpecMap g)).fromTildeΓ

The affine comparison for the restriction to D(g), built from explicit quasi-coherent data on the original affine scheme.

theorem AlgebraicGeometry.Scheme.Modules.moduleFinite_globalSections_of_generatingSections {R : CommRingCat} (M : (Spec R).Modules) (σ : SheafOfModules.GeneratingSections M) [σ.IsFiniteType] [CategoryTheory.IsIso M.fromTildeΓ] : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)

A finite family of global generators gives finitely generated global sections whenever the affine comparison map is an isomorphism.

noncomputable def AlgebraicGeometry.Scheme.Modules.freeEpiOfSpan {R : CommRingCat} (M : (Spec R).Modules) (s : Set ↑(moduleSpecΓFunctor.obj M)) : SheafOfModules.free ↑s ⟶ M

The map out of a free sheaf that a chosen spanning family provides.

Transport across tildeFinsupp, apply tilde to Finsupp.linearCombination, and land through the affine comparison.

M.fromTildeΓ is composed with, not inverted, so the map exists for any M. It is epi_freeEpiOfSpan that needs [IsIso M.fromTildeΓ], and it takes it there.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.epi_freeEpiOfSpan {R : CommRingCat} (M : (Spec R).Modules) [CategoryTheory.IsIso M.fromTildeΓ] (s : Set ↑(moduleSpecΓFunctor.obj M)) (hs : Submodule.span (↑R) s = ⊤) : CategoryTheory.Epi (M.freeEpiOfSpan s)

It is an epimorphism exactly when the chosen family spans.

tilde is a left adjoint (tilde.adjunction), so it preserves colimits and hence epimorphisms; Finsupp.linearCombination is surjective precisely when the span is everything (Finsupp.range_linearCombination); and the two outer maps are isomorphisms.

Two elaboration hazards, both paid for once:

1. Keep PreservesEpimorphisms inside the have. Left in context as a local instance it makes every later instance search diverge, and the resulting heartbeat timeout is reported as an ordinary "failed to synthesize", which reads like a missing instance rather than a budget.
2. backward.isDefEq.respectTransparency false is required, as elsewhere in this repository: without it the goal after the first rewrite is "not type-correct under the instances transparency level" and Iso.hom_inv_id_assoc silently fails to match.

theorem AlgebraicGeometry.Scheme.Modules.exists_finite_free_epi_of_moduleFinite {R : CommRingCat} (M : (Spec R).Modules) [CategoryTheory.IsIso M.fromTildeΓ] [Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)] : ∃ (I : Type u) (_ : Finite I) (p : SheafOfModules.free I ⟶ M), CategoryTheory.Epi p

A finite module of global sections gives a finite free epimorphism.

The converse of moduleFinite_globalSections_of_generatingSections, and the direction Serre's global generation needs: paired with GeneratingSections.ofFreeEpi it turns Module.Finite of the global sections into an M.GeneratingSections, closing the loop between the two.

The index type is a Finset of the global sections, so its finiteness is definitional rather than transported.

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

A finite global presentation on an affine scheme gives finitely generated global sections.

theorem AlgebraicGeometry.Scheme.Modules.exists_basicOpen_finiteGenerating_cover {R : CommRingCat} (M : (Spec R).Modules) (hM : SheafOfModules.IsFiniteType M) : ∃ (I : Type u) (g : I → ↑R), Ideal.span (Set.range g) = ⊤ ∧ ∀ (i : I), ∃ (σ : (SheafOfModules.over M (PrimeSpectrum.basicOpen (g i))).GeneratingSections), σ.IsFiniteType

A finite-type module sheaf on Spec R has finite generating families on a basic-open cover whose defining elements generate the unit ideal.

theorem AlgebraicGeometry.Scheme.Modules.moduleFinite_globalSections_of_isFiniteType {R : CommRingCat} (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 scheme has finitely generated global sections. This is the finite-generation corollary of the affine comparison.

theorem AlgebraicGeometry.Scheme.Modules.moduleFinite_globalSections {R : CommRingCat} (M : (Spec R).Modules) (hM : SheafOfModules.IsFinitePresentation M) : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)

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