Quasi-coherence, coherence, and sections on Proj

This file is the finiteness-facing boundary of DerivedAlgGeo's graded-module sheaf construction. Mathlib supplies the affine charts

Spec (A_f)₀ ⟶ Proj A,

while AlgebraicGeometry.Proj.Modules.AssociatedSheaf supplies the sheaf M̃, its stalks, and the canonical map

(M_f)₀ ⟶ Γ(D₊(f), M̃).

The general affine comparison is deliberately represented by AffineComparisonData: it is an isomorphism between the restriction of M̃ to each standard affine chart and Mathlib's affine tilde construction. For the graded ring considered as a module over itself, this file now constructs the comparison canonically from associatedSheafSelfIso; no certificate input is needed in that case. Once comparison data is present, quasi-coherence follows by gluing the affine presentations, and coherence follows from explicit finite-presentation hypotheses on the localized modules.

The global-section API is similarly conservative. TwistingSectionRange records exactly the degrees in which a chosen algebraic module is known to compute Γ(Proj A, O(d)); no all-degree Serre correspondence is asserted. The projective-space corollary uses Mathlib's finite generation of homogeneous multivariate polynomials and therefore has no hidden noetherianity assumption.

Main declarations

• AffineComparisonData: affine tilde comparison on every standard Proj chart;
• affineComparisonDataSelf: the constructed comparison for the structure module;
• localizedNatShiftDegreeOneIso: the explicit rank-one trivialization of A(d) on a degree-one chart;
• moduleAwayToSection_natShift_degreeOne_bijective: the corresponding constructed basic-open section comparison for every nonnegative twist;
• associatedSheaf_isQuasicoherent: quasi-coherence from those comparisons;
• associatedSheaf_isCoherent_of_finitePresentation: coherence from explicit finite presentation of every localized module;
• associatedSheaf_isCoherent_of_noetherian_finite: the common noetherian + finite-generation specialization;
• BasicOpenSectionData: bijectivity of the canonical basic-open section map;
• basicOpenSectionDataSelf: constructed basic-open certificates for the structure module;
• TwistingSectionRange: a degree-bounded global-section comparison for O(d);
• projectiveSpace_globalSections_finite: finite generation for the polynomial-ring specialization in every certified degree.

The standard affine charts

@[reducible, inline]

abbrev AlgebraicGeometry.Proj.StandardChartIndex {A σA : Type u} [SetLike σA A] (𝒜 : ℕ → σA) : Type u

The canonical index type for the standard affine cover of Proj A: a positive natural degree together with a homogeneous element of that degree.

Equations

• AlgebraicGeometry.Proj.StandardChartIndex 𝒜 = ((n : ℕ+) × ↥(𝒜 ↑n))

noncomputable def AlgebraicGeometry.Proj.standardAway {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (i : StandardChartIndex 𝒜) : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 ↑i.snd)) ⟶ Proj 𝒜

The standard affine chart morphism Spec (A_f)₀ ⟶ Proj A.

Equations

• AlgebraicGeometry.Proj.standardAway 𝒜 i = AlgebraicGeometry.Proj.awayι 𝒜 ↑i.snd ⋯ ⋯

instance AlgebraicGeometry.Proj.standardAway_isOpenImmersion {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (i : StandardChartIndex 𝒜) : IsOpenImmersion (standardAway 𝒜 i)

noncomputable def AlgebraicGeometry.Proj.localizedModule {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (i : StandardChartIndex 𝒜) : ModuleCat (HomogeneousLocalization.Away 𝒜 ↑i.snd)

The degree-zero localization of M on a standard affine chart, bundled as a module over the chart ring (A_f)₀.

Equations

• AlgebraicGeometry.Proj.localizedModule 𝒜 𝓜 i = ModuleCat.of (HomogeneousLocalization.Away 𝒜 ↑i.snd) ↥(GradedModule.DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers ↑i.snd))

@[simp]

theorem AlgebraicGeometry.Proj.standardAway_eq_affineOpenCover_f {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (i : StandardChartIndex 𝒜) : standardAway 𝒜 i = (affineOpenCover 𝒜).f i

Affine comparison and quasi-coherence

structure AlgebraicGeometry.Proj.AffineComparisonData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] : Type u

The exact local input needed to recognize M̃ as quasi-coherent.

Each field identifies the restriction to a standard chart with the affine sheaf attached to the degree-zero localized module. It is data, not an axiom or typeclass: callers can see precisely where the still-missing graded affine-comparison proof is used.

• localIso (i : StandardChartIndex 𝒜) : (associatedSheaf 𝒜 𝓜).restrict (standardAway 𝒜 i) ≅ tilde (localizedModule 𝒜 𝓜 i)

noncomputable def AlgebraicGeometry.Proj.localizedModuleSelfIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (i : StandardChartIndex 𝒜) : localizedModule 𝒜 𝒜 i ≅ ModuleCat.of (HomogeneousLocalization.Away 𝒜 ↑i.snd) (HomogeneousLocalization.Away 𝒜 ↑i.snd)

For the structure module, the localized module on a standard chart is the chart ring as a module over itself.

Equations

• AlgebraicGeometry.Proj.localizedModuleSelfIso 𝒜 i = (GradedModule.DegreeZeroLocalization.selfLinearEquiv 𝒜 (Submonoid.powers ↑i.snd)).symm.toModuleIso

def AlgebraicGeometry.Proj.degreeOneStandardChart {A σA : Type u} [SetLike σA A] (𝒜 : ℕ → σA) (f : ↥(𝒜 1)) : StandardChartIndex 𝒜

A degree-one homogeneous element, bundled as a standard positive-degree chart index.

Equations

• AlgebraicGeometry.Proj.degreeOneStandardChart 𝒜 f = ⟨⟨1, Nat.zero_lt_one⟩, f⟩

noncomputable def AlgebraicGeometry.Proj.localizedNatShiftDegreeOneIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (f : ↥(𝒜 1)) (d : ℕ) : localizedModule 𝒜 (GradedModule.natShift 𝒜 d) (degreeOneStandardChart 𝒜 f) ≅ ModuleCat.of (HomogeneousLocalization.Away 𝒜 ↑f) (HomogeneousLocalization.Away 𝒜 ↑f)

On a degree-one chart, the localized module underlying the nonnegative twist A(d) is canonically free of rank one.

Equations

• AlgebraicGeometry.Proj.localizedNatShiftDegreeOneIso 𝒜 f d = (GradedModule.DegreeZeroLocalization.natShiftAwayLinearEquiv 𝒜 ⋯ d).toModuleIso

noncomputable def AlgebraicGeometry.Proj.natShiftOverIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {V : (Proj 𝒜).Opens} (hV : V ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.natShift 𝒜 d)) V ≅ SheafOfModules.over (associatedSheaf 𝒜 𝒜) V

Over an open contained in a degree-one chart, the nonnegative twist A(d)̃ is isomorphic to the structure module as a sheaf of modules on the slice site.

The componentwise map is the chart trivialization natShiftSectionLinearEquivOn, and naturality is natShiftSectionToSelfOn_map: dividing by f ^ d is pointwise, so it commutes with restriction on the nose. Working on the slice over V rather than after restriction along the chart immersion avoids crossing the open immersion entirely; SheafOfModules.QuasicoherentData transports along this isomorphism directly.

Equations

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

theorem AlgebraicGeometry.Proj.standardAway_degreeOne_opensRange_le {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (f : ↥(𝒜 1)) : Scheme.Hom.opensRange (standardAway 𝒜 (degreeOneStandardChart 𝒜 f)) ≤ ProjectiveSpectrum.basicOpen 𝒜 ↑f

A degree-one standard chart has range exactly its basic open, so the twist trivialization applies over it.

noncomputable def AlgebraicGeometry.Proj.affineComparisonDataSelf {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : AffineComparisonData 𝒜 𝒜

The canonical affine-chart comparison for the graded ring considered as a module over itself. This is constructed from the global structure-module isomorphism, restriction of the unit module, and Mathlib's tildeSelf; it is not certificate input.

Equations

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

noncomputable def AlgebraicGeometry.Proj.AffineComparisonData.localQuasicoherentData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) (i : StandardChartIndex 𝒜) : (SheafOfModules.over (associatedSheaf 𝒜 𝓜) (Scheme.Hom.opensRange (standardAway 𝒜 i))).QuasicoherentData

Quasi-coherent data on one range slice, transported from the affine tilde presentation.

Equations

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

theorem AlgebraicGeometry.Proj.AffineComparisonData.standardCharts_coversTop {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : (Opens.grothendieckTopology ↥(Proj 𝒜)).CoversTop fun (i : StandardChartIndex 𝒜) => Scheme.Hom.opensRange (standardAway 𝒜 i)

The standard affine charts cover Proj A in the open-set Grothendieck topology.

noncomputable def AlgebraicGeometry.Proj.AffineComparisonData.quasicoherentData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) : SheafOfModules.QuasicoherentData (associatedSheaf 𝒜 𝓜)

Global quasi-coherent data obtained by gluing the standard affine tilde presentations.

Equations

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

theorem AlgebraicGeometry.Proj.AffineComparisonData.associatedSheaf_isQuasicoherent {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) : SheafOfModules.IsQuasicoherent (associatedSheaf 𝒜 𝓜)

The associated sheaf of a graded module is quasi-coherent once the canonical affine-chart comparisons have been supplied.

Comparison on a sub-family of charts

AffineComparisonData asks for a comparison on every standard chart, and for some modules that is more than is true. The nonnegative twist A(d) is the motivating case: it is trivialized on a chart D₊(f) by dividing by a power of f, which needs deg f to divide the twist, so localizedNatShiftDegreeOneIso is available in degree one and not in general. Asking for all degrees would be asking for O(d) to be locally free on Proj of an arbitrary graded ring, which is false.

Quasi-coherence does not need it. It is a local property and SheafOfModules.QuasicoherentData.bind glues over any covering family, so a sub-family that still covers is enough. AffineComparisonDataOn is that weakening; AffineComparisonData is the total-family case and is unchanged.

structure AlgebraicGeometry.Proj.AffineComparisonDataOn {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {ι : Type u} (charts : ι → StandardChartIndex 𝒜) : Type u

Affine tilde comparison on a chosen family of standard charts, together with the proof that the family covers. Weaker than AffineComparisonData, and enough for quasi-coherence.

• coversTop : (Opens.grothendieckTopology ↥(Proj 𝒜)).CoversTop fun (j : ι) => Scheme.Hom.opensRange (standardAway 𝒜 (charts j))

  The chosen charts cover Proj A; without this the local data glues to nothing.

• localIso (j : ι) : (associatedSheaf 𝒜 𝓜).restrict (standardAway 𝒜 (charts j)) ≅ tilde (localizedModule 𝒜 𝓜 (charts j))

  The affine comparison on each chart of the family.

noncomputable def AlgebraicGeometry.Proj.AffineComparisonDataOn.localQuasicoherentData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ℕ → σA} {𝓜 : ℕ → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {ι : Type u} {charts : ι → StandardChartIndex 𝒜} (c : AffineComparisonDataOn 𝒜 𝓜 charts) (j : ι) : (SheafOfModules.over (associatedSheaf 𝒜 𝓜) (Scheme.Hom.opensRange (standardAway 𝒜 (charts j)))).QuasicoherentData

Quasi-coherent data on one chart of the family, transported from its tilde presentation. The same argument as AffineComparisonData.localQuasicoherentData, over one index.

Equations

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

theorem AlgebraicGeometry.Proj.AffineComparisonDataOn.associatedSheaf_isQuasicoherent {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ℕ → σA} {𝓜 : ℕ → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {ι : Type u} {charts : ι → StandardChartIndex 𝒜} (c : AffineComparisonDataOn 𝒜 𝓜 charts) : SheafOfModules.IsQuasicoherent (associatedSheaf 𝒜 𝓜)

Quasi-coherence from comparisons on a covering sub-family of charts.

theorem AlgebraicGeometry.Proj.degreeOneCharts_coversTop {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {ι : Type u} (f : ι → ↥(𝒜 1)) (hf : Algebra.adjoin (↥(𝒜 0)) (Set.range fun (j : ι) => ↑(f j)) = ⊤) : (Opens.grothendieckTopology ↥(Proj 𝒜)).CoversTop fun (j : ι) => Scheme.Hom.opensRange (standardAway 𝒜 (degreeOneStandardChart 𝒜 (f j)))

A family of degree-one elements generating A over 𝒜 0 gives a covering family of degree-one charts.

This is what makes the sub-family weakening usable: AffineComparisonDataOn needs a covering family, and for a graded ring generated in degree one — projective space being the case this library computes on — the degree-one charts already cover, so nothing of higher degree is needed. Mathlib's Proj.iSup_basicOpen_eq_top' does the work; the content here is only identifying each chart's range with its basic open.

def AlgebraicGeometry.Proj.AffineComparisonData.toOn {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) : AffineComparisonDataOn 𝒜 𝓜 id

The total family is a family: every AffineComparisonData restricts to one on all charts.

Equations

• AlgebraicGeometry.Proj.AffineComparisonData.toOn 𝒜 𝓜 c = { coversTop := ⋯, localIso := c.localIso }

theorem AlgebraicGeometry.Proj.associatedSheaf_self_isQuasicoherent {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : SheafOfModules.IsQuasicoherent (associatedSheaf 𝒜 𝒜)

The associated structure module is quasi-coherent with no external chart certificate.

noncomputable def AlgebraicGeometry.Proj.natShiftLocalQuasicoherentData {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (f : ↥(𝒜 1)) (d : ℕ) : (SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.natShift 𝒜 d)) (Scheme.Hom.opensRange (standardAway 𝒜 (degreeOneStandardChart 𝒜 f)))).QuasicoherentData

Quasi-coherent data for a nonnegative twist on a degree-one standard chart, obtained by transporting the structure module's data along the chart trivialization.

No AffineComparisonData for natShift 𝒜 d is required, and none is available: that structure demands a comparison on every standard chart, including charts of degree greater than one, where A(d) need not be trivial at all. Quasi-coherence does not need them. It is local, so data on any covering family suffices, and SheafOfModules.QuasicoherentData.bind accepts any such family — for a graded ring generated in degree one the degree-one charts already cover.

Equations

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

noncomputable def AlgebraicGeometry.Proj.natShiftQuasicoherentData {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {I : Type u} (g : I → ↥(𝒜 1)) (d : ℕ) (hg : Algebra.adjoin (↥(𝒜 0)) (Set.range fun (j : I) => ↑(g j)) = ⊤) : SheafOfModules.QuasicoherentData (associatedSheaf 𝒜 (GradedModule.natShift 𝒜 d))

Quasi-coherent data for a nonnegative twist, glued from the degree-one charts alone.

Equations

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

theorem AlgebraicGeometry.Proj.natShift_isQuasicoherent {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {I : Type u} (g : I → ↥(𝒜 1)) (d : ℕ) (hg : Algebra.adjoin (↥(𝒜 0)) (Set.range fun (j : I) => ↑(g j)) = ⊤) : SheafOfModules.IsQuasicoherent (associatedSheaf 𝒜 (GradedModule.natShift 𝒜 d))

A nonnegative twist is quasi-coherent as soon as degree-one elements generate A over 𝒜 0.

The hypothesis is exactly what the degree-one trivialization needs, and it is strictly weaker than an AffineComparisonData for natShift 𝒜 d, which would demand a comparison on charts of every positive degree — charts on which A(d) need not be trivial at all. It is the same hypothesis degreeOneCharts_coversTop takes, so the two compose directly.

Integer twists

The same three steps as the nonnegative case. The one difference is that the chart trivialization lands at A(0) rather than at A, so the transport is composed with the zero-normalization — which is an isomorphism for the cheapest possible reason: intShift 𝒜 0 and 𝒜 have the same members.

noncomputable def AlgebraicGeometry.Proj.intShiftOverIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {V : (Proj 𝒜).Opens} (hV : V ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 d)) V ≅ SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 0)) V

Trivializing an integer twist over an open contained in a degree-one chart.

Equations

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

The same, for a graded module

intShiftOverIso and the chart trivializations under it are stated for 𝒜 as a module over itself, which is all quasi-coherence and coherence of O(d) ever need. #584's tensor comparison F ⊗ O(d) ≅ F(d) needs an arbitrary graded module, and the port is direct now that intShiftModuleSectionLinearEquivOn exists: the same three steps, at 𝓜 instead of 𝒜.

noncomputable def AlgebraicGeometry.Proj.intShiftModuleOverIso {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {V : (Proj 𝒜).Opens} (hV : V ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝓜 d)) V ≅ SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝓜 0)) V

Trivializing an integer twist of a graded module over an open inside a degree-one chart.

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftModuleZeroIso {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] : associatedSheaf 𝒜 (GradedModule.intShift 𝓜 0) ≅ associatedSheaf 𝒜 𝓜

The zero twist of a graded module is the module itself, as associated sheaves.

Equations

• AlgebraicGeometry.Proj.intShiftModuleZeroIso 𝒜 𝓜 = AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff 𝒜 (GradedModule.intShift 𝓜 0) 𝓜 ⋯

noncomputable def AlgebraicGeometry.Proj.intShiftModuleOverSelfIso {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {V : (Proj 𝒜).Opens} (hV : V ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝓜 d)) V ≅ SheafOfModules.over (associatedSheaf 𝒜 𝓜) V

On a degree-one chart, an integer twist of a graded module is the module itself.

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftZeroIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : associatedSheaf 𝒜 (GradedModule.intShift 𝒜 0) ≅ associatedSheaf 𝒜 𝒜

The zero twist is the structure module, as associated sheaves.

Equations

• AlgebraicGeometry.Proj.intShiftZeroIso 𝒜 = AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff 𝒜 (GradedModule.intShift 𝒜 0) 𝒜 ⋯

noncomputable def AlgebraicGeometry.Proj.intShiftLocalQuasicoherentData {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (f : ↥(𝒜 1)) (d : ℤ) : (SheafOfModules.over (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 d)) (Scheme.Hom.opensRange (standardAway 𝒜 (degreeOneStandardChart 𝒜 f)))).QuasicoherentData

Quasi-coherent data for an integer twist on a degree-one standard chart.

As in the nonnegative case no AffineComparisonData for intShift 𝒜 d is required or available: quasi-coherence is local, and for a graded ring generated in degree one the degree-one charts already cover.

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftQuasicoherentData {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {I : Type u} (g : I → ↥(𝒜 1)) (d : ℤ) (hg : Algebra.adjoin (↥(𝒜 0)) (Set.range fun (j : I) => ↑(g j)) = ⊤) : SheafOfModules.QuasicoherentData (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 d))

Quasi-coherent data for an integer twist, glued from the degree-one charts alone.

Equations

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

theorem AlgebraicGeometry.Proj.intShift_isQuasicoherent {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {I : Type u} (g : I → ↥(𝒜 1)) (d : ℤ) (hg : Algebra.adjoin (↥(𝒜 0)) (Set.range fun (j : I) => ↑(g j)) = ⊤) : SheafOfModules.IsQuasicoherent (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 d))

Every integer twist is quasi-coherent as soon as degree-one elements generate A over 𝒜 0.

This is the hypothesis the nonnegative statement already takes, unchanged: the sign of the twist never enters, because the chart trivialization it rests on is uniform in the sign.

Coherence

structure AlgebraicGeometry.Proj.LocalizedFinitePresentationData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] : Prop

Explicit finite-presentation hypotheses for all degree-zero localized modules. No noetherianity is needed when these stronger hypotheses are available directly.

• finitePresentation (i : StandardChartIndex 𝒜) : Module.FinitePresentation (HomogeneousLocalization.Away 𝒜 ↑i.snd) ↑(localizedModule 𝒜 𝓜 i)

structure AlgebraicGeometry.Proj.LocalizedNoetherianFiniteData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] : Prop

Explicit hypotheses for the common noetherian criterion: every standard chart ring is noetherian and every degree-zero localized module is finitely generated.

• isNoetherian (i : StandardChartIndex 𝒜) : IsNoetherianRing (HomogeneousLocalization.Away 𝒜 ↑i.snd)
• finite (i : StandardChartIndex 𝒜) : Module.Finite (HomogeneousLocalization.Away 𝒜 ↑i.snd) ↑(localizedModule 𝒜 𝓜 i)

theorem AlgebraicGeometry.Proj.associatedSheaf_isCoherent_of_finitePresentation {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) (hfin : LocalizedFinitePresentationData 𝒜 𝓜) : Scheme.Modules.IsCoherent (Proj 𝒜) (associatedSheaf 𝒜 𝓜)

Finite presentation of all standard-chart localizations makes the associated sheaf coherent.

The proof uses Mathlib's finite-presentation theorem for affine tilde, transports it across the explicit local comparison, and glues over the canonical affine open cover.

theorem AlgebraicGeometry.Proj.localizedFinitePresentationDataSelf {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : LocalizedFinitePresentationData 𝒜 𝒜

The structure module has the required finite-presentation data on every standard chart.

theorem AlgebraicGeometry.Proj.associatedSheaf_self_isCoherent {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : Scheme.Modules.IsCoherent (Proj 𝒜) (associatedSheaf 𝒜 𝒜)

The associated structure module is coherent without an external comparison or finiteness certificate.

theorem AlgebraicGeometry.Proj.associatedSheaf_isCoherent_of_noetherian_finite {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : AffineComparisonData 𝒜 𝓜) (hfin : LocalizedNoetherianFiniteData 𝒜 𝓜) : Scheme.Modules.IsCoherent (Proj 𝒜) (associatedSheaf 𝒜 𝓜)

Over noetherian standard chart rings, finite generation of the localized modules is enough for coherence. Both hypotheses are fields of hfin, so neither is inferred globally.

Basic-open and global sections

structure AlgebraicGeometry.Proj.BasicOpenSectionData {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] : Prop

Bijectivity certificates for the canonical maps (M_f)₀ → Γ(D₊(f), M̃) on all standard charts. Keeping this separate from AffineComparisonData is useful when a proof only needs sections and not an isomorphism of sheaves.

• bijective (i : StandardChartIndex 𝒜) : Function.Bijective ⇑(moduleAwayToSection 𝒜 𝓜 ↑i.snd)

theorem AlgebraicGeometry.Proj.basicOpenSectionDataSelf {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : BasicOpenSectionData 𝒜 𝒜

The canonical basic-open section certificates for the graded ring as a module over itself.

noncomputable def AlgebraicGeometry.Proj.basicOpenSectionEquiv {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (c : BasicOpenSectionData 𝒜 𝓜) (i : StandardChartIndex 𝒜) : ↥(GradedModule.DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers ↑i.snd)) ≃+ (associatedSheafInType 𝒜 𝓜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑i.snd))

The canonical additive equivalence on a standard basic open, obtained from its explicit bijectivity certificate.

Equations

• AlgebraicGeometry.Proj.basicOpenSectionEquiv 𝒜 𝓜 c i = AddEquiv.ofBijective (AlgebraicGeometry.Proj.moduleAwayToSection 𝒜 𝓜 ↑i.snd) ⋯

noncomputable def AlgebraicGeometry.Proj.twistingGlobalSectionsModule {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (R : Type u) [CommRing R] (ρ : R →+* ↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op ⊤))) (d : ℤ) : ModuleCat R

Global sections of O(d), viewed as a module over a chosen base ring map into global functions. The ring map is explicit because Γ(Proj A, O) need not be definitionally A₀.

Equations

• AlgebraicGeometry.Proj.twistingGlobalSectionsModule 𝒜 R ρ d = (ModuleCat.restrictScalars ρ).obj ((AlgebraicGeometry.Proj.twistingSheaf 𝒜 d).val.obj (Opposite.op ⊤))

structure AlgebraicGeometry.Proj.TwistingSectionRange {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (R : Type u) [CommRing R] (ρ : R →+* ↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op ⊤))) : Type (u + 1)

A deliberately degree-bounded identification of algebraic modules with the global sections of O(d). This is the precise input consumed by Serre-finiteness arguments; it does not claim a global-section formula outside degrees.

• degrees : Set ℕ
• algebraicSections : ℕ → ModuleCat R
• comparison (d : ℕ) (hd : d ∈ self.degrees) : self.algebraicSections d ≅ twistingGlobalSectionsModule 𝒜 R ρ ↑d

theorem AlgebraicGeometry.Proj.TwistingSectionRange.globalSections_finite {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {R : Type u} [CommRing R] {ρ : R →+* ↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op ⊤))} (c : TwistingSectionRange 𝒜 R ρ) (d : ℕ) (hd : d ∈ c.degrees) [Module.Finite R ↑(c.algebraicSections d)] : Module.Finite R ↑(twistingGlobalSectionsModule 𝒜 R ρ ↑d)

Finite generation transfers across a certified global-section comparison in one degree.

Projective-space specialization

theorem AlgebraicGeometry.Proj.projectiveSpace_variableSection_bijective (ι R : Type u) [CommRing R] (i : ι) (d : ℕ) : Function.Bijective ⇑(moduleAwayToSection (MvPolynomial.polynomialGrading ι R) (GradedModule.natShift (MvPolynomial.polynomialGrading ι R) d) (MvPolynomial.X i))

Every standard variable chart of polynomial projective space has the constructed basic-open section comparison for each nonnegative twist.

structure AlgebraicGeometry.Proj.ProjectiveSpaceSectionComparison (ι R : Type u) [CommRing R] (ρ : R →+* ↑((ProjectiveSpectrum.Proj.structureSheaf (MvPolynomial.polynomialGrading ι R)).obj.obj (Opposite.op ⊤))) (d : ℕ) : Type u

A section comparison for projective space in degree d. The source is the concrete module of homogeneous polynomials of degree d; the target is Γ(Proj R[X_i], O(d)), restricted to the chosen base-ring action.

• comparison : ModuleCat.of R ↥(MvPolynomial.homogeneousSubmodule ι R d) ≅ twistingGlobalSectionsModule (MvPolynomial.polynomialGrading ι R) R ρ ↑d

theorem AlgebraicGeometry.Proj.projectiveSpace_globalSections_finite {ι R : Type u} [CommRing R] [Finite ι] {ρ : R →+* ↑((ProjectiveSpectrum.Proj.structureSheaf (MvPolynomial.polynomialGrading ι R)).obj.obj (Opposite.op ⊤))} (d : ℕ) (c : ProjectiveSpaceSectionComparison ι R ρ d) : Module.Finite R ↑(twistingGlobalSectionsModule (MvPolynomial.polynomialGrading ι R) R ρ ↑d)

In a finite-variable projective-space specialization, every certified nonnegative twist has finitely generated global sections over the base ring.