@[reducible, inline]

abbrev QCohProjective.HomogCoordRing (k : Type u_1) [CommSemiring k] (n : ℕ) : Type u_1

Homogeneous coordinate ring k[X_0, …, X_n] of ℙ^n_k.

def QCohProjective.gradedComponent (k : Type u_1) [CommSemiring k] (n d : ℕ) : Submodule k (HomogCoordRing k n)

Degree-d homogeneous component of the homogeneous coordinate ring of ℙ^n_k.

noncomputable def QCohProjective.irrelevantIdeal (k : Type u_1) [CommSemiring k] (n : ℕ) : Ideal (HomogCoordRing k n)

The irrelevant ideal (X_0, …, X_n) of the homogeneous coordinate ring of ℙ^n_k.

structure QCohProjective.GradedModuleData (k : Type u_1) [Field k] (n : ℕ) : Type (max u_1 (u_2 + 1))

Abstract data of a graded module over the homogeneous coordinate ring of ℙ^n_k: an integer-indexed family of k-vector spaces with a graded multiplication action by homogeneous polynomials.

• component : ℤ → Type u_2
• instACG (d : ℤ) : AddCommGroup (self.component d)
• instMod (d : ℤ) : Module k (self.component d)
• gsmul (i : ℕ) (j : ℤ) : ↥(gradedComponent k n i) → self.component j → self.component (↑i + j)

def QCohProjective.GradedModuleData.twist {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d : ℤ) : GradedModuleData k n

Degree shift M ↦ M(d) of a graded module, corresponding to tensoring with the twist 𝒪(d) on ℙ^n_k.

theorem QCohProjective.twist_twist {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d₁ d₂ i : ℤ) : ((M.twist d₁).twist d₂).component i = M.component (i + d₂ + d₁)

Iterating the twist: (M(d₁))(d₂) agrees component-wise with the shift by d₁ + d₂.

theorem QCohProjective.twist_zero {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (i : ℤ) : (M.twist 0).component i = M.component i

The trivial twist M(0) agrees with M on every degree component.

theorem QCohProjective.twist_neg_cancel {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d i : ℤ) : ((M.twist d).twist (-d)).component i = M.component i

Twisting by d then by -d recovers the original module component-wise.

theorem QCohProjective.twist_add {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d₁ d₂ i : ℤ) : ((M.twist d₁).twist d₂).component i = (M.twist (d₁ + d₂)).component i

Successive twists add: (M(d₁))(d₂) ≅ M(d₁ + d₂) component-wise.

theorem QCohProjective.torsion_iff_killed {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] (m : M) : m ∈ Submodule.torsion R M ↔ ∃ (r : R), r ≠ 0 ∧ r • m = 0

Over a domain, m is torsion iff it is annihilated by some nonzero scalar.

theorem QCohProjective.torsion_module_iff_all_torsion {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] : (∀ (m : M), m ∈ Submodule.torsion R M) ↔ ∀ (m : M), ∃ (r : R), r ≠ 0 ∧ r • m = 0

Over a domain, a module is entirely torsion iff every element is annihilated by some nonzero scalar.

theorem QCohProjective.torsion_submodule_eq_set {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] : ↑(Submodule.torsion R M) = {m : M | ∃ (r : R), r ≠ 0 ∧ r • m = 0}

Set-level description of the torsion submodule over a domain.

theorem QCohProjective.serre_quotient_iso_criterion {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ((∀ (m : M), f m = 0 → m ∈ Submodule.torsion R M) ∧ ∀ (n : N), ∃ (r : R), r ≠ 0 ∧ r • n ∈ f.range) → (∀ (m : M), f m ∈ Submodule.torsion R N → m ∈ Submodule.torsion R M) ∧ ∀ (n : N), n ∈ Submodule.torsion R N ∨ ∃ (r : R), r ≠ 0 ∧ r • n ∈ f.range

Serre quotient criterion: a kernel-killing / cokernel-killing condition for a linear map f : M → N implies that f becomes an isomorphism after quotienting by torsion (mirrors the proof that graded modules and quasi-coherent sheaves on ℙ^n agree modulo torsion).

theorem QCohProjective.tilde_proj_exact {R : Type u_1} [CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (hex : Function.Exact ⇑f ⇑g) (S : Submonoid R) : Function.Exact ⇑((LocalizedModule.map S) f) ⇑((LocalizedModule.map S) g)

Exactness of localization for the tilde construction on Proj: applying S^{-1}(−) preserves exactness of a pair of consecutive maps.

theorem QCohProjective.shiftedModule_degree_zero_eq (k : Type u_1) [Field k] {n : ℕ} (M : GradedModuleData k n) (d : ℤ) : (M.twist d).component 0 = M.component d

Degree-0 component of the shift M(d) equals the degree-d component of M, the basic identity behind Γ(ℙ^n, 𝒪(d)) = S_d.

theorem QCohProjective.globalSections_Od_finrank (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d) = (n + d).choose n

Dimension formula dim_k Γ(ℙ^n, 𝒪(d)) = (n+d choose n) for the degree-d homogeneous component of k[X_0, …, X_n].

theorem QCohProjective.homogeneous_component_finiteDim (k : Type u_1) [Field k] (n d : ℕ) : Module.Finite k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d)

The degree-d homogeneous component of a polynomial ring in finitely many variables is finite-dimensional over the base.

theorem QCohProjective.surjective_mapQ {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (p : Submodule R M) (q : Submodule R N) (hpq : p ≤ Submodule.comap f q) : Function.Surjective ⇑(p.mapQ q f hpq)

Surjectivity is preserved by Submodule.mapQ: a surjection on the ambient modules descends to a surjection on the quotients.

theorem QCohProjective.localization_preserves_surjectivity {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) {P : Type u_4} [AddCommGroup P] [Module R P] (g : N →ₗ[R] P) (hg : Function.Surjective ⇑g) : Function.Surjective ⇑(g ∘ₗ f)

The composition of two surjective linear maps is surjective.

theorem QCohProjective.fg_module_quotient_of_free (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f

Every finitely generated module admits a surjection from a finite-rank free module R^n (a basic presentation result used to test quasi-coherence).

theorem QCohProjective.torsion_killed_by_localization {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] (S : Submonoid R) (m : M) (hm : m ∈ Submodule.torsion R M) (hS : nonZeroDivisors R ≤ S) : ∃ (t : ↥S), ↑t • m = 0

Torsion elements are killed by localization at any submonoid containing the nonzero divisors: a torsion m admits an s ∈ S with s • m = 0.

theorem QCohProjective.torsion_module_localization_trivial {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] (htors : ∀ (m : M), m ∈ Submodule.torsion R M) (m : M) : ∃ (r : R), r ≠ 0 ∧ r • m = 0

For a totally torsion module over a domain, every element is annihilated by a nonzero scalar.

theorem QCohProjective.double_twist_eq_twist_add {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d₁ d₂ i : ℤ) : ((M.twist d₁).twist d₂).component i = (M.twist (d₁ + d₂)).component i

Component-wise additivity of twists: M(d₁)(d₂) and M(d₁ + d₂) agree on every degree component.

@[deprecated QCohProjective.double_twist_eq_twist_add (since := "2025-01-01")]

theorem QCohProjective.twist_tensor_product_correspondence {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d₁ d₂ i : ℤ) : ((M.twist d₁).twist d₂).component i = (M.twist (d₁ + d₂)).component i

Deprecated alias for double_twist_eq_twist_add, formerly motivated by the tensor product identity 𝒪(d₁) ⊗ 𝒪(d₂) ≅ 𝒪(d₁ + d₂).

theorem QCohProjective.twist_zero_structure_sheaf {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (i : ℤ) : (M.twist 0).component i = M.component i

The zero twist is the identity on every degree component.

theorem QCohProjective.globalSections_twisted_structure_sheaf {k : Type u_1} [Field k] {n : ℕ} (M : GradedModuleData k n) (d : ℤ) : (M.twist d).component 0 = M.component d

Γ(ℙ^n, 𝒪(d)) = S_d: degree-zero of the shifted module recovers the degree-d piece (graded analog of global sections of a twisted structure sheaf).

theorem QCohProjective.globalSections_Od_dimension (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(gradedComponent k n d) = (n + d).choose n

Dimension formula for Γ(ℙ^n, 𝒪(d)), packaged via the gradedComponent abbreviation.

theorem QCohProjective.hilbert_function_via_Od (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(gradedComponent k n d) = (n + d).choose d

The Hilbert function of the homogeneous coordinate ring of ℙ^n equals binom(n+d, d), recovered from Γ(ℙ^n, 𝒪(d)) via Pascal's symmetry.

theorem QCohProjective.gradedComponent_mono (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(gradedComponent k n d) ≤ Module.finrank k ↥(gradedComponent k n (d + 1))

The dimensions of the graded components of k[X_0, …, X_n] are nondecreasing in degree.