noncomputable def CoherentLineBundlesProj.IsCoherent {Y : AlgebraicGeometry.Scheme} (ℱ : Y.Modules) : Prop

Predicate asserting that a sheaf of modules ℱ on a scheme Y is coherent.

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

The Serre twisting sheaf O(d) on Proj 𝒜 for an integer d.

noncomputable def CoherentLineBundlesProj.FGGradedModule {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : Type u

The type of finitely generated graded modules over the graded ring 𝒜.

noncomputable def CoherentLineBundlesProj.tildeSheaf {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M : FGGradedModule 𝒜) : (AlgebraicGeometry.Proj 𝒜).Modules

The sheaf M̃ on Proj 𝒜 associated to a finitely generated graded module M.

theorem CoherentLineBundlesProj.prop20_coherent_from_fg_module {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hcoh : IsCoherent ℱ) : ∃ (M : FGGradedModule 𝒜), Nonempty (tildeSheaf 𝒜 M ≅ ℱ)

Every coherent sheaf on Proj 𝒜 arises (up to isomorphism) as M̃ for some finitely generated graded module M.

theorem CoherentLineBundlesProj.fg_module_line_bundle_surjection {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M : FGGradedModule 𝒜) : ∃ (d : ℕ) (r : ℕ) (φ : (∐ fun (x : Fin r) => twistingSheafProj 𝒜 (-↑d)) ⟶ tildeSheaf 𝒜 M), CategoryTheory.Epi φ

For any finitely generated graded module M, there exists a surjection from a finite direct sum of twisting sheaves O(-d) onto M̃.

theorem CoherentLineBundlesProj.serre_coherent_presentation {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hcoh : IsCoherent ℱ) : ∃ (d : ℕ) (r : ℕ) (φ : (∐ fun (x : Fin r) => twistingSheafProj 𝒜 (-↑d)) ⟶ ℱ), CategoryTheory.Epi φ

Serre's theorem: every coherent sheaf on Proj 𝒜 is a quotient of a finite direct sum of Serre twisting sheaves O(-d).