@[implicit_reducible]

noncomputable instance TwistSheaf.mvPolyModule (k : Type u_1) [Field k] (n : ℕ) : Module k (MvPolynomial (Fin (n + 1)) k)

The k-module structure on the multivariate polynomial ring k[X₀,…,Xₙ].

noncomputable def TwistSheaf.polyGrSub (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) : Submodule k (QCohProjective.HomogCoordRing k n)

The k-submodule of polynomials of homogeneous degree d, defined for all integers d by setting it to ⊥ for d < 0.

@[reducible, inline]

abbrev TwistSheaf.polyGrComp (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) : Type u_1

The degree-d graded component as a type.

theorem TwistSheaf.polyGrSub_nonneg (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) (hd : 0 ≤ d) : polyGrSub k n d = MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d.toNat

For d ≥ 0, the degree-d graded piece agrees with the usual homogeneous submodule of degree d.toNat.

theorem TwistSheaf.polyGrSub_neg (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) (hd : d < 0) : polyGrSub k n d = ⊥

For d < 0, the degree-d graded piece is trivial.

theorem TwistSheaf.polyGrComp_nat (k : Type u_1) [Field k] (n d : ℕ) : polyGrComp k n ↑d = ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)

Identifies the integer-indexed graded component at a natural number d with the standard nat-indexed homogeneous submodule.

noncomputable def TwistSheaf.polyGsmul (k : Type u_1) [Field k] (n i : ℕ) (j : ℤ) : ↥(QCohProjective.gradedComponent k n i) → polyGrComp k n j → polyGrComp k n (↑i + j)

Graded multiplication: multiplying a degree-i homogeneous polynomial with a degree-j graded element gives a degree-(i+j) graded element.

noncomputable def TwistSheaf.structureSheafData (k : Type u_1) [Field k] (n : ℕ) : QCohProjective.GradedModuleData k n

Graded-module data realizing the structure sheaf of P^n as the trivial shift: the graded pieces are the homogeneous components of k[X₀,…,Xₙ].

noncomputable def TwistSheaf.serreTwist (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) : QCohProjective.GradedModuleData k n

The Serre twist O(d) on P^n, expressed as the graded-module data obtained by shifting the structure sheaf by d.

theorem TwistSheaf.serreTwist_zero_component (k : Type u_1) [Field k] (n : ℕ) (i : ℤ) : (serreTwist k n 0).component i = (structureSheafData k n).component i

O(0) recovers the structure sheaf component-wise.

theorem TwistSheaf.serreTwist_double (k : Type u_1) [Field k] (n : ℕ) (d₁ d₂ i : ℤ) : ((serreTwist k n d₁).twist d₂).component i = (serreTwist k n (d₁ + d₂)).component i

Tensor product of twists: O(d₁) ⊗ O(d₂) = O(d₁ + d₂) at the level of graded components.

theorem TwistSheaf.serreTwist_neg_cancel (k : Type u_1) [Field k] (n : ℕ) (d i : ℤ) : ((serreTwist k n d).twist (-d)).component i = (structureSheafData k n).component i

Inverse twist: O(d) ⊗ O(-d) = O, witnessing that O(d) is invertible in the Picard group.

theorem TwistSheaf.globalSections_serreTwist (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) : (serreTwist k n d).component 0 = (structureSheafData k n).component d

Global sections of O(d): the degree-0 graded piece of O(d) equals the degree-d piece of the structure sheaf.

theorem TwistSheaf.globalSections_serreTwist_eq (k : Type u_1) [Field k] (n d : ℕ) : (serreTwist k n ↑d).component 0 = ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)

Global sections of O(d) for d ≥ 0 are the homogeneous degree-d polynomials in k[X₀,…,Xₙ].

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

dim_k H⁰(P^n, O(d)) = C(n+d, n): the dimension formula for global sections of O(d).

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

Symmetric form: dim_k H⁰(P^n, O(d)) = C(n+d, d).

theorem TwistSheaf.globalSections_O0_finrank (k : Type u_1) [Field k] (n : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k 0) = 1

H⁰(P^n, O) = k: the structure sheaf has one-dimensional global sections.

theorem TwistSheaf.globalSections_O1_finrank (k : Type u_1) [Field k] (n : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k 1) = n + 1

H⁰(P^n, O(1)) has dimension n + 1, matching the linear forms in n + 1 variables.

theorem TwistSheaf.twist_shift_add (k : Type u_1) [Field k] (n : ℕ) (d₁ d₂ i : ℤ) : (serreTwist k n (d₁ + d₂)).component i = ((serreTwist k n d₁).twist d₂).component i

Addition formula for twists: O(d₁ + d₂) = O(d₁) ⊗ O(d₂) component-wise.

@[deprecated TwistSheaf.twist_shift_add (since := "2025-01-01")]

theorem TwistSheaf.picard_group_twist (k : Type u_1) [Field k] (n : ℕ) (d₁ d₂ i : ℤ) : (serreTwist k n (d₁ + d₂)).component i = ((serreTwist k n d₁).twist d₂).component i

Deprecated alias witnessing Picard-group additivity of twists; use twist_shift_add instead.

theorem TwistSheaf.globalSections_mono (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d) ≤ Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k (d + 1))

Monotonicity of global sections: dim H⁰(P^n, O(d)) is nondecreasing in d.

theorem TwistSheaf.globalSections_negative_trivial (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) (hd : d < 0) : polyGrSub k n d = ⊥

Negative twists have no nonzero global sections at the polynomial level.