structure RiemannRochGeometric.SmoothCurveWithCohomology (k : Type) [Field k] : Type 1

Axiomatic data for a smooth complete curve X over a field k, together with cohomology dimensions and the Riemann–Roch ingredients (rank, degree, arithmetic genus) needed for Thm 24.2 (Lec 24).

• X : AlgebraicGeometry.Scheme
• f : self.X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)
• isIntegral : AlgebraicGeometry.IsIntegral self.X
• isProper : AlgebraicGeometry.IsProper self.f
• isSmooth : AlgebraicGeometry.SmoothOfRelativeDimension 1 self.f
• dimH0 : self.X.Modules → ℕ
• dimH1 : self.X.Modules → ℕ
• degree : self.X.Modules → ℤ
• sheafRank : self.X.Modules → ℤ
• arithmeticGenus : ℕ
• chiK0 : ℤ × ℤ →+ ℤ
• chi_eq_chiK0 (F : self.X.Modules) : ↑(self.dimH0 F) - ↑(self.dimH1 F) = self.chiK0 (self.sheafRank F, self.degree F)
• chi_structureSheaf : self.chiK0 (1, 0) = 1 - ↑self.arithmeticGenus
• chi_skyscraper : self.chiK0 (0, 1) = 1

def RiemannRochGeometric.SmoothCurveWithCohomology.eulerChar {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) : ℤ

Euler characteristic χ(F) = h^0(F) - h^1(F) of a sheaf on a smooth complete curve.

noncomputable def RiemannRochGeometric.SmoothCurveWithCohomology.structureSheafMod {k : Type} [Field k] (C : SmoothCurveWithCohomology k) : C.X.Modules

The structure sheaf of a smooth complete curve, packaged as a module sheaf.

def RiemannRochGeometric.SmoothCurveWithCohomology.rrFormula {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (r d : ℤ) : ℤ

The Riemann–Roch formula evaluated on (r, d): d + r(1 - g).

theorem RiemannRochGeometric.additive_hom_determined (f : ℤ × ℤ →+ ℤ) (p : ℤ × ℤ) : f p = p.1 * f (1, 0) + p.2 * f (0, 1)

Any additive map ℤ × ℤ → ℤ is determined by its values on the generators (1, 0) and (0, 1).

theorem RiemannRochGeometric.theorem_24_2 {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) : C.eulerChar F = C.degree F + C.sheafRank F * (1 - ↑C.arithmeticGenus)

Theorem 24.2 (Riemann–Roch for curves, Lec 24): for any sheaf F, χ(F) = deg(F) + rank(F)·(1 - g_a).

theorem RiemannRochGeometric.theorem_24_2_alt {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) : C.eulerChar F = C.degree F - C.sheafRank F * (↑C.arithmeticGenus - 1)

Alternative form of Theorem 24.2: χ(F) = deg(F) - rank(F)·(g_a - 1).

theorem RiemannRochGeometric.theorem_24_2_rank_one {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) (hrank : C.sheafRank F = 1) : C.eulerChar F = C.degree F + 1 - ↑C.arithmeticGenus

Theorem 24.2 specialized to line bundles (rank 1): χ(L) = d + 1 - g.

theorem RiemannRochGeometric.theorem_24_2_torsion {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) (hrank : C.sheafRank F = 0) : C.eulerChar F = C.degree F

Theorem 24.2 for torsion (rank 0) sheaves: χ(F) = deg(F).

theorem RiemannRochGeometric.theorem_24_2_structure_sheaf {k : Type} [Field k] (C : SmoothCurveWithCohomology k) (F : C.X.Modules) (hrank : C.sheafRank F = 1) (hdeg : C.degree F = 0) : C.eulerChar F = 1 - ↑C.arithmeticGenus

Theorem 24.2 specialized to the structure sheaf: χ(𝒪_X) = 1 - g.