def SerreDualityCurves.residueMap (k : Type u_1) [Field k] : (ℤ →₀ k) →ₗ[k] k

The residue map (ℤ →₀ k) →ₗ[k] k sending a Laurent polynomial to its coefficient at index -1.

@[simp]

theorem SerreDualityCurves.residueMap_apply (k : Type u_1) [Field k] (f : ℤ →₀ k) : (residueMap k) f = f (-1)

Unfolds residueMap to the coefficient at index -1.

theorem SerreDualityCurves.residueMap_single_neg_one (k : Type u_1) [Field k] (a : k) : (residueMap k) (Finsupp.single (-1) a) = a

The residue of a single-term Laurent polynomial concentrated at index -1 is its coefficient.

theorem SerreDualityCurves.residueMap_single_ne (k : Type u_1) [Field k] (n : ℤ) (hn : n ≠ -1) (a : k) : (residueMap k) (Finsupp.single n a) = 0

Single-term Laurent polynomials concentrated at any index other than -1 have residue zero.

def SerreDualityCurves.derivCoeff (k : Type u_1) [Field k] (f : ℤ →₀ k) (m : ℤ) : k

Coefficient of the formal derivative: (d/dz f)(m) = (m+1) · f(m+1).

theorem SerreDualityCurves.derivCoeff_neg_one (k : Type u_1) [Field k] (f : ℤ →₀ k) : derivCoeff k f (-1) = 0

The (-1)-coefficient of a formal derivative vanishes (the prefactor 0 · f(0) is zero).

theorem SerreDualityCurves.residue_of_exact_zero (k : Type u_1) [Field k] (n : ℤ) (a : k) : (residueMap k) (Finsupp.single (n - 1) (↑n * a)) = 0

The residue of an exact differential d(a · z^n) = n · a · z^{n-1} vanishes.

theorem SerreDualityCurves.residue_annihilates_derivs (k : Type u_1) [Field k] (f : ℤ →₀ k) : derivCoeff k f (-1) = 0

The residue annihilates exact forms: formal derivatives have vanishing -1-coefficient.

def SerreDualityCurves.residuePairing (k : Type u_1) [Field k] (f g : ℤ →₀ k) : k

The residue pairing ⟨f, g⟩ = ∑ i f(i) · g(-1 - i), which extracts the -1-coefficient of the convolution product.

theorem SerreDualityCurves.residuePairing_single (k : Type u_1) [Field k] (i j : ℤ) (a b : k) : residuePairing k (Finsupp.single i a) (Finsupp.single j b) = if i + j = -1 then a * b else 0

The residue pairing on single-term Laurent polynomials: equals a · b when i + j = -1 and 0 otherwise.

theorem SerreDualityCurves.residuePairing_single_comm (k : Type u_1) [Field k] (i j : ℤ) (a b : k) : residuePairing k (Finsupp.single i a) (Finsupp.single j b) = residuePairing k (Finsupp.single j b) (Finsupp.single i a)

Symmetry of the residue pairing on single-term Laurent polynomials.

theorem SerreDualityCurves.serre_duality_chi_rank1 (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0

Rank-1 Euler-characteristic form of Serre duality on a smooth complete curve: χ(O(d)) + χ(O(K - d)) = 0.

theorem SerreDualityCurves.serre_duality_chi_O_K (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, 0) + C.χ (1, C.degK) = 0

Serre duality applied to O ↔ K: χ(O) + χ(K) = 0.

theorem SerreDualityCurves.serre_duality_chi_rank_r (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) + C.χ (r, r * C.degK - d) = 0

General rank-r Euler-characteristic form of Serre duality on a smooth complete curve: χ(E) + χ(E∨ ⊗ K) = 0 numerically.

theorem SerreDualityCurves.serre_duality_numerical_from_chi (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0E h1E h0EK h1EK : ℤ) (hRR_E : h0E - h1E = C.χ (1, d)) (hRR_EK : h0EK - h1EK = C.χ (1, C.degK - d)) (hSD : h0E = h1EK) : h1E = h0EK

Numerical Serre duality from the χ-identity: given Riemann–Roch and the duality h⁰(E) = h¹(E∨ ⊗ K), conclude h¹(E) = h⁰(E∨ ⊗ K).

structure SerreDualityCurves.LocallyFreeSheaf (C : CanonicalSheafCurves.SmoothCompleteCurve) : Type

Numerical model of a locally free sheaf on a curve C: tracks rank and degree.

• rk : ℕ
• deg : ℤ

theorem SerreDualityCurves.LocallyFreeSheaf.ext {C : CanonicalSheafCurves.SmoothCompleteCurve} {x y : LocallyFreeSheaf C} (rk : x.rk = y.rk) (deg : x.deg = y.deg) : x = y

theorem SerreDualityCurves.LocallyFreeSheaf.ext_iff {C : CanonicalSheafCurves.SmoothCompleteCurve} {x y : LocallyFreeSheaf C} : x = y ↔ x.rk = y.rk ∧ x.deg = y.deg

def SerreDualityCurves.LocallyFreeSheaf.K0class {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : ℤ × ℤ

The K-theory class of a locally free sheaf is the pair (rank, degree) ∈ ℤ × ℤ.

def SerreDualityCurves.LocallyFreeSheaf.chi {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : ℤ

The Euler characteristic χ(E) = h⁰(E) - h¹(E) of a locally free sheaf, computed from its rank and degree via Riemann–Roch.

def SerreDualityCurves.LocallyFreeSheaf.serreDual {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : LocallyFreeSheaf C

The Serre dual E∨ ⊗ K at the level of (rank, degree): same rank, degree replaced by rank · deg K − deg E.

theorem SerreDualityCurves.LocallyFreeSheaf.serreDual_deg {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : E.serreDual.deg = ↑E.rk * C.degK - E.deg

Unfolds the degree of the Serre dual.

theorem SerreDualityCurves.LocallyFreeSheaf.serre_duality_chi {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : E.chi + E.serreDual.chi = 0

Serre duality at the level of Euler characteristics: χ(E) + χ(E∨ ⊗ K) = 0.

theorem SerreDualityCurves.LocallyFreeSheaf.serreDual_serreDual {C : CanonicalSheafCurves.SmoothCompleteCurve} (E : LocallyFreeSheaf C) : E.serreDual.serreDual = E

Serre duality is an involution at the numerical level: (E∨ ⊗ K)∨ ⊗ K = E.

def SerreDualityCurves.LocallyFreeSheaf.ofIdeal (C : CanonicalSheafCurves.SmoothCompleteCurve) (deg : ℤ) : LocallyFreeSheaf C

The line bundle of a given degree.

def SerreDualityCurves.LocallyFreeSheaf.structureSheaf (C : CanonicalSheafCurves.SmoothCompleteCurve) : LocallyFreeSheaf C

The structure sheaf O_C as a locally free sheaf of rank 1 and degree 0.

def SerreDualityCurves.LocallyFreeSheaf.canonical (C : CanonicalSheafCurves.SmoothCompleteCurve) : LocallyFreeSheaf C

The canonical bundle K_C as a locally free sheaf of rank 1 and degree deg K.

def SerreDualityCurves.structureSheaf (C : CanonicalSheafCurves.SmoothCompleteCurve) : LocallyFreeSheaf C

Standalone alias for the structure sheaf of C.

def SerreDualityCurves.canonicalSheaf (C : CanonicalSheafCurves.SmoothCompleteCurve) : LocallyFreeSheaf C

Standalone alias for the canonical sheaf of C.

theorem SerreDualityCurves.structureSheaf_serreDual (C : CanonicalSheafCurves.SmoothCompleteCurve) : (structureSheaf C).serreDual = canonicalSheaf C

The Serre dual of O_C is K_C numerically.

theorem SerreDualityCurves.serre_duality_O_K (C : CanonicalSheafCurves.SmoothCompleteCurve) : (structureSheaf C).chi + (canonicalSheaf C).chi = 0

Serre duality for O ↔ K: χ(O) + χ(K) = 0.

theorem SerreDualityCurves.serre_duality_P1_dimension (k : Type) [Field k] (n : ℤ) : RiemannRoch.dimH1 k n = RiemannRoch.dimH0 k (-2 - n)

Serre duality on ℙ¹ at the level of dimensions: dim H¹(O(n)) = dim H⁰(O(-2 - n)).

def SerreDualityCurves.P1Curve : CanonicalSheafCurves.SmoothCompleteCurve

The projective line ℙ¹ as a smooth complete curve of genus 0.

theorem SerreDualityCurves.P1Curve_genus : P1Curve.g = 0

ℙ¹ has genus zero.

theorem SerreDualityCurves.P1Curve_degK : P1Curve.degK = -2

The degree of the canonical divisor on ℙ¹ is -2.

def SerreDualityCurves.O_P1 (n : ℤ) : LocallyFreeSheaf P1Curve

The line bundle O_{ℙ¹}(n) on ℙ¹ as a numerical locally free sheaf.

theorem SerreDualityCurves.O_P1_serreDual (n : ℤ) : (O_P1 n).serreDual = O_P1 (-2 - n)

The Serre dual of O_{ℙ¹}(n) is O_{ℙ¹}(-2 - n).

theorem SerreDualityCurves.chi_O_P1_duality (n : ℤ) : (O_P1 n).chi + (O_P1 (-2 - n)).chi = 0

Numerical Serre duality on ℙ¹: χ(O(n)) + χ(O(-2 - n)) = 0.

theorem SerreDualityCurves.chi_O_P1 (n : ℤ) : (O_P1 n).chi = n + 1

Riemann–Roch on ℙ¹: χ(O(n)) = n + 1.

theorem SerreDualityCurves.serre_duality_P1_via_shift (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Nonempty (((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) ≃ₗ[k] ↥(CohomologyP1.CechH0 k (-2 - n)))

Serre duality on ℙ¹ (nonempty version): for n < -1, the quotient (ℤ →₀ k) / (NonNeg ⊔ AtMost n) is linearly equivalent to CechH⁰(-2 - n).

theorem SerreDualityCurves.serre_duality_P1_finrank_eq (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Module.finrank k ((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) = Module.finrank k ↥(CohomologyP1.CechH0 k (-2 - n))

Serre duality on ℙ¹ at the dimension level: for n < -1, dim H¹(O(n)) = dim H⁰(O(-2 - n)).

theorem SerreDualityCurves.residuePairing_via_shift (k : Type u_1) [Field k] (i : ℤ) (a : k) (g : ℤ →₀ k) : residuePairing k (Finsupp.single i a) g = a * g (SerreDualityP1.residueShift i)

The residue pairing of a · z^i with g equals a · g(-1 - i).

theorem SerreDualityCurves.residue_shift_is_pairing_bijection (n : ℤ) : SerreDualityP1.residueShift '' Set.Icc 0 n = Set.Icc (-1 - n) (-1)

The shift i ↦ -1 - i sends [0, n] bijectively onto [-1 - n, -1], showing the pairing matches degrees of one side with degrees of the dual side.

theorem SerreDualityCurves.serre_duality_theorem (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0 ∧ C.χ (1, d) = d + 1 - C.g

The combined Serre duality and Riemann–Roch statement on a smooth complete curve: χ(O(d)) + χ(O(K - d)) = 0 and χ(O(d)) = d + 1 − g.

theorem SerreDualityCurves.genus_arithmetic_eq_geometric (C : CanonicalSheafCurves.SmoothCompleteCurve) (ga gm h0_O h1_O h0_K h1_K : ℤ) (_hh0_O : h0_O = 1) (hga : ga = h1_O) (hgm : gm = h0_K) (hRR_O : h0_O - h1_O = C.χ (1, 0)) (hRR_K : h0_K - h1_K = C.χ (1, C.degK)) (hSD : h0_O = h1_K) : ga = gm

Arithmetic genus equals geometric genus: combining Riemann–Roch for O and K with the Serre duality h⁰(O) = h¹(K) yields g_a = g_m.

theorem SerreDualityCurves.serre_duality_both_directions (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0_E h1_E h0_EK h1_EK : ℤ) (hRR_E : h0_E - h1_E = C.χ (1, d)) (hRR_EK : h0_EK - h1_EK = C.χ (1, C.degK - d)) (hSD_0 : h0_E = h1_EK) : h1_E = h0_EK

Numerical Serre duality, both directions: assuming h⁰(E) = h¹(E∨ ⊗ K) yields the reverse h¹(E) = h⁰(E∨ ⊗ K).

theorem SerreDualityCurves.riemann_roch_serre_form_general (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0_D h0_KD : ℤ) (hRR : h0_D - h0_KD = C.χ (1, d)) : h0_D - h0_KD = d + 1 - C.g

Riemann–Roch in Serre form: h⁰(D) − h⁰(K − D) = d + 1 − g.

theorem SerreDualityCurves.riemann_inequality_from_RR (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0 h1 : ℤ) (hh1_nn : h1 ≥ 0) (hRR : h0 - h1 = d + 1 - C.g) : h0 ≥ d + 1 - C.g

Riemann's inequality: h⁰(D) ≥ d + 1 − g, derived from Riemann–Roch and the non-negativity of h¹.

theorem SerreDualityCurves.deg_K_from_serre_duality (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK = 2 * C.g - 2

The degree of the canonical divisor is 2g - 2.

theorem SerreDualityCurves.serre_duality_chi_rank1_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) (d : ℤ) : C.toSmoothCompleteCurve.χ (1, d) + C.toSmoothCompleteCurve.χ (1, C.toSmoothCompleteCurve.degK - d) = 0

Rank-1 Serre duality χ-identity transported to a DedekindCurve.

theorem SerreDualityCurves.serre_duality_chi_rank_r_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) (r d : ℤ) : C.toSmoothCompleteCurve.χ (r, d) + C.toSmoothCompleteCurve.χ (r, r * C.toSmoothCompleteCurve.degK - d) = 0

Rank-r Serre duality χ-identity transported to a DedekindCurve.

theorem SerreDualityCurves.serre_duality_canonical_h0_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.χ (1, 0) + C.toSmoothCompleteCurve.χ (1, C.toSmoothCompleteCurve.degK) = 0

Serre duality for O ↔ K on a DedekindCurve.