Coherence of the integer twists

Quasi-coherence of O(d) is proved in DerivedAlgGeo.AlgebraicGeometry.ProjectiveSpectrum.Modules.Finiteness by trivializing the twist on the degree-one charts. Coherence follows the same route and for the same reason: coherence is local, the degree-one charts cover when A is generated in degree one, and on such a chart O(d) is isomorphic to the structure sheaf, which is coherent.

The restriction to degree-one charts is not an artifact. On a chart D₊(f) with deg f = m the twist O(d) is trivial only when m ∣ d, so no comparison on charts of every positive degree is available and AffineComparisonData for intShift 𝒜 d cannot be asked for.

noncomputable def AlgebraicGeometry.Proj.intShiftOverSelfIso {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))) ≅ SheafOfModules.over (associatedSheaf 𝒜 𝒜) (Scheme.Hom.opensRange (standardAway 𝒜 (degreeOneStandardChart 𝒜 f)))

On a degree-one chart, an integer twist is isomorphic to the structure sheaf.

Equations

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

theorem AlgebraicGeometry.Proj.intShift_isCoherent {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)) = ⊤) : Scheme.Modules.IsCoherent (Proj 𝒜) (associatedSheaf 𝒜 (GradedModule.intShift 𝒜 d))

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

This is the hypothesis quasi-coherence already takes, unchanged.