noncomputable def RiemannHurwitzFormula.DVRRamificationIndex {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra R S] : ℕ

The ramification index of an extension of DVRs R ⊆ S, defined as the ramification index of the maximal ideals.

def RiemannHurwitzFormula.DVRIsUnramified {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra R S] : Prop

An extension of DVRs R ⊆ S is unramified iff the ramification index equals 1.

theorem RiemannHurwitzFormula.DVR_ef_eq_degree {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [IsDedekindDomain R] [IsDedekindDomain S] (hp0 : IsLocalRing.maximalIdeal R ≠ ⊥) : DVRRamificationIndex * (IsLocalRing.maximalIdeal R).inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L

Fundamental identity for an extension of DVRs: the ramification index times the inertia degree equals the field extension degree [L : K].

theorem RiemannHurwitzFormula.DVR_unramified_inertiaDeg_eq_degree {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [IsDedekindDomain R] [IsDedekindDomain S] (hp0 : IsLocalRing.maximalIdeal R ≠ ⊥) (hunr : DVRIsUnramified) : (IsLocalRing.maximalIdeal R).inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L

In the unramified case for DVRs, the inertia degree equals the field extension degree [L : K].

theorem RiemannHurwitzFormula.DVR_ramification_contribution_nonneg {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra R S] [IsDedekindDomain R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hp0 : IsLocalRing.maximalIdeal R ≠ ⊥) [(IsLocalRing.maximalIdeal R).IsMaximal] [(IsLocalRing.maximalIdeal S).IsPrime] [(IsLocalRing.maximalIdeal S).LiesOver (IsLocalRing.maximalIdeal R)] : 0 ≤ ↑DVRRamificationIndex - 1

The local contribution e - 1 of a DVR extension to the ramification divisor is non-negative.

noncomputable def RiemannHurwitzFormula.ramificationDivisorDegreeAt {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (p : Ideal R) [p.IsMaximal] (_hp0 : p ≠ ⊥) : ℤ

The local degree at p of the ramification divisor of an extension R ⊆ S of Dedekind domains: the sum over primes P over p of e_P - 1.

theorem RiemannHurwitzFormula.ramificationDivisorDegreeAt_nonneg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : 0 ≤ ramificationDivisorDegreeAt S p hp0

The local ramification-divisor degree at p is non-negative.

theorem RiemannHurwitzFormula.ramificationDivisorDegreeAt_le_finrank {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ramificationDivisorDegreeAt S p hp0 ≤ ↑(Module.finrank K L)

The local ramification-divisor degree at p is bounded above by the field extension degree [L : K], via the fundamental identity.

theorem RiemannHurwitzFormula.ramificationDivisorDegreeAt_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ramificationDivisorDegreeAt S p hp0 = 0 ↔ ∀ P ∈ primesOverFinset p S, p.ramificationIdx P = 1

The local ramification-divisor degree at p vanishes iff every prime above p is unramified (e_P = 1).

structure RiemannHurwitzFormula.CurveMorphismData : Type

Numerical data attached to a finite morphism f : X → Y of smooth curves: the degree, the degrees of the canonical divisors on source and target, and the degree of the ramification divisor, with non-negativity/positivity hypotheses.

• degree : ℤ
• deg_KX : ℤ
• deg_KY : ℤ
• deg_R : ℤ
• h_deg_R_nonneg : 0 ≤ self.deg_R
• h_deg_pos : 0 < self.degree

theorem RiemannHurwitzFormula.riemann_hurwitz_canonical_decomp (f : CurveMorphismData) (deg_fKY : ℤ) (h_pullback : deg_fKY = f.degree * f.deg_KY) (h_canonical : f.deg_KX = deg_fKY + f.deg_R) : f.deg_KX = f.degree * f.deg_KY + f.deg_R

Given the canonical decomposition K_X = f*K_Y + R and the pullback identity deg f*K_Y = n · deg K_Y, we obtain deg K_X = n · deg K_Y + deg R.

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

Riemann–Hurwitz in degree form (Cor 27, Lec 21): for a CurveCovering, deg K_X = n · deg K_Y + deg R.

theorem RiemannHurwitzFormula.riemann_hurwitz_genus_from_data (f : CurveMorphismData) (g_X g_Y : ℤ) (h_gX : f.deg_KX = 2 * g_X - 2) (h_gY : f.deg_KY = 2 * g_Y - 2) (h_decomp : f.deg_KX = f.degree * f.deg_KY + f.deg_R) : 2 * g_X - 2 = f.degree * (2 * g_Y - 2) + f.deg_R

Translating Riemann–Hurwitz from canonical degrees to genus form via deg K_X = 2 g_X - 2, deg K_Y = 2 g_Y - 2.

theorem RiemannHurwitzFormula.riemann_hurwitz_genus_lower_bound (f : CurveMorphismData) (g_X g_Y : ℤ) (h_gX : f.deg_KX = 2 * g_X - 2) (h_gY : f.deg_KY = 2 * g_Y - 2) (h_decomp : f.deg_KX = f.degree * f.deg_KY + f.deg_R) : 2 * g_X - 2 ≥ f.degree * (2 * g_Y - 2)

Lower bound for the genus from Riemann–Hurwitz and ramification non-negativity.

theorem RiemannHurwitzFormula.riemann_hurwitz_ramification_determines_genus (f : CurveMorphismData) (h_decomp : f.deg_KX = f.degree * f.deg_KY + f.deg_R) : f.deg_R = f.deg_KX - f.degree * f.deg_KY

Solving Riemann–Hurwitz for deg R: it is determined by the canonical degrees and the cover degree.

def RiemannHurwitzFormula.CurveMorphismData.toP1 (n deg_KX deg_R : ℤ) (h_nonneg : 0 ≤ deg_R) (h_pos : 0 < n) : CurveMorphismData

Construct CurveMorphismData for a degree-n cover of ℙ¹, where deg K_Y = -2.

theorem RiemannHurwitzFormula.riemann_hurwitz_P1_target (n deg_KX deg_R : ℤ) (h_nonneg : 0 ≤ deg_R) (h_pos : 0 < n) (h_formula : deg_KX = -2 * n + deg_R) : (CurveMorphismData.toP1 n deg_KX deg_R h_nonneg h_pos).deg_KX = -2 * (CurveMorphismData.toP1 n deg_KX deg_R h_nonneg h_pos).degree + (CurveMorphismData.toP1 n deg_KX deg_R h_nonneg h_pos).deg_R

Riemann–Hurwitz decomposition for a cover of ℙ¹ (target genus 0).

theorem RiemannHurwitzFormula.riemann_hurwitz_P1_genus (n g deg_R : ℤ) (h_RH : 2 * g - 2 = -2 * n + deg_R) : deg_R = 2 * g + 2 * n - 2

Riemann–Hurwitz for a cover of ℙ¹ solved for deg R.

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

Totally ramified cover of ℙ¹: if there are r totally ramified points (each contributing n - 1), then 2 g = r(n-1) - 2n + 2.

theorem RiemannHurwitzFormula.elliptic_curve_canonical_degree_zero : have n := 2; have num_ram := 4; have e := 2; have deg_R := num_ram * (e - 1); have deg_KP1 := -2; n * deg_KP1 + deg_R = 0

Numerical identity: a degree-2 cover of ℙ¹ with 4 simple ramification points has n · deg K_{ℙ¹} + deg R = 0, recovering deg K_X = 0 for an elliptic curve.

theorem RiemannHurwitzFormula.elliptic_curve_genus_one : have n := 2; have deg_R := 4 * (2 - 1); have g := 1; 2 * g - 2 = n * -2 + deg_R

Numerical identity: Riemann–Hurwitz for a double cover of ℙ¹ with four simple branch points has genus g = 1.

def RiemannHurwitzFormula.ellipticCurveP1Data : CurveMorphismData

CurveMorphismData for a double cover E → ℙ¹ realizing an elliptic curve.

theorem RiemannHurwitzFormula.ellipticCurveP1_satisfies_RH : ellipticCurveP1Data.deg_KX = ellipticCurveP1Data.degree * ellipticCurveP1Data.deg_KY + ellipticCurveP1Data.deg_R

Verifies that ellipticCurveP1Data satisfies Riemann–Hurwitz in degree form.

theorem RiemannHurwitzFormula.ellipticCurve_genus_from_canonical : 0 = 2 * 1 - 2

Numerical: for an elliptic curve deg K = 0 = 2·1 - 2.

theorem RiemannHurwitzFormula.hyperelliptic_branch_points_eq (g b : ℤ) (h_RH : 2 * g - 2 = 2 * -2 + b) : b = 2 * g + 2

For a hyperelliptic curve of genus g (a double cover of ℙ¹), the number of branch points satisfies b = 2g + 2.

def RiemannHurwitzFormula.hyperellipticData (g : ℤ) (hg : 0 ≤ 2 * g + 2) : CurveMorphismData

CurveMorphismData for a hyperelliptic double cover of ℙ¹ realizing a curve of genus g, with 2g + 2 simple branch points.

theorem RiemannHurwitzFormula.hyperellipticData_satisfies_RH (g : ℤ) (hg : 0 ≤ 2 * g + 2) : (hyperellipticData g hg).deg_KX = (hyperellipticData g hg).degree * (hyperellipticData g hg).deg_KY + (hyperellipticData g hg).deg_R

The hyperelliptic data satisfies Riemann–Hurwitz in degree form.

theorem RiemannHurwitzFormula.riemann_hurwitz_arithmetic_genus_constraint (g_X g_Y : ℕ) (n deg_R : ℤ) (h_formula : 2 * ↑g_X - 2 = n * (2 * ↑g_Y - 2) + deg_R) : deg_R = 2 * ↑g_X - 2 - n * (2 * ↑g_Y - 2)

Express the ramification divisor degree in terms of arithmetic genera.

theorem RiemannHurwitzFormula.riemann_hurwitz_genus_growth (g_X g_Y n deg_R : ℤ) (hR : 0 ≤ deg_R) (h_formula : 2 * g_X - 2 = n * (2 * g_Y - 2) + deg_R) : g_X ≥ n * (g_Y - 1) + 1

Genus growth bound: the source genus satisfies g_X ≥ n(g_Y - 1) + 1.

theorem RiemannHurwitzFormula.riemann_hurwitz_isomorphism_genus (g_X g_Y : ℤ) (h_formula : 2 * g_X - 2 = 1 * (2 * g_Y - 2) + 0) : g_X = g_Y

A degree-1 unramified cover is an isomorphism in the sense that source and target have the same genus.

theorem RiemannHurwitzFormula.riemann_hurwitz_etale_genus (g_X g_Y n : ℤ) (h_formula : 2 * g_X - 2 = n * (2 * g_Y - 2) + 0) : g_X = n * g_Y - n + 1

For an étale (unramified) cover of degree n, g_X = n g_Y - n + 1.