structure ProjectiveQCohProperties.ZGradedModule {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] (𝒜 : ℕ → σ) : Type (u + 1)

A ℤ-graded module over a ℕ-graded ring 𝒜: an A-module with a ℤ-indexed internal direct sum decomposition compatible with the grading on 𝒜.

• carrier : Type u
• instAddCommGroup : AddCommGroup self.carrier
• instModule : Module A self.carrier
• component : ℤ → AddSubgroup self.carrier
• isInternal : DirectSum.IsInternal self.component
• graded_smul (n : ℕ) (d : ℤ) (a : A) (m : self.carrier) : a ∈ ↑(𝒜 n) → m ∈ self.component d → a • m ∈ self.component (↑n + d)

def ProjectiveQCohProperties.ZGradedModule.IsFG {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] {𝒜 : ℕ → σ} (M : ZGradedModule 𝒜) : Prop

A graded module is finitely generated if its underlying module is.

def ProjectiveQCohProperties.ZGradedModule.IsFinDim {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] {𝒜 : ℕ → σ} (M : ZGradedModule 𝒜) : Prop

A graded module is "finite-dimensional" if only finitely many graded components are nonzero.

def ProjectiveQCohProperties.ZGradedModule.IsLocNilpotent {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (M : ZGradedModule 𝒜) : Prop

A graded module is locally nilpotent (with respect to the irrelevant ideal) if for every element x, some power of every element of the irrelevant ideal annihilates x.

structure ProjectiveQCohProperties.ZGradedModule.SES {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] {𝒜 : ℕ → σ} (M₁ M₂ M₃ : ZGradedModule 𝒜) : Type u

A short exact sequence 0 → M₁ → M₂ → M₃ → 0 of graded modules.

• f : M₁.carrier →ₗ[A] M₂.carrier
• g : M₂.carrier →ₗ[A] M₃.carrier
• f_injective : Function.Injective ⇑self.f
• g_surjective : Function.Surjective ⇑self.g
• exact : self.g.ker = self.f.range

noncomputable def ProjectiveQCohProperties.ZGradedModule.gradeShift {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d : ℤ) : ZGradedModule 𝒜

The grading shift A(d): A viewed as a graded module with degrees shifted by d.

noncomputable def ProjectiveQCohProperties.ZGradedModule.copies {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (M : ZGradedModule 𝒜) (k : ℕ) : ZGradedModule 𝒜

The direct sum of k copies of a graded module M.

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

Predicate that a sheaf of modules on a scheme is quasicoherent.

noncomputable def ProjectiveQCohProperties.CoherentSheafPred {X : AlgebraicGeometry.Scheme} : X.Modules → Prop

Placeholder predicate "is coherent" for a sheaf of modules on a scheme.

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

The "tilde" construction sending a graded 𝒜-module to the associated quasicoherent sheaf on Proj 𝒜.

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

The Serre twisting sheaf 𝒪(d) on Proj 𝒜.

noncomputable def ProjectiveQCohProperties.tilde_shifted_copies_iso_coproduct_twisting {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (d k : ℕ) : tildeProjFunctor 𝒜 ((ZGradedModule.gradeShift 𝒜 (-↑d)).copies k) ≅ ∐ fun (x : Fin k) => twistingSheaf 𝒜 (-↑d)

The tilde of k copies of the shifted graded ring A(-d) is canonically isomorphic to a coproduct of k copies of 𝒪(-d).

noncomputable def ProjectiveQCohProperties.gradedModuleOfSheaf {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) : ZGradedModule 𝒜

Recovers a graded module from a sheaf on Proj 𝒜 by taking the direct sum of twisted global sections ⊕ Γ(F(n)).

theorem ProjectiveQCohProperties.prop20_tildeFunctor_exact {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M₁ M₂ M₃ : ZGradedModule 𝒜) (ses : M₁.SES M₂ M₃) : ∃ (f : tildeProjFunctor 𝒜 M₁ ⟶ tildeProjFunctor 𝒜 M₂) (g : tildeProjFunctor 𝒜 M₂ ⟶ tildeProjFunctor 𝒜 M₃) (w : CategoryTheory.CategoryStruct.comp f g = 0), { X₁ := tildeProjFunctor 𝒜 M₁, X₂ := tildeProjFunctor 𝒜 M₂, X₃ := tildeProjFunctor 𝒜 M₃, f := f, g := g, zero := w }.ShortExact

Proposition 20 (exactness): the M ↦ M̃ functor sends short exact sequences of graded modules to short exact sequences of sheaves on Proj 𝒜.

theorem ProjectiveQCohProperties.prop20_tildeFunctor_essentiallySurjective {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hqc : IsQCoh ℱ) : ∃ (M : ZGradedModule 𝒜), Nonempty (tildeProjFunctor 𝒜 M ≅ ℱ)

Proposition 20 (essential surjectivity): every quasicoherent sheaf on Proj 𝒜 is isomorphic to M̃ for some graded module M.

theorem ProjectiveQCohProperties.prop20_tildeFunctor_essentiallySurjective_fg {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hcoh : CoherentSheafPred ℱ) : ∃ (M : ZGradedModule 𝒜), M.IsFG ∧ Nonempty (tildeProjFunctor 𝒜 M ≅ ℱ)

Refinement of Proposition 20: every coherent sheaf on Proj 𝒜 comes from a finitely generated graded module.

theorem ProjectiveQCohProperties.fg_graded_surjection_from_shifted_free {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M : ZGradedModule 𝒜) (hfg : M.IsFG) : ∃ (d : ℕ) (k : ℕ) (f : ((ZGradedModule.gradeShift 𝒜 (-↑d)).copies k).carrier →ₗ[A] M.carrier), Function.Surjective ⇑f

Every finitely generated graded module is a quotient of a finite direct sum of shifted copies of the graded ring A(-d).

theorem ProjectiveQCohProperties.tildeProjFunctor_epi_of_surjection {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M N : ZGradedModule 𝒜) (f : M.carrier →ₗ[A] N.carrier) (hf : Function.Surjective ⇑f) : ∃ (φ : tildeProjFunctor 𝒜 M ⟶ tildeProjFunctor 𝒜 N), CategoryTheory.Epi φ

A surjection of graded modules induces an epimorphism between their tilde sheaves.

theorem ProjectiveQCohProperties.cor18_coherent_quotient_module_level {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules) (hcoh : CoherentSheafPred ℱ) : ∃ (d : ℕ) (k : ℕ) (φ : tildeProjFunctor 𝒜 ((ZGradedModule.gradeShift 𝒜 (-↑d)).copies k) ⟶ ℱ), CategoryTheory.Epi φ

Corollary 18 (module-level): every coherent sheaf on Proj 𝒜 admits a surjection from the tilde of k copies of A(-d).

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

Corollary 18: every coherent sheaf on Proj 𝒜 is a quotient of a coproduct of twisting sheaves 𝒪(-d), i.e. a quotient of a vector bundle.

theorem ProjectiveQCohProperties.prop21_tilde_zero_iff_locNilpotent {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M : ZGradedModule 𝒜) : CategoryTheory.Limits.IsZero (tildeProjFunctor 𝒜 M) ↔ M.IsLocNilpotent

Proposition 21: M̃ = 0 on Proj 𝒜 iff M is locally nilpotent with respect to the irrelevant ideal.

theorem ProjectiveQCohProperties.prop21_tilde_zero_iff_finDim {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (M : ZGradedModule 𝒜) (hfg : M.IsFG) : CategoryTheory.Limits.IsZero (tildeProjFunctor 𝒜 M) ↔ M.IsFinDim

Proposition 21 for finitely generated modules: M̃ = 0 iff M has finite total dimension as a graded module.

theorem ProjectiveQCohProperties.prop21_serre_correspondence {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : (∀ (ℱ : (AlgebraicGeometry.Proj 𝒜).Modules), IsQCoh ℱ → ∃ (M : ZGradedModule 𝒜), Nonempty (tildeProjFunctor 𝒜 M ≅ ℱ)) ∧ (∀ (M : ZGradedModule 𝒜), CategoryTheory.Limits.IsZero (tildeProjFunctor 𝒜 M) ↔ M.IsLocNilpotent) ∧ ∀ (M : ZGradedModule 𝒜), M.IsFG → (CategoryTheory.Limits.IsZero (tildeProjFunctor 𝒜 M) ↔ M.IsFinDim)

Proposition 21 (Serre correspondence): QCoh(Proj 𝒜) is equivalent to the category of graded 𝒜-modules modulo locally nilpotent modules.