noncomputable def CanonicalDivisorCurves.canonicalDivisorClass_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : ℤ × ℤ

Canonical divisor class of a Dedekind curve C: the class of its canonical sheaf in the Picard-group representation ℤ × ℤ (rank, degree).

theorem CanonicalDivisorCurves.canonical_degree_eq_2g_minus_2_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.degK = 2 * C.toSmoothCompleteCurve.g - 2

For a Dedekind curve C, the canonical degree equals 2g - 2.

theorem CanonicalDivisorCurves.canonical_chi_eq_g_minus_1_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.χ (1, C.toSmoothCompleteCurve.degK) = C.toSmoothCompleteCurve.g - 1

Serre duality consequence: χ(K) = g - 1 for a Dedekind curve.

theorem CanonicalDivisorCurves.structure_chi_eq_1_minus_g_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.χ (1, 0) = 1 - C.toSmoothCompleteCurve.g

The Euler characteristic of the structure sheaf of a Dedekind curve is 1 - g.

theorem CanonicalDivisorCurves.serre_duality_chi_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.χ (1, 0) + C.toSmoothCompleteCurve.χ (1, C.toSmoothCompleteCurve.degK) = 0

Serre duality in characteristic form: χ(O) + χ(K) = 0.

theorem CanonicalDivisorCurves.rr_formula_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) (r d : ℤ) : C.toSmoothCompleteCurve.χ (r, d) = d - r * (C.toSmoothCompleteCurve.g - 1)

Riemann-Roch formula for a Dedekind curve: χ(r, d) = d - r(g - 1).

theorem CanonicalDivisorCurves.toSCC_degK_eq_dedekind_degK {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.degK = C.degK

The canonical degree from the underlying SmoothCompleteCurve agrees with the Dedekind canonical degree.

theorem CanonicalDivisorCurves.toSCC_g_eq_ddGenus {k : Type u_1} [Field k] (C : DedekindCurve k) : C.toSmoothCompleteCurve.g = ↑C.ddGenus

The genus from the underlying SmoothCompleteCurve agrees with the Dedekind genus.