theorem GenusConstruction.chi_P1_struct_from_cech (k : Type) [Field k] : ↑(RiemannRoch.dimH0 k 0) - ↑(RiemannRoch.dimH1 k 0) = 1

Euler characteristic of the structure sheaf on P^1 via Čech: χ(O_{P^1}) = 1.

theorem GenusConstruction.chi_P1_canonical_from_cech (k : Type) [Field k] : ↑(RiemannRoch.dimH0 k (-2)) - ↑(RiemannRoch.dimH1 k (-2)) = -1

Euler characteristic of the canonical sheaf on P^1: χ(ω_{P^1}) = -1.

theorem GenusConstruction.chi_P1_struct_eq_rrHom (k : Type) [Field k] : ↑(RiemannRoch.dimH0 k 0) - ↑(RiemannRoch.dimH1 k 0) = (RiemannRochCurves.rrHom 0) (1, 0)

The Čech computation of χ(O_{P^1}) matches the value predicted by the Riemann-Roch map.

theorem GenusConstruction.chi_P1_canonical_eq_rrHom (k : Type) [Field k] : ↑(RiemannRoch.dimH0 k (-2)) - ↑(RiemannRoch.dimH1 k (-2)) = (RiemannRochCurves.rrHom 0) (1, -2)

The Čech computation of χ(ω_{P^1}) matches the Riemann-Roch prediction for genus 0.

def GenusConstruction.P1CurveFromCech (_k : Type) [Field _k] : CanonicalSheafCurves.SmoothCompleteCurve

The smooth complete curve P^1 packaged from Čech data: genus 0, canonical degree -2, Euler characteristic given by the Riemann-Roch homomorphism.

theorem GenusConstruction.P1CurveFromCech_genus (k : Type) [Field k] : (P1CurveFromCech k).g = 0

The genus of P1CurveFromCech k is 0.

theorem GenusConstruction.P1CurveFromCech_degK (k : Type) [Field k] : (P1CurveFromCech k).degK = -2

The canonical degree of P1CurveFromCech k is -2.

theorem GenusConstruction.P1CurveFromCech_eq_mkCurve (k : Type) [Field k] : P1CurveFromCech k = CanonicalSheafCurves.mkCurve 0

P1CurveFromCech k agrees with the abstract genus-0 curve mkCurve 0.

theorem GenusConstruction.P1_chi_struct_validated (k : Type) [Field k] : (P1CurveFromCech k).χ (1, 0) = ↑(RiemannRoch.dimH0 k 0) - ↑(RiemannRoch.dimH1 k 0)

Validation: the Riemann-Roch value of O_{P^1} on P1CurveFromCech matches the Čech result.

theorem GenusConstruction.P1_chi_canonical_validated (k : Type) [Field k] : (P1CurveFromCech k).χ (1, (P1CurveFromCech k).degK) = ↑(RiemannRoch.dimH0 k (-2)) - ↑(RiemannRoch.dimH1 k (-2))

Validation: the Riemann-Roch value of ω_{P^1} matches the Čech-computed Euler characteristic.

theorem GenusConstruction.P1_H0_struct_from_cech (k : Type) [Field k] : RiemannRoch.dimH0 k 0 = 1

h^0(O_{P^1}) = 1: the structure sheaf has a one-dimensional global section space.

theorem GenusConstruction.P1_H1_struct_from_cech (k : Type) [Field k] : RiemannRoch.dimH1 k 0 = 0

h^1(O_{P^1}) = 0: the arithmetic genus of P^1 is zero.

theorem GenusConstruction.P1_H0_canonical_from_cech (k : Type) [Field k] : RiemannRoch.dimH0 k (-2) = 0

h^0(ω_{P^1}) = 0: the canonical bundle on P^1 has no global sections.

theorem GenusConstruction.P1_H1_canonical_from_cech (k : Type) [Field k] : RiemannRoch.dimH1 k (-2) = 1

h^1(ω_{P^1}) = 1: dual to global sections of O_{P^1} via Serre duality.

noncomputable def GenusConstruction.curveFromDedekind (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : CanonicalSheafCurves.SmoothCompleteCurve

A smooth complete curve constructed from a finite-dimensional Dedekind algebra A over k: genus is the curve genus of A, canonical degree is 2g - 2, and Euler characteristic is the Riemann-Roch homomorphism.

theorem GenusConstruction.curveFromDedekind_genus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : (curveFromDedekind k A).g = ↑(RiemannRochCurves.curveGenus k A)

Genus of curveFromDedekind k A is the Dedekind-curve genus.

theorem GenusConstruction.curveFromDedekind_degK (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : (curveFromDedekind k A).degK = 2 * ↑(RiemannRochCurves.curveGenus k A) - 2

Canonical degree of curveFromDedekind k A is 2g - 2.

theorem GenusConstruction.curveFromDedekind_eq_mkCurve (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : curveFromDedekind k A = CanonicalSheafCurves.mkCurve (RiemannRochCurves.curveGenus k A)

curveFromDedekind k A coincides with the abstract genus-g curve mkCurve g.

theorem GenusConstruction.curveFromDedekind_eq_toSmoothCompleteCurve {k : Type u_1} [Field k] (C : DedekindCurve k) : curveFromDedekind k C.A = C.toSmoothCompleteCurve

Bridge: the smooth complete curve constructed from a Dedekind curve agrees with its packaged toSmoothCompleteCurve.

theorem GenusConstruction.ddGenus_eq_curveFromDedekind_genus {k : Type u_1} [Field k] (C : DedekindCurve k) : ↑C.ddGenus = (curveFromDedekind k C.A).g

The Dedekind genus equals the genus of the corresponding curveFromDedekind.

theorem GenusConstruction.curveFromDedekind_degK_eq_dedekind {k : Type u_1} [Field k] (C : DedekindCurve k) : (curveFromDedekind k C.A).degK = C.toSmoothCompleteCurve.degK

Canonical degrees agree across the Dedekind bridge.