noncomputable def RiemannRochDedekind.h1_O (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℕ

H^1 of the structure sheaf for a Dedekind curve, repackaged at the top-level of this namespace.

theorem RiemannRochDedekind.h1_O_eq_genus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : h1_O k A = Module.finrank k Ω[A⁄k]

h^1(𝒪) = dim_k Ω_{A/k}, i.e. the arithmetic genus, for a Dedekind curve.

def RiemannRochDedekind.h1_sky (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℕ

H^1 of a skyscraper sheaf on a Dedekind curve, repackaged.

theorem RiemannRochDedekind.h1_sky_eq_zero (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : h1_sky k A = 0

The H^1 of a skyscraper sheaf vanishes.

theorem RiemannRochDedekind.dedekind_curve_rr {k : Type u_1} [Field k] (C : DedekindCurve k) (r d : ℤ) : C.toSmoothCompleteCurve.χ (r, d) = d - r * (↑C.ddGenus - 1)

Riemann–Roch for a Dedekind curve C (Dedekind-ring perspective): χ(r, d) = d - r(g - 1).