noncomputable def twistingSheaf {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d : ℤ) : (AlgebraicGeometry.Proj 𝒜).Modules

The Serre twisting sheaf O(d) on Proj 𝒜, defined as the tilde of the shifted graded module R(d).

theorem twistingSheaf_eq_tildeProj_shift {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d : ℤ) : twistingSheaf 𝒜 d = tildeProj 𝒜 (GrMod.shift 𝒜 d)

Unfolding lemma: O(d) is by definition the tilde of the shifted module R(d).

noncomputable def IsLocallyFreeRank {X : AlgebraicGeometry.Scheme} : X.Modules → ℕ → Prop

Predicate: a sheaf of O_X-modules is locally free of rank n.

def IsLineBundle {X : AlgebraicGeometry.Scheme} (ℱ : X.Modules) : Prop

A line bundle is a locally free sheaf of rank one.

theorem twistingSheaf_isLineBundle {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d : ℤ) : IsLineBundle (twistingSheaf 𝒜 d)

Each twisting sheaf O(d) on Proj 𝒜 is a line bundle (locally free of rank one).

def degreePiece {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) (d : ℕ) : AddSubgroup A

The degree-d graded piece of A packaged as an additive subgroup.

theorem globalSections_twistingSheaf {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d : ℕ) : ∃ (f : ↥(degreePiece 𝒜 d) →+ ↑((twistingSheaf 𝒜 ↑d).val.obj (Opposite.op ⊤))), Function.Bijective ⇑f

Global sections of O(d) on Proj 𝒜 are in bijection with the degree-d graded piece of 𝒜.

theorem cor18_coherent_quotient_of_twistingSheaf {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hcoh : IsCoherentSheaf ℱ) : ∃ (d : ℕ) (k : ℕ) (φ : tildeProj 𝒜 ((GrMod.shift 𝒜 (-↑d)).directSumCopies k) ⟶ ℱ), CategoryTheory.Epi φ

Corollary 18: every coherent sheaf on Proj 𝒜 is a quotient of a finite direct sum of twists O(-d)^k of the structure sheaf.