structure DedekindCurve (k : Type u_1) [Field k] : Type (max u_1 (u_2 + 1))

A Dedekind curve over a field k: the data of a finite k-algebra A which is a Dedekind domain. Models a smooth affine curve over k.

• A : Type u_2
• instCR : CommRing self.A
• instID : IsDomain self.A
• instDD : IsDedekindDomain self.A
• instAlg : Algebra k self.A
• instFin : Module.Finite k self.A

noncomputable def DedekindCurve.ddGenus {k : Type u_1} [Field k] (C : DedekindCurve k) : ℕ

The genus of a Dedekind curve, defined as the k-dimension of its global Kähler differentials Ω[A⁄k].

noncomputable def DedekindCurve.curveIdealDeg {k : Type u_1} [Field k] (C : DedekindCurve k) (I : Ideal C.A) : ℕ

Degree of an ideal I on a Dedekind curve C, measured as dim_k (A/I).

noncomputable def DedekindCurve.curveModuleRk {k : Type u_1} [Field k] (C : DedekindCurve k) (M : Type u_2) [AddCommGroup M] [Module C.A M] : ℕ

The generic rank of an A-module M on the curve C, defined as the dimension of its localization at the generic point.

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

The Euler characteristic of the structure sheaf of a Dedekind curve: χ(O_X) = 1 - g.

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

The degree of the canonical divisor on a Dedekind curve: deg K = 2g - 2.

noncomputable def DedekindCurve.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¹(O_X) for a Dedekind curve, defined via dim_k Ω[A⁄k] using Serre duality.

theorem DedekindCurve.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¹(O_X) agrees by definition with dim_k Ω[A⁄k] (the genus).

def DedekindCurve.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¹ of a skyscraper sheaf on a Dedekind curve vanishes (by dimension); modeled as 0.

theorem DedekindCurve.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

h¹ of a skyscraper is zero, by definition.

noncomputable def DedekindCurve.cohChi {k : Type u_1} [Field k] (C : DedekindCurve k) : ℤ × ℤ →+ ℤ

The additive Euler-characteristic homomorphism on the K-theory generators (rank, degree), sending (r, d) to r·χ(O_X) + d·χ(sky).

theorem DedekindCurve.cohChi_struct {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi (1, 0) = 1 - ↑(h1_O k C.A)

Value of cohChi on the generator (1, 0) (the structure sheaf class).

theorem DedekindCurve.cohChi_sky {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi (0, 1) = 1 - ↑(h1_sky k C.A)

Value of cohChi on the skyscraper generator (0, 1).

theorem DedekindCurve.cohChi_struct_eq {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi (1, 0) = 1 - ↑C.ddGenus

Rewritten value of cohChi on (1, 0), expressed via the genus g.

theorem DedekindCurve.cohChi_sky_eq {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi (0, 1) = 1

The skyscraper generator contributes 1 to the Euler characteristic.

theorem DedekindCurve.cohChi_eq_rrHom {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi = RiemannRochCurves.rrHom ↑C.ddGenus

The Euler-characteristic homomorphism cohChi agrees with the Riemann–Roch homomorphism rrHom g parametrized by the genus.

theorem DedekindCurve.eulerCharO_eq {k : Type u_1} [Field k] (C : DedekindCurve k) : C.eulerCharO = 1 - ↑C.ddGenus

Definitional unfolding of eulerCharO: χ(O_X) = 1 - g.

theorem DedekindCurve.degK_eq_2g_sub_2 {k : Type u_1} [Field k] (C : DedekindCurve k) : C.degK = 2 * ↑C.ddGenus - 2

Definitional unfolding of degK: deg K = 2g - 2.

noncomputable def DedekindCurve.toSmoothCompleteCurve {k : Type u_1} [Field k] (C : DedekindCurve k) : CanonicalSheafCurves.SmoothCompleteCurve

Repackage a Dedekind curve as an abstract SmoothCompleteCurve carrying genus, Euler characteristic, and canonical degree.

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

Riemann–Roch on the smooth complete curve associated to C: χ(E) = deg E - rk E · (g - 1).

noncomputable def DedekindCurve.h1_O_sheaf (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℕ

Sheaf-level h¹(O_X) for a Dedekind curve, again defined via dim_k Ω[A⁄k].

theorem DedekindCurve.h1_O_sheaf_eq_genus (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : h1_O_sheaf k A = Module.finrank k Ω[A⁄k]

h1_O_sheaf agrees with the Kähler-differential dimension defining the genus.

noncomputable def DedekindCurve.eulerCharO_sheaf (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℤ

Sheaf-level Euler characteristic of O_X for a Dedekind curve: 1 - g.

theorem DedekindCurve.eulerCharO_sheaf_eq_formula (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : eulerCharO_sheaf k A = 1 - ↑(Module.finrank k Ω[A⁄k])

Definitional equality showing eulerCharO_sheaf k A = 1 - dim_k Ω[A⁄k].

noncomputable def DedekindCurve.degK_sheaf (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℤ

Sheaf-level degree of the canonical divisor of a Dedekind curve: 2g - 2.

theorem DedekindCurve.degK_sheaf_eq_formula (k : Type u_2) [Field k] (A : Type u_3) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : degK_sheaf k A = 2 * ↑(Module.finrank k Ω[A⁄k]) - 2

Definitional equality showing degK_sheaf k A = 2 · dim_k Ω[A⁄k] - 2.