A coherent sheaf is generated on a degree-one chart by finitely many sections

Step 2 of Serre's global generation (#586). On the chart D₊(g) of a degree-one element, a coherent F is generated by finitely many sections over the whole chart: near every point of every open inside D₊(g), every section of F is a structure-sheaf combination of their restrictions.

Where the finiteness comes from, and where it is spent

D₊(g) is Spec A_{(g)}, and moduleFinite_globalSections makes the chart's module of sections finitely generated from finite presentation alone -- no Noetherian hypothesis, as Modules/Coherent/AffineChart.lean records. A finite spanning set of that module is the family.

That the family generates locally, and not merely spans the global sections of the chart, is the affine extension lemma: a section over a smaller basic open D₊(g) ⊓ D₊(f), multiplied by a power of f / gᵉ, extends to the chart (exists_pow_smul_eq_res_chart), where it is a combination of the spanning set; and f / gᵉ is invertible on D₊(g) ⊓ D₊(f) (fracSection_mul_fracSection_symm), so the section itself is a combination there.

The neighbourhood is a positive-degree basic open

Basic opens D₊(r), r : A arbitrary, form a basis of Proj 𝒜, but the chart lemmas need a homogeneous r of positive degree. basicOpen_eq_union_of_projection splits D₊(r) into the basic opens of its homogeneous components, and multiplying the component by g -- which does not move the open outside D₊(g), because D₊(f g) = D₊(f) ⊓ D₊(g) -- raises the degree above zero. exists_mem_basicOpen_le packages that.

Scope

One chart. The family is stated over the chart's image awayι ''ᵁ ⊤, taken as a variable pinned by an equation in the style of ChartProj.lean, so that a caller instantiates it at D₊(g) without transporting sections. The cover, the twist, and the surjection are in GlobalGeneration.lean.

theorem AlgebraicGeometry.Proj.exists_mem_basicOpen_le {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {g : A} (hg : g ∈ 𝒜 1) (U : (Proj 𝒜).Opens) (x : ↥(Proj 𝒜)) (hx : x ∈ U) (hxg : x ∈ ProjectiveSpectrum.basicOpen 𝒜 g) : ∃ (e : ℕ) (f : A) (_ : f ∈ 𝒜 e), 0 < e ∧ x ∈ ProjectiveSpectrum.basicOpen 𝒜 f ∧ ProjectiveSpectrum.basicOpen 𝒜 f ≤ U

A point of an open inside D₊(g) has a positive-degree basic-open neighbourhood in it.

The basis of Proj 𝒜 supplies D₊(r) ∋ x inside U for some r : A; a homogeneous component of r still has x in its basic open (basicOpen_eq_union_of_projection); and multiplying that component by g makes the degree positive while cutting the open down to D₊(g).

theorem AlgebraicGeometry.Proj.exists_finite_generators_of_isCoherent {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (F : (Proj 𝒜).Modules) (hF : Scheme.Modules.IsCoherent (Proj 𝒜) F) {g : A} (hg : g ∈ 𝒜 1) {W : (Proj 𝒜).Opens} (hW : (Scheme.Hom.opensFunctor (awayι 𝒜 g hg Nat.one_pos)).obj ⊤ = W) : ∃ (κ : Type u) (x : Fintype κ) (s : κ → ↑(F.presheaf.obj (Opposite.op W))), ∀ (U : (Proj 𝒜).Opens) (hUW : U ≤ W) (u : ↑(F.presheaf.obj (Opposite.op U))), ∀ x_1 ∈ U, ∃ (V : (Proj 𝒜).Opens) (hVU : V ≤ U), x_1 ∈ V ∧ ∃ (c : κ → ↑((Proj 𝒜).presheaf.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE hVU).op)) u = ∑ a : κ, c a • (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (s a)

Finitely many sections over D₊(g) generate a coherent sheaf there.

For F coherent and g of degree one, there is a finite family of sections of F over the chart such that, near every point of every open U inside the chart, every section of F over U is a structure-sheaf combination of the family's restrictions.

The chart is awayι ''ᵁ ⊤, pinned to the caller's spelling by hW as in ChartProj.lean. The family is a finite spanning set of the chart's module of sections; local generation is the affine extension lemma followed by inverting the chart scalar (f / gᵉ)ⁿ, which is a unit on the positive-degree basic open D₊(g) ⊓ D₊(f) that exists_mem_basicOpen_le finds around the point.