structure RiemannHurwitzDegree.CurveCoverData : Type

Bundle of data for a finite cover f : X → Y of smooth complete curves: a CurveMorphismData together with the source and target curves and equalities identifying the abstract canonical degrees with the curves' canonical degrees.

• morphism : RiemannHurwitzFormula.CurveMorphismData
• source : CanonicalSheafCurves.SmoothCompleteCurve
• target : CanonicalSheafCurves.SmoothCompleteCurve
• h_degK_X : self.morphism.deg_KX = self.source.degK
• h_degK_Y : self.morphism.deg_KY = self.target.degK

theorem RiemannHurwitzDegree.riemann_hurwitz_genus_form (f : CurveCoverData) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : 2 * f.source.g - 2 = f.morphism.degree * (2 * f.target.g - 2) + f.morphism.deg_R

Riemann–Hurwitz in genus form: for a cover f : X → Y of smooth complete curves with Riemann–Hurwitz decomposition deg K_X = n · deg K_Y + deg R, one has 2 g_X - 2 = n (2 g_Y - 2) + deg R (Thm 21.1, Cor 27, Lec 21).

theorem RiemannHurwitzDegree.riemann_hurwitz_genus_solve (f : CurveCoverData) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : 2 * f.source.g = f.morphism.degree * (2 * f.target.g - 2) + f.morphism.deg_R + 2

Solving Riemann–Hurwitz for 2 g_X: gives 2 g_X = n (2 g_Y - 2) + deg R + 2.

theorem RiemannHurwitzDegree.riemann_hurwitz_genus_lower_bound_cover (f : CurveCoverData) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : 2 * f.source.g - 2 ≥ f.morphism.degree * (2 * f.target.g - 2)

Consequence of Riemann–Hurwitz: since the ramification divisor has non-negative degree, 2 g_X - 2 ≥ n (2 g_Y - 2).

def RiemannHurwitzDegree.CurveCoverData.mk' (X Y : CanonicalSheafCurves.SmoothCompleteCurve) (n degR : ℤ) (h_nonneg : 0 ≤ degR) (h_pos : 0 < n) (_h_RH : 2 * X.g - 2 = n * (2 * Y.g - 2) + degR) : CurveCoverData

Convenience constructor for CurveCoverData from a source and target curve, a degree n, a ramification degree degR, and the hypothesis that the genus form of Riemann–Hurwitz holds.

theorem RiemannHurwitzDegree.riemann_hurwitz_P1_genus_form (g_X n degR : ℤ) (h_RH : 2 * g_X - 2 = n * (2 * 0 - 2) + degR) : 2 * g_X - 2 = -2 * n + degR

Specialization of the Riemann–Hurwitz genus formula when the target is ℙ¹ (genus 0): 2 g_X - 2 = -2 n + deg R.

theorem RiemannHurwitzDegree.riemann_hurwitz_P1_genus_solve (g n degR : ℤ) (h_RH : 2 * g - 2 = -2 * n + degR) : 2 * g = degR - 2 * n + 2

Solving the ℙ¹-target Riemann–Hurwitz formula for 2 g_X.

theorem RiemannHurwitzDegree.simple_ramification_degR (r : ℤ) : r * (2 - 1) = r

Simple ramification contribution: each simple ramification point (multiplicity 2) contributes (2 - 1) = 1 to the ramification divisor degree.

theorem RiemannHurwitzDegree.riemann_hurwitz_simple_genus (g n r : ℤ) (h_RH : 2 * g - 2 = -2 * n + r * (2 - 1)) : 2 * g - 2 = -2 * n + r

Riemann–Hurwitz for a cover with only simple ramification: substituting r · (2 - 1) = r gives 2 g - 2 = -2 n + r.

theorem RiemannHurwitzDegree.simple_ramification_count (g n r : ℤ) (h_RH : 2 * g - 2 = -2 * n + r) : r = 2 * g + 2 * n - 2

Counts the number of simple ramification points in terms of g and n for a cover of ℙ¹ with only simple ramification.

theorem RiemannHurwitzDegree.genus_hyperelliptic_from_curves (g : ℕ) : have X := CanonicalSheafCurves.mkCurve g; have Y := CanonicalSheafCurves.mkCurve 0; 2 * X.g - 2 = 2 * (2 * Y.g - 2) + (2 * ↑g + 2)

For a hyperelliptic double cover of ℙ¹ by a curve of genus g, Riemann–Hurwitz reduces to 2 g - 2 = 2(2·0 - 2) + (2 g + 2).

theorem RiemannHurwitzDegree.hyperelliptic_genus_from_branch_points (g b : ℤ) (h_RH : 2 * g - 2 = 2 * -2 + b) : 2 * g = b - 2

Recovering the genus of a hyperelliptic curve from its branch point count: if b is the number of branch points, then 2g = b - 2.

theorem RiemannHurwitzDegree.genus_plane_quartic : have d := 4; have g := 3; 2 * g - 2 = d * (d - 3)

A smooth plane quartic has genus 3: 2g - 2 = d(d - 3) with d = 4.

theorem RiemannHurwitzDegree.plane_quartic_degK : 4 * (4 - 3) = 2 * 3 - 2

Canonical degree numerical identity for a plane quartic of genus 3.

theorem RiemannHurwitzDegree.plane_quartic_as_cover_P1 : 2 * 3 - 2 = -2 * 4 + 12

A plane quartic viewed as a degree-4 cover of ℙ¹: the Riemann–Hurwitz numerical identity 2·3 - 2 = -2·4 + 12.

theorem RiemannHurwitzDegree.plane_quartic_ramification_count : 2 * 3 + 2 * 4 - 2 = 12

Ramification count for a plane quartic seen as a degree-4 cover of ℙ¹.

theorem RiemannHurwitzDegree.genus_plane_quintic : have d := 5; have g := 6; 2 * g - 2 = d * (d - 3)

A smooth plane quintic has genus 6: 2g - 2 = d(d - 3) with d = 5.

theorem RiemannHurwitzDegree.genus_degree3_cover_4_total_ram : have n := 3; have r := 4; have e := 3; have degR := r * (e - 1); have g := 2; 2 * g - 2 = -2 * n + degR

Genus from a degree-3 cover of ℙ¹ with 4 totally ramified (multiplicity 3) points: numerical check of Riemann–Hurwitz.

theorem RiemannHurwitzDegree.genus_degree3_cover_6_simple_ram : have n := 3; have degR := 6; have g := 1; 2 * g - 2 = -2 * n + degR

Genus from a degree-3 cover of ℙ¹ with 6 simple ramification points.

theorem RiemannHurwitzDegree.genus_unramified_double_cover_genus2 : have C_X := CanonicalSheafCurves.mkCurve 3; have C_Y := CanonicalSheafCurves.mkCurve 2; 2 * C_X.g - 2 = 2 * (2 * C_Y.g - 2) + 0

For an unramified double cover of a genus-2 curve, the cover has genus 3 (checked numerically via Riemann–Hurwitz).

theorem RiemannHurwitzDegree.genus_etale_cover (g_X g_Y n : ℤ) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2)) : g_X = n * (g_Y - 1) + 1

Étale (unramified) covers: from Riemann–Hurwitz with deg R = 0, g_X = n (g_Y - 1) + 1.

theorem RiemannHurwitzDegree.luroth_bound (n degR g_X : ℤ) (hg : g_X ≥ 0) (h_RH : 2 * g_X - 2 = -2 * n + degR) : degR ≥ 2 * n - 2

Lüroth-type bound: for a cover X → ℙ¹ with g_X ≥ 0, the ramification divisor satisfies deg R ≥ 2n - 2.

theorem RiemannHurwitzDegree.luroth_bound_alt (n degR g_X : ℤ) (hg : g_X ≥ 0) (h_RH : 2 * g_X - 2 = -2 * n + degR) : degR ≥ 2 * (n - 1)

Alternative form of the Lüroth bound: deg R ≥ 2(n - 1).

theorem RiemannHurwitzDegree.genus_nonneg_constraint (g_X n degR : ℤ) (hg_X : g_X ≥ 0) (h_RH : 2 * g_X - 2 = -2 * n + degR) : degR ≥ 2 * n - 2

The non-negativity of the genus forces the ramification divisor degree to satisfy deg R ≥ 2n - 2 for any cover of ℙ¹.

theorem RiemannHurwitzDegree.hyperelliptic_min_branch_points (g_X : ℤ) (hg : g_X ≥ 0) (b : ℤ) (h_RH : 2 * g_X - 2 = 2 * -2 + b) : b ≥ 2

A hyperelliptic double cover of ℙ¹ must have at least 2 branch points.

theorem RiemannHurwitzDegree.degree3_min_ramification (g_X : ℤ) (hg : g_X ≥ 0) (degR : ℤ) (h_RH : 2 * g_X - 2 = -2 * 3 + degR) : degR ≥ 4

A degree-3 cover of ℙ¹ must have ramification divisor of degree at least 4.

theorem RiemannHurwitzDegree.riemann_hurwitz_parity (g_X g_Y n degR : ℤ) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) : ∃ (k : ℤ), degR = 2 * k

The Riemann–Hurwitz formula forces the ramification divisor degree deg R to be even.

def RiemannHurwitzDegree.ellipticCoverP1 : CurveCoverData

A double cover of ℙ¹ by an elliptic curve (genus 1) with 4 simple ramification points; the standard example.

theorem RiemannHurwitzDegree.ellipticCoverP1_source_genus : ellipticCoverP1.source.g = 1

The source of ellipticCoverP1 has genus 1.

theorem RiemannHurwitzDegree.ellipticCoverP1_target_genus : ellipticCoverP1.target.g = 0

The target of ellipticCoverP1 is ℙ¹ (genus 0).

theorem RiemannHurwitzDegree.ellipticCoverP1_degree : ellipticCoverP1.morphism.degree = 2

The degree of ellipticCoverP1 is 2.

theorem RiemannHurwitzDegree.ellipticCoverP1_degR : ellipticCoverP1.morphism.deg_R = 4

The ramification divisor of ellipticCoverP1 has degree 4.

theorem RiemannHurwitzDegree.ellipticCoverP1_RH : 2 * ellipticCoverP1.source.g - 2 = ellipticCoverP1.morphism.degree * (2 * ellipticCoverP1.target.g - 2) + ellipticCoverP1.morphism.deg_R

Riemann–Hurwitz holds for ellipticCoverP1 in genus form.

def RiemannHurwitzDegree.genus2CoverP1 : CurveCoverData

A double cover of ℙ¹ by a genus-2 curve with 6 simple ramification points.

theorem RiemannHurwitzDegree.genus2CoverP1_source_genus : genus2CoverP1.source.g = 2

The source of genus2CoverP1 has genus 2.

theorem RiemannHurwitzDegree.genus2CoverP1_RH : 2 * genus2CoverP1.source.g - 2 = genus2CoverP1.morphism.degree * (2 * genus2CoverP1.target.g - 2) + genus2CoverP1.morphism.deg_R

Riemann–Hurwitz holds for genus2CoverP1 in genus form.

def RiemannHurwitzDegree.genus3CoverP1 : CurveCoverData

A double cover of ℙ¹ by a genus-3 curve with 8 simple ramification points.

theorem RiemannHurwitzDegree.genus3CoverP1_RH : 2 * genus3CoverP1.source.g - 2 = genus3CoverP1.morphism.degree * (2 * genus3CoverP1.target.g - 2) + genus3CoverP1.morphism.deg_R

Riemann–Hurwitz holds for genus3CoverP1 in genus form.

def RiemannHurwitzDegree.hyperellipticCover (g : ℕ) : CurveCoverData

Hyperelliptic cover: a generic double cover X → ℙ¹ where X has genus g and the cover has 2g + 2 simple ramification points.

theorem RiemannHurwitzDegree.hyperellipticCover_source_genus (g : ℕ) : (hyperellipticCover g).source.g = ↑g

The source of hyperellipticCover g has genus g.

theorem RiemannHurwitzDegree.hyperellipticCover_target_genus (g : ℕ) : (hyperellipticCover g).target.g = 0

The target of hyperellipticCover g is ℙ¹.

theorem RiemannHurwitzDegree.hyperellipticCover_degree (g : ℕ) : (hyperellipticCover g).morphism.degree = 2

The hyperelliptic cover has degree 2.

theorem RiemannHurwitzDegree.hyperellipticCover_degR (g : ℕ) : (hyperellipticCover g).morphism.deg_R = 2 * ↑g + 2

The hyperelliptic cover of genus g has ramification divisor of degree 2g + 2.

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

The Riemann–Hurwitz degree formula: for a finite cover f : X → Y of smooth complete curves of degree n, deg K_X = n · deg K_Y + deg R.