noncomputable def CurveGenusGeometric.geometricGenus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : ℕ

The geometric genus g_m of a curve over k, defined as the k-dimension of the global sections of the canonical sheaf, modeled here as Ω[A⁄k].

noncomputable def CurveGenusGeometric.arithmeticGenus (k : Type u_1) [Field k] (H1_O : Type u_3) [AddCommGroup H1_O] [Module k H1_O] : ℕ

The arithmetic genus of a curve, defined as the k-dimension of H¹(O_X).

theorem CurveGenusGeometric.cor29_arithmetic_eq_geometric_genus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (H1_O : Type u_3) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[A⁄k]) : arithmeticGenus k H1_O = geometricGenus k A

Corollary 29: Under Serre duality (here as a k-linear equivalence H¹(O_X) ≃ (Ω[A⁄k])*), the arithmetic genus equals the geometric genus.

theorem CurveGenusGeometric.genus_eq_finrank_kahler (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (H1_O : Type u_3) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[A⁄k]) : arithmeticGenus k H1_O = Module.finrank k Ω[A⁄k]

The arithmetic genus equals the Kähler-differential dimension dim_k Ω[A⁄k], via Serre duality between H¹(O_X) and the dual of the global differentials.

theorem CurveGenusGeometric.euler_char_structure_sheaf (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (H0_O : Type u_3) [AddCommGroup H0_O] [Module k H0_O] (H1_O : Type u_4) [AddCommGroup H1_O] [Module k H1_O] (h_h0 : Module.finrank k H0_O = 1) (h_h1 : Module.finrank k H1_O = geometricGenus k A) : ↑(Module.finrank k H0_O) - ↑(Module.finrank k H1_O) = 1 - ↑(geometricGenus k A)

Euler characteristic identity for the structure sheaf: given h⁰(O_X) = 1 and h¹(O_X) = g, we get χ(O_X) = 1 - g.

theorem CurveGenusGeometric.serre_duality_euler_char (g : ℤ) : 1 - g + (g - 1) = 0

Serre duality consistency: the Euler characteristics χ(O_X) = 1 - g and χ(ω_X) = g - 1 sum to zero.

theorem CurveGenusGeometric.geometricGenus_nonneg (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : 0 ≤ ↑(geometricGenus k A)

The geometric genus is non-negative when viewed as an integer.

theorem CurveGenusGeometric.genus_zero_iff_rational (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (H1_O : Type u_3) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[A⁄k]) (hg : geometricGenus k A = 0) : arithmeticGenus k H1_O = 0

Genus-zero (rational) curves: if the geometric genus vanishes, then so does the arithmetic genus, via Serre duality.

theorem CurveGenusGeometric.genus_one_elliptic (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (H1_O : Type u_3) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[A⁄k]) (hg : geometricGenus k A = 1) : arithmeticGenus k H1_O = 1

Genus-one (elliptic) case: if the geometric genus equals 1, then so does the arithmetic genus.