noncomputable def globalRamification {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (basePrimes : Finset (Ideal R)) (hmax : ∀ p ∈ basePrimes, p.IsMaximal) (hbot : ∀ p ∈ basePrimes, p ≠ ⊥) : ℤ

Global ramification contribution: sum of the total ramification at each prime of R lying under the cover S/R.

theorem globalRamification_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (basePrimes : Finset (Ideal R)) (hmax : ∀ p ∈ basePrimes, p.IsMaximal) (hbot : ∀ p ∈ basePrimes, p ≠ ⊥) : globalRamification S basePrimes hmax hbot = ∑ p ∈ basePrimes, if h : p ∈ basePrimes then totalRamificationAt S p ⋯ else 0

Unfolding of globalRamification as a sum of local total-ramification contributions.

theorem globalRamification_nonneg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (basePrimes : Finset (Ideal R)) (hmax : ∀ p ∈ basePrimes, p.IsMaximal) (hbot : ∀ p ∈ basePrimes, p ≠ ⊥) : 0 ≤ globalRamification S basePrimes hmax hbot

The global ramification is non-negative.

structure CurveCovering : Type (max (u_1 + 1) (u_2 + 1))

Data of a finite covering of smooth complete curves X → Y arising from a Dedekind ring extension R ⊂ S, together with the local canonical-degree decompositions used in the Riemann–Hurwitz formula.

• R : Type u_1
• S : Type u_2
• instCR : CommRing self.R
• instDR : IsDedekindDomain self.R
• instCS : CommRing self.S
• instDS : IsDedekindDomain self.S
• instAlg : Algebra self.R self.S
• instNZ : NoZeroSMulDivisors self.R self.S
• X : CanonicalSheafCurves.SmoothCompleteCurve
• Y : CanonicalSheafCurves.SmoothCompleteCurve
• n : ℤ
• h_n_pos : 0 < self.n
• basePrimes : Finset (Ideal self.R)
• h_max (p : Ideal self.R) : p ∈ self.basePrimes → p.IsMaximal
• h_bot (p : Ideal self.R) : p ∈ self.basePrimes → p ≠ ⊥
• localDegK_X : Ideal self.R → ℤ
• localDegK_Y : Ideal self.R → ℤ
• h_degK_X_sum : self.X.degK = self.basePrimes.sum self.localDegK_X
• h_degK_Y_sum : self.Y.degK = self.basePrimes.sum self.localDegK_Y
• h_local_degree (p : Ideal self.R) : p ∈ self.basePrimes → self.localDegK_X p = self.n * self.localDegK_Y p + if h : p ∈ self.basePrimes then totalRamificationAt self.S p ⋯ else 0

noncomputable def CurveCovering.deg_R (f : CurveCovering) : ℤ

The ramification degree deg R of a curve covering.

theorem CurveCovering.deg_R_nonneg (f : CurveCovering) : 0 ≤ f.deg_R

deg R is non-negative.

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

Canonical divisor identity in a covering: K_X = n · K_Y + R.

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

Riemann-Hurwitz formula for a covering: 2g_X - 2 = n(2g_Y - 2) + deg R.

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

Genus lower bound: g_X ≥ n(g_Y - 1) + 1.

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

Solving Riemann-Hurwitz for deg R in terms of the genera.

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

Alternate derivation of the Riemann-Hurwitz formula via the explicit riemann_hurwitz_formula helper.

theorem 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 covering (no ramification), 2g_X - 2 = n(2g_Y - 2).

theorem CurveCovering.etale_genus_exact (f : CurveCovering) (h : f.deg_R = 0) : f.X.g = f.n * (f.Y.g - 1) + 1

Exact étale formula: g_X = n(g_Y - 1) + 1 when deg R = 0.

theorem CurveCovering.etale_double_cover_genus (f : CurveCovering) (h_etale : f.deg_R = 0) (h_double : f.n = 2) : f.X.g = 2 * f.Y.g - 1

Étale double covers satisfy g_X = 2 g_Y - 1.

theorem hyperelliptic_identity (g : ℤ) : 2 * g - 2 = 2 * (2 * 0 - 2) + (2 * g + 2)

Numerical identity for hyperelliptic curves: 2g - 2 = 2(2·0 - 2) + (2g + 2).

def CurveCovering.ellipticIdentity : CurveCovering

Trivial identity covering of an elliptic curve by itself (degree 1, no ramification).

theorem CurveCovering.ellipticIdentity_deg_R : ellipticIdentity.deg_R = 0

deg R = 0 for the elliptic identity covering.

theorem CurveCovering.ellipticIdentity_degK_eq : ellipticIdentity.X.degK = ellipticIdentity.n * ellipticIdentity.Y.degK + ellipticIdentity.deg_R

Canonical-degree identity for the elliptic identity covering.

theorem CurveCovering.ellipticIdentity_rh_genus : 2 * ellipticIdentity.X.g - 2 = ellipticIdentity.n * (2 * ellipticIdentity.Y.g - 2) + ellipticIdentity.deg_R

Riemann-Hurwitz applied to the elliptic identity covering.

theorem CurveCovering.ellipticIdentity_genus_bound : ellipticIdentity.X.g ≥ ellipticIdentity.n * (ellipticIdentity.Y.g - 1) + 1

Genus lower bound applied to the elliptic identity covering.

theorem CurveCovering.ellipticIdentity_values : ellipticIdentity.X.g = 1 ∧ ellipticIdentity.Y.g = 1 ∧ ellipticIdentity.n = 1 ∧ ellipticIdentity.deg_R = 0

Numerical values realised by the elliptic identity covering: genera 1, 1, degree 1, ramification 0.

noncomputable def CurveCovering.P1Identity (p : Ideal ℤ) (hp_max : p.IsMaximal) (hp_bot : p ≠ ⊥) (h_totalRam : totalRamificationAt ℤ p hp_bot = 0) : CurveCovering

Identity covering of P^1 by itself, using a prescribed prime p of ℤ with vanishing total ramification.

noncomputable def CurveCovering.identityCovering (C : CanonicalSheafCurves.SmoothCompleteCurve) (p : Ideal ℤ) (hp_max : p.IsMaximal) (hp_bot : p ≠ ⊥) (h_totalRam : totalRamificationAt ℤ p hp_bot = 0) : CurveCovering

General identity covering: a smooth complete curve C paired with itself at degree 1.

theorem CurveCovering.identityCovering_deg_R (C : CanonicalSheafCurves.SmoothCompleteCurve) (p : Ideal ℤ) (hp_max : p.IsMaximal) (hp_bot : p ≠ ⊥) (h_totalRam : totalRamificationAt ℤ p hp_bot = 0) : (identityCovering C p hp_max hp_bot h_totalRam).deg_R = 0

The identity covering has ramification degree 0 when the local total ramification vanishes.

theorem CurveCovering.identityCovering_rh_genus (C : CanonicalSheafCurves.SmoothCompleteCurve) (p : Ideal ℤ) (hp_max : p.IsMaximal) (hp_bot : p ≠ ⊥) (h_totalRam : totalRamificationAt ℤ p hp_bot = 0) : 2 * C.g - 2 = 1 * (2 * C.g - 2) + (identityCovering C p hp_max hp_bot h_totalRam).deg_R

Riemann-Hurwitz for the identity covering: the trivial relation 2g - 2 = 1 · (2g - 2) + 0.

structure CurveCoveringDirect : Type (max (u_1 + 1) (u_2 + 1))

Simplified curve-covering structure: stores only the global canonical-degree formula without local data.

• R : Type u_1
• S : Type u_2
• instCR : CommRing self.R
• instDR : IsDedekindDomain self.R
• instCS : CommRing self.S
• instDS : IsDedekindDomain self.S
• instAlg : Algebra self.R self.S
• instNZ : NoZeroSMulDivisors self.R self.S
• X : CanonicalSheafCurves.SmoothCompleteCurve
• Y : CanonicalSheafCurves.SmoothCompleteCurve
• n : ℤ
• h_n_pos : 0 < self.n
• basePrimes : Finset (Ideal self.R)
• h_max (p : Ideal self.R) : p ∈ self.basePrimes → p.IsMaximal
• h_bot (p : Ideal self.R) : p ∈ self.basePrimes → p ≠ ⊥
• h_degK_formula : self.X.degK = self.n * self.Y.degK + globalRamification self.S self.basePrimes ⋯ ⋯

noncomputable def CurveCoveringDirect.deg_R (f : CurveCoveringDirect) : ℤ

Ramification degree of a CurveCoveringDirect.

theorem CurveCoveringDirect.deg_R_nonneg (f : CurveCoveringDirect) : 0 ≤ f.deg_R

Non-negativity of deg R for a CurveCoveringDirect.

theorem CurveCoveringDirect.degK_eq (f : CurveCoveringDirect) : f.X.degK = f.n * f.Y.degK + f.deg_R

Canonical-degree identity packaged in CurveCoveringDirect.

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

Riemann-Hurwitz for CurveCoveringDirect.

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

Solving Riemann-Hurwitz for deg R in CurveCoveringDirect.

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

Genus lower bound for CurveCoveringDirect.

theorem CurveCoveringDirect.etale_genus_exact (f : CurveCoveringDirect) (h : f.deg_R = 0) : f.X.g = f.n * (f.Y.g - 1) + 1

Exact étale formula for CurveCoveringDirect.

theorem CurveCoveringDirect.etale_double_cover_genus (f : CurveCoveringDirect) (h_etale : f.deg_R = 0) (h_double : f.n = 2) : f.X.g = 2 * f.Y.g - 1

Étale double covers in CurveCoveringDirect satisfy g_X = 2 g_Y - 1.

def CurveCovering.toDirect (f : CurveCovering) : CurveCoveringDirect

Forgetful map from the local CurveCovering data to the simpler CurveCoveringDirect.