24.6. SerrePairing.SerreDualityPairing🔗

Jacobians.SerrePairing.SerreDualityPairing — source

SerreDualityData

The Forster §17 instantiation (the geometric data of Serre duality on X): a canonical divisor K with lDim K = genus (17.4 at D=0: 𝒪_K ≅ Ω), and the residue pairing ι_D : L(K−D) → (H¹(𝒪_D))* which is bijective (17.6 injective + 17.9 surjective), with H¹ finite.

structure SerreDualityData (𝔘 : FiniteCover X) where

serre_eq

Forster 17.11 — the Serre duality dimension equality. dim H¹(X,𝒪_D) = dim H⁰(X,𝒪_{K−D}), i.e. h1Dim D = lDim (K − D). The pairing ι_D is bijective, so L(K−D) ≃ (H¹(𝒪_D))*, and the dual of a finite-dimensional space has equal dimension.

theorem serre_eq (data : SerreDualityData 𝔘) (D : Divisor X) :
    𝔘.h1Dim D = lDim (X := X) (data.K - D)

lDim_le_h1Dim

The ≤ half wired through the 17.6 core (finrank_le_of_injective_to_dual): injectivity of the pairing gives lDim (K−D) ≤ h1Dim D. (Recorded separately to exhibit the core wiring; subsumed by serre_eq.)

theorem lDim_le_h1Dim (data : SerreDualityData 𝔘) (D : Divisor X) :
    lDim (X := X) (data.K - D) ≤ 𝔘.h1Dim D

arithmeticGenus

Forster 17.10 at D = 0 — arithmeticGenus_eq_genus. h1Dim 0 = genus X.

theorem arithmeticGenus (data : SerreDualityData 𝔘) : 𝔘.h1Dim 0 = genus X

serreH1

General Serre duality serre_h1_eq from the data: a single canonical K works for all D.

theorem serreH1 (data : SerreDualityData 𝔘) :
    ∃ K : Divisor X, ∀ D : Divisor X, 𝔘.h1Dim D = lDim (X := X) (K - D)