theorem Theorem22_20.lemma_22_13_curve_level {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] {Ω : Type u_4} [AddCommGroup Ω] [Module F Ω] [Module k Ω] [IsScalarTower k F Ω] (divΩ : Ω → CurveDivisor C) (D : CurveDivisor C) (h_add : ∀ (ω₁ ω₂ : Ω), ω₁ + ω₂ ≠ 0 → ∀ (P : C), min ((divΩ ω₁) P) ((divΩ ω₂) P) ≤ (divΩ (ω₁ + ω₂)) P) (h_smul : ∀ (c : k) (ω : Ω), c • ω ≠ 0 → ∀ (P : C), (divΩ ω) P ≤ (divΩ (c • ω)) P) : ↑(Module.finrank k ↥(RiemannRochSpace.differentialSpaceD divΩ D h_add h_smul)) = RiemannRochSpace.indexOfSpeciality D

Curve-level reformulation of Lemma 22.13: the $k$-dimension of the differential space $\Omega(D)$ associated to a divisor $D$ equals the index of speciality $i(D)$.

noncomputable def Theorem22_20.duality_iso {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] {Ω : Type u_4} [AddCommGroup Ω] [Module F Ω] [Module k Ω] [IsScalarTower k F Ω] (divΩ : Ω → CurveDivisor C) (W D : CurveDivisor C) (ω₀ : Ω) (hω₀ : ω₀ ≠ 0) (hW_eq : W = divΩ ω₀) (h_add : ∀ (ω₁ ω₂ : Ω), ω₁ + ω₂ ≠ 0 → ∀ (P : C), min ((divΩ ω₁) P) ((divΩ ω₂) P) ≤ (divΩ (ω₁ + ω₂)) P) (h_smul : ∀ (c : k) (ω : Ω), c • ω ≠ 0 → ∀ (P : C), (divΩ ω) P ≤ (divΩ (c • ω)) P) (div_smul_F_eq : ∀ (f : F) (hf : f ≠ 0), divΩ (f • ω₀) = CurveWithOrd.principalDivisor (Units.mk0 f hf) + divΩ ω₀) (omega_one_dim : ∀ (ω' : Ω), ω' ≠ 0 → ∃ (f : F), f ≠ 0 ∧ ω' = f • ω₀) (smul_faithful : ∀ (f : F), f • ω₀ = 0 → f = 0) : ↥(RiemannRochSpace.riemannRochSpace (W - D)) ≃ₗ[k] ↥(RiemannRochSpace.differentialSpaceD divΩ D h_add h_smul)

Theorem 22.20 (Serre duality for curves). Given a nonzero differential $\omega_0$ with divisor $W = \mathrm{div}(\omega_0)$, the Riemann–Roch space $L(W - D)$ is naturally isomorphic as a $k$-vector space to the space of differentials $\Omega(D)$ regular at $D$.