noncomputable def SerreDualityDedekind.h0_ideal (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (I : Ideal A) : ℕ

h⁰ of the ideal sheaf I on a Dedekind curve, defined as the k-dimension of I viewed as a submodule.

noncomputable def SerreDualityDedekind.h1_ideal (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (I : Ideal A) : ℕ

h¹ of the ideal sheaf I, defined via Serre duality as the k-dimension of Hom_A(I, Ω_{A/k}).

theorem SerreDualityDedekind.serre_duality_ideal (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (I : Ideal A) : h1_ideal k A I = Module.finrank k (↥I →ₗ[A] Ω[A⁄k])

Serre duality definition for ideal sheaves: h¹(I) = dim_k Hom_A(I, Ω_{A/k}).

theorem SerreDualityDedekind.h1_ideal_top_eq_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] : h1_ideal k A ⊤ = DedekindCurve.h1_O k A

For the unit ideal I = ⊤, the Serre-dual definition h¹(I) agrees with h¹(O_X) defined as dim_k Ω_{A/k}.

noncomputable def SerreDualityDedekind.homTopOmegaEquivK (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : (↥⊤ →ₗ[A] Ω[A⁄k]) ≃ₗ[k] Ω[A⁄k]

Hom_A(⊤, Ω_{A/k}) ≃ₗ[k] Ω_{A/k}: evaluating at 1 ∈ A.

theorem SerreDualityDedekind.finrank_hom_top_eq_finrank_omega (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : Module.finrank k (↥⊤ →ₗ[A] Ω[A⁄k]) = Module.finrank k Ω[A⁄k]

The k-dimension of Hom_A(⊤, Ω_{A/k}) equals that of Ω_{A/k}.

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

Serre duality consistency check: h¹(O_X) = dim_k Ω_{A/k}, combining the ideal-sheaf duality with the Hom(⊤, Ω) ≃ Ω equivalence.

theorem SerreDualityDedekind.h1_ideal_top_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_ideal k A ⊤ = Module.finrank k Ω[A⁄k]

h¹ of the unit ideal sheaf equals dim_k Ω_{A/k}, the geometric genus.

noncomputable def SerreDualityDedekind.DedekindCurve.chi_ideal {k : Type u_1} [Field k] (C : DedekindCurve k) (I : Ideal C.A) : ℤ

Euler characteristic of an ideal sheaf on a Dedekind curve: χ(I) = h⁰(I) − h¹(I).

theorem SerreDualityDedekind.cech_serre_duality_P1_nonneg (k : Type) [Field k] (n : ℤ) (hn : 0 ≤ n) : Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

Serre duality on ℙ¹ (nonneg case): for n ≥ 0, dim H¹(O(n)) = dim H⁰(O(-2 - n)).

theorem SerreDualityDedekind.cech_serre_duality_P1_neg (k : Type) [Field k] (n : ℤ) (hn : n < 0) : Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

Serre duality on ℙ¹ (negative case): for n < 0, dim H¹(O(n)) = dim H⁰(O(-2 - n)).

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

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

noncomputable def SerreDualityDedekind.h1_ideal_sheaf (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (I : Ideal A) : ℕ

Alternative name for h¹ of an ideal sheaf, emphasizing the sheaf perspective.

theorem SerreDualityDedekind.serre_duality_ideal_sheaf (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (I : Ideal A) : h1_ideal_sheaf k A I = Module.finrank k (↥I →ₗ[A] Ω[A⁄k])

Sheaf-theoretic Serre duality: h¹(I) = dim_k Hom_A(I, Ω_{A/k}).