structure RiemannHurwitzAssembly.CurveCovering : Type

A finite morphism of smooth complete curves: source X, target Y, degree n > 0, and a ramification divisor of nonnegative degree deg_R, together with the canonical-divisor identity K_X = n · K_Y + R.

• X : CanonicalSheafCurves.SmoothCompleteCurve
• Y : CanonicalSheafCurves.SmoothCompleteCurve
• n : ℤ
• hn : 0 < self.n
• deg_R : ℤ
• deg_R_nonneg : 0 ≤ self.deg_R
• degK_eq : self.X.degK = self.n * self.Y.degK + self.deg_R

theorem RiemannHurwitzAssembly.CurveCovering.riemann_hurwitz_genus (f : CurveCovering) : 2 * f.X.g - 2 = f.n * (2 * f.Y.g - 2) + f.deg_R

Riemann–Hurwitz theorem: for a finite morphism of smooth complete curves, 2 g_X − 2 = n(2 g_Y − 2) + deg R, obtained from K_X = n K_Y + R.

theorem RiemannHurwitzAssembly.CurveCovering.riemann_hurwitz_genus_explicit (f : CurveCovering) : 2 * f.X.g - 2 = f.n * (2 * f.Y.g - 2) + f.deg_R

Explicit (step-by-step) version of the Riemann–Hurwitz formula.

theorem RiemannHurwitzAssembly.CurveCovering.degree_form (f : CurveCovering) : f.X.degK = f.n * f.Y.degK + f.deg_R

The defining canonical-divisor identity K_X = n K_Y + R, repackaged.

theorem RiemannHurwitzAssembly.CurveCovering.genus_lower_bound (f : CurveCovering) : f.X.g ≥ f.n * f.Y.g - f.n + 1

Genus lower bound from Riemann–Hurwitz: g_X ≥ n · g_Y − n + 1.

theorem RiemannHurwitzAssembly.CurveCovering.deg_R_from_genera (f : CurveCovering) : f.deg_R = 2 * f.X.g - 2 - f.n * (2 * f.Y.g - 2)

The ramification-divisor degree expressed via the source and target genera.

theorem RiemannHurwitzAssembly.CurveCovering.etale_genus (f : CurveCovering) (h : f.deg_R = 0) : 2 * f.X.g - 2 = f.n * (2 * f.Y.g - 2)

For an étale cover (no ramification), the Riemann–Hurwitz formula reduces to the exact relation 2 g_X − 2 = n(2 g_Y − 2).

theorem RiemannHurwitzAssembly.CurveCovering.hyperelliptic_ramification (f : CurveCovering) (hn : f.n = 2) (hg : f.Y.g = 0) : f.deg_R = 2 * f.X.g + 2

Hyperelliptic curve example: a double cover of ℙ¹ has ramification divisor of degree 2 g_X + 2 (the number of Weierstrass points).

theorem RiemannHurwitzAssembly.riemann_hurwitz_theorem (f : CurveCovering) : 2 * f.X.g - 2 = f.n * (2 * f.Y.g - 2) + f.deg_R

The Riemann–Hurwitz theorem (Thm 21.1) packaged as a standalone statement about CurveCovering.

theorem RiemannHurwitzAssembly.canonical_degree_eq_2g_sub_2 (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK = 2 * C.g - 2

Restating: the canonical divisor of a smooth complete curve has degree 2g − 2.

theorem RiemannHurwitzAssembly.riemann_hurwitz_from_A1 (f : CurveCovering) : 2 * f.X.g - 2 = f.n * (2 * f.Y.g - 2) + f.deg_R

Alternative derivation of Riemann–Hurwitz via the abstract numerical lemma riemann_hurwitz_formula applied to canonical degrees.