noncomputable def ArithmeticGeometricGenus.arithmeticGenusP1 (k : Type) [Field k] : ℕ

The arithmetic genus of ℙ¹_k: g_a := dim_k H¹(ℙ¹, O).

noncomputable def ArithmeticGeometricGenus.geometricGenusP1 (k : Type) [Field k] : ℕ

The geometric genus of ℙ¹_k: g_m := dim_k Γ(ℙ¹, ω) = dim_k H⁰(ℙ¹, O(-2)).

theorem ArithmeticGeometricGenus.arithmeticGenusP1_eq_zero (k : Type) [Field k] : arithmeticGenusP1 k = 0

The arithmetic genus of ℙ¹ is 0.

theorem ArithmeticGeometricGenus.geometricGenusP1_eq_zero (k : Type) [Field k] : geometricGenusP1 k = 0

The geometric genus of ℙ¹ is 0, since H⁰(ℙ¹, O(-2)) = 0.

theorem ArithmeticGeometricGenus.arith_eq_geom_genus_P1 (k : Type) [Field k] : arithmeticGenusP1 k = geometricGenusP1 k

For ℙ¹, the arithmetic and geometric genera coincide (instance of Cor 29, Lec 25).

theorem ArithmeticGeometricGenus.cor29_arithmetic_eq_geometric_genus {k : Type u_1} [Field k] (C : DedekindCurve k) (H1_O : Type u_2) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[C.A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[C.A⁄k]) : Module.finrank k H1_O = Module.finrank k Ω[C.A⁄k]

Corollary 29 (Lec 25), abstract form: Serre duality H¹(O) ≃ Γ(K_X)* implies dim H¹(O) = dim Γ(K_X), so the arithmetic and geometric genera agree.

theorem ArithmeticGeometricGenus.cor29_arith_genus_eq_ddGenus {k : Type u_1} [Field k] (C : DedekindCurve k) (H1_O : Type u_2) [AddCommGroup H1_O] [Module k H1_O] [FiniteDimensional k H1_O] [FiniteDimensional k Ω[C.A⁄k]] (hSD : H1_O ≃ₗ[k] Module.Dual k Ω[C.A⁄k]) : Module.finrank k H1_O = C.ddGenus

Restatement of Corollary 29 in terms of the differential-defined genus ddGenus of a Dedekind curve: dim H¹(O) = g.

theorem ArithmeticGeometricGenus.serre_duality_numerical_P1 (k : Type) [Field k] (n : ℤ) : Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

Numerical Serre duality on ℙ¹: dim H¹(O(n)) = dim H⁰(O(-2-n)).

theorem ArithmeticGeometricGenus.euler_char_eq_one_minus_arithmeticGenus_P1 (k : Type) [Field k] : ↑(Module.finrank k (SheafCohomology.H0 k 0)) - ↑(Module.finrank k (SheafCohomology.H1 k 0)) = 1 - ↑(arithmeticGenusP1 k)

Euler characteristic of O on ℙ¹: χ(O) = 1 - g_a = 1.