Presentations on a basic-open cover

A quasi-coherent sheaf on an affine scheme has presentations on the members of some cover of the open-set site. This file refines that cover to basic opens. Mathlib v4.32.1 supplies the global quasi-coherent affine comparison; this local refinement remains a separate presentation-cover result.

Main results

• AlgebraicGeometry.Scheme.Modules.exists_basicOpen_presentation_cover_of_quasicoherentData refines explicit quasi-coherent data to a cover by basic opens carrying presentations.
• AlgebraicGeometry.Scheme.Modules.exists_basicOpen_presentation_cover does the same for a quasi-coherent sheaf and records that the defining elements generate the unit ideal.

Implementation notes

The cover index consists of a member U of the quasi-coherent presentation cover together with a basic open contained in U. Every point lies in one of the original cover members, and the basis theorem for principal opens supplies a contained D(g) through that point. The identity PrimeSpectrum.iSup_basicOpen_eq_top_iff then turns the resulting topological cover into the unit-ideal condition.

Restriction of presentations and quasi-coherent data to arbitrary over sites is supplied by Algebra.Category.ModuleCat.Sheaf.Presentation.Over; this file begins when the open-set site is that of Spec R and the cover is refined to distinguished opens. Mathlib's finite-cover comparison proof is in AlgebraicGeometry/Modules/Tilde.lean; this result is not an input to that upstream proof.

References

• Stacks, Tag 01IA, for the affine quasi-coherent comparison context.
• See the affine and projective spectrum placement map for the pinned source of the basic-open cover criterion.

Tags

affine scheme, basic opens, quasi-coherent data, presentations, unit-ideal cover

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

theorem AlgebraicGeometry.Scheme.Modules.exists_basicOpen_presentation_cover_of_quasicoherentData {R : CommRingCat} (M : (Spec R).Modules) (q : SheafOfModules.QuasicoherentData M) : ∃ (I : Type u) (g : I → ↑R), Ideal.span (Set.range g) = ⊤ ∧ ∀ (i : I), Nonempty (SheafOfModules.over M (PrimeSpectrum.basicOpen (g i))).Presentation

Explicit quasi-coherent data on Spec R refines to presentations on a basic-open cover.

theorem AlgebraicGeometry.Scheme.Modules.exists_basicOpen_presentation_cover {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : ∃ (I : Type u) (g : I → ↑R), Ideal.span (Set.range g) = ⊤ ∧ ∀ (i : I), Nonempty (SheafOfModules.over M (PrimeSpectrum.basicOpen (g i))).Presentation

A quasi-coherent sheaf on Spec R has presentations on a basic-open cover.

The algebraic cover condition says that the defining elements generate the unit ideal; equivalently, the corresponding basic opens have supremum ⊤.