theorem RiemannHurwitzApplications.genus_bound_cover_pos_genus (g_X g_Y n degR : ℤ) (hR : 0 ≤ degR) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) (_h_gY : g_Y ≥ 1) : g_X ≥ n * g_Y - (n - 1)

Genus lower bound for a degree-n cover of a positive-genus target: g_X ≥ n · g_Y − (n − 1), an immediate consequence of Riemann–Hurwitz with deg R ≥ 0.

theorem RiemannHurwitzApplications.genus_bound_cover_pos_genus_alt (g_X g_Y n degR : ℤ) (hR : 0 ≤ degR) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) : g_X ≥ n * (g_Y - 1) + 1

Reformulation of the genus bound: g_X ≥ n(g_Y − 1) + 1.

theorem RiemannHurwitzApplications.genus_bound_cover_gY_ge_1_CurveCover (f : RiemannHurwitzDegree.CurveCoverData) (_h_gY : f.target.g ≥ 1) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : f.source.g ≥ f.morphism.degree * f.target.g - (f.morphism.degree - 1)

Bundled form of the genus bound for CurveCoverData with g_Y ≥ 1.

theorem RiemannHurwitzApplications.genus_cover_ge_target_genus (g_X g_Y n degR : ℤ) (hR : 0 ≤ degR) (hn : n ≥ 1) (h_gY : g_Y ≥ 1) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) : g_X ≥ g_Y

For a cover of a positive-genus curve, the source genus dominates the target genus: g_X ≥ g_Y.

theorem RiemannHurwitzApplications.genus_cover_strict_inequality (g_X g_Y n degR : ℤ) (hR : 0 ≤ degR) (hn : n ≥ 2) (h_gY : g_Y ≥ 2) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) : g_X > g_Y

Strict genus inequality g_X > g_Y for a degree-≥ 2 cover of a curve of general type (g_Y ≥ 2).

theorem RiemannHurwitzApplications.genus_cover_strict_inequality_CurveCover (f : RiemannHurwitzDegree.CurveCoverData) (hn : f.morphism.degree ≥ 2) (h_gY : f.target.g ≥ 2) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : f.source.g > f.target.g

Bundled form: strict genus inequality for a degree-≥ 2 cover of a curve of general type.

theorem RiemannHurwitzApplications.genus_etale_cover_exact (g_X g_Y n : ℤ) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + 0) : g_X = n * (g_Y - 1) + 1

Étale cover (no ramification): the Riemann–Hurwitz formula degenerates to the exact relation g_X = n(g_Y − 1) + 1.

theorem RiemannHurwitzApplications.luroth_theorem_target_genus_zero (g_Y n degR : ℤ) (hR : 0 ≤ degR) (hn : n ≥ 1) (hgY : g_Y ≥ 0) (h_RH : 2 * 0 - 2 = n * (2 * g_Y - 2) + degR) : g_Y = 0

Lüroth's theorem (target-side): a cover of ℙ¹ (g_X = 0) forces the target to have genus zero, g_Y = 0.

theorem RiemannHurwitzApplications.ramification_formula_genus_zero (n degR : ℤ) (h_RH : 2 * 0 - 2 = n * (2 * 0 - 2) + degR) : degR = 2 * (n - 1)

For ℙ¹ → ℙ¹ of degree n, the ramification divisor has degree 2(n−1).

theorem RiemannHurwitzApplications.degree_one_unramified_genus_zero (degR : ℤ) (h_RH : 2 * 0 - 2 = 1 * (2 * 0 - 2) + degR) : degR = 0

A degree-1 cover ℙ¹ → ℙ¹ (an isomorphism) is unramified: deg R = 0.

theorem RiemannHurwitzApplications.luroth_target_genus_zero_CurveCover (f : RiemannHurwitzDegree.CurveCoverData) (h_gX : f.source.g = 0) (hn : f.morphism.degree ≥ 1) (hgY : f.target.g ≥ 0) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : f.target.g = 0

Bundled Lüroth's theorem for CurveCoverData.

theorem RiemannHurwitzApplications.ramification_formula_CurveCover (f : RiemannHurwitzDegree.CurveCoverData) (h_gX : f.source.g = 0) (h_gY : f.target.g = 0) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : f.morphism.deg_R = 2 * (f.morphism.degree - 1)

Bundled version of the ramification formula deg R = 2(n − 1) for covers of ℙ¹ by ℙ¹.

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

For an arbitrary cover of ℙ¹, 2 g_X = deg R − 2n + 2.

theorem RiemannHurwitzApplications.genus_zero_implies_degK_neg2 (C : CanonicalSheafCurves.SmoothCompleteCurve) (h : C.g = 0) : C.degK = -2

A genus-zero smooth complete curve has canonical degree −2.

theorem RiemannHurwitzApplications.genus_zero_degK_eq_P1 (C : CanonicalSheafCurves.SmoothCompleteCurve) (h : C.g = 0) : C.degK = (CanonicalSheafCurves.mkCurve 0).degK

A genus-zero curve has the same canonical degree as ℙ¹.

theorem RiemannHurwitzApplications.genus_zero_numerical_invariants (C : CanonicalSheafCurves.SmoothCompleteCurve) (h : C.g = 0) : C.g = (CanonicalSheafCurves.mkCurve 0).g ∧ C.degK = (CanonicalSheafCurves.mkCurve 0).degK

A genus-zero curve shares the genus and canonical degree of ℙ¹, i.e. its numerical invariants.

theorem RiemannHurwitzApplications.genus_zero_unique_numerical (C C' : CanonicalSheafCurves.SmoothCompleteCurve) (hC : C.g = 0) (hC' : C'.g = 0) : C.g = C'.g ∧ C.degK = C'.degK

Two genus-zero curves have the same numerical invariants (genus and canonical degree).

theorem RiemannHurwitzApplications.genus_zero_cover_data (f : RiemannHurwitzDegree.CurveCoverData) (h_gX : f.source.g = 0) (hn : f.morphism.degree ≥ 1) (hgY : f.target.g ≥ 0) (h_decomp : f.morphism.deg_KX = f.morphism.degree * f.morphism.deg_KY + f.morphism.deg_R) : f.target.g = 0 ∧ f.morphism.deg_R = 2 * (f.morphism.degree - 1)

Combined statement: a genus-zero cover forces the target to be ℙ¹ (i.e. g_Y = 0) and the ramification divisor to satisfy deg R = 2(n − 1).

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

Specialization to a target ℙ¹: 2 g_X = deg R − 2n + 2.

theorem RiemannHurwitzApplications.genus_formula_target_elliptic (g_X n degR : ℤ) (hR : 0 ≤ degR) (h_RH : 2 * g_X - 2 = n * (2 * 1 - 2) + degR) : g_X ≥ 1

For a cover of an elliptic curve (g_Y = 1), the source has g_X ≥ 1.

theorem RiemannHurwitzApplications.etale_cover_elliptic_genus (g_X n : ℤ) (h_RH : 2 * g_X - 2 = n * (2 * 1 - 2) + 0) : g_X = 1

An étale cover of an elliptic curve is itself elliptic: g_X = 1.

theorem RiemannHurwitzApplications.genus_ge_2_for_cover_of_general_type (g_X g_Y n degR : ℤ) (hR : 0 ≤ degR) (hn : n ≥ 1) (h_gY : g_Y ≥ 2) (h_RH : 2 * g_X - 2 = n * (2 * g_Y - 2) + degR) : g_X ≥ 2

A cover of a general-type curve (g_Y ≥ 2) has genus g_X ≥ 2.

structure RiemannHurwitzApplications.NormalDomainLocalizationData (R : Type u_1) [CommRing R] [IsDomain R] : Prop

Prop 39 (Lec, normal domain criterion): the data needed to express integrality of a fraction in terms of local conditions at height-one primes.

• isIntegrallyClosed : IsIntegrallyClosed R
• intersection_property (a b : R) : b ≠ 0 → (∀ (p : Ideal R), p.IsPrime → p ≠ ⊥ → p.height ≤ 1 → ∃ (r : R), ∃ s ∉ p, a * s = b * r) → ∃ (q : R), a = b * q

def RiemannHurwitzApplications.NormalDomainLocalizationData.ofDedekind (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : NormalDomainLocalizationData R

Dedekind domains canonically satisfy the normal-domain localization property: an algebraic Hartogs-type construction recovers the global element from compatible local fractions.

theorem RiemannHurwitzApplications.normal_domain_element_criterion (R : Type u_1) [CommRing R] [IsDomain R] (hR : NormalDomainLocalizationData R) (a b : R) (hb : b ≠ 0) (h_local : ∀ (p : Ideal R), p.IsPrime → p ≠ ⊥ → p.height ≤ 1 → ∃ (r : R), ∃ s ∉ p, a * s = b * r) : ∃ (q : R), a = b * q

The element-criterion form of Prop 39: divisibility b ∣ a holds globally iff it holds at every height-one prime.

theorem RiemannHurwitzApplications.dedekind_normal_domain (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] : IsIntegrallyClosed R

Every Dedekind domain is integrally closed (a normal domain).