structure SerreDualityStatement.SmoothCompleteCurveVS (k : Type u) [Field k] : Type (u + 1)

Abstract vector-space-level model of a smooth complete curve over k: locally free sheaves with finite-dimensional global sections and H¹, together with a Serre dual involution and distinguished O_X, K_X.

• LocallyFreeSheaf : Type u
• globalSections : self.LocallyFreeSheaf → Type u
• globalSections_addCommGroup (E : self.LocallyFreeSheaf) : AddCommGroup (self.globalSections E)
• globalSections_module (E : self.LocallyFreeSheaf) : Module k (self.globalSections E)
• globalSections_finiteDimensional (E : self.LocallyFreeSheaf) : Module.Finite k (self.globalSections E)
• H1 : self.LocallyFreeSheaf → Type u
• H1_addCommGroup (E : self.LocallyFreeSheaf) : AddCommGroup (self.H1 E)
• H1_module (E : self.LocallyFreeSheaf) : Module k (self.H1 E)
• H1_finiteDimensional (E : self.LocallyFreeSheaf) : Module.Finite k (self.H1 E)
• serreDual : self.LocallyFreeSheaf → self.LocallyFreeSheaf
• canonicalSheaf : self.LocallyFreeSheaf
• structureSheaf : self.LocallyFreeSheaf
• serreDual_globalSections_equiv (E : self.LocallyFreeSheaf) : self.globalSections (self.serreDual (self.serreDual E)) ≃ₗ[k] self.globalSections E
• serreDual_H1_equiv (E : self.LocallyFreeSheaf) : self.H1 (self.serreDual (self.serreDual E)) ≃ₗ[k] self.H1 E

noncomputable def SerreDualityStatement.serre_duality_iso {k : Type u} [Field k] (X : SmoothCompleteCurveVS k) (E : X.LocallyFreeSheaf) : Module.Dual k (X.globalSections E) ≃ₗ[k] X.H1 (X.serreDual E)

Serre duality (Thm 24.3): for a locally free sheaf E on a complete smooth irreducible curve, the canonical isomorphism Γ(E)* ≅ H¹(E∨ ⊗ K_X).

theorem SerreDualityStatement.serre_duality_finrank_general {k : Type u} [Field k] (X : SmoothCompleteCurveVS k) (E : X.LocallyFreeSheaf) : Module.finrank k (X.globalSections E) = Module.finrank k (X.H1 (X.serreDual E))

Serre duality at the dimension level: dim Γ(E) = dim H¹(E∨ ⊗ K_X).

theorem SerreDualityStatement.serre_duality_reverse_finrank_general {k : Type u} [Field k] (X : SmoothCompleteCurveVS k) (E : X.LocallyFreeSheaf) : Module.finrank k (X.H1 E) = Module.finrank k (X.globalSections (X.serreDual E))

Reverse direction of Serre duality: dim H¹(E) = dim Γ(E∨ ⊗ K_X), obtained by applying the forward statement to E∨ ⊗ K_X and using the involution.