noncomputable def CurveCovering.toCurveMorphismData (C : CurveCovering) : RiemannHurwitzFormula.CurveMorphismData

Convert a CurveCovering into the abstract CurveMorphismData used by the Riemann–Hurwitz formula, by packaging degree, canonical degrees, and ramification.

theorem CurveCovering.toCurveMorphismData_satisfies_RH (C : CurveCovering) : C.toCurveMorphismData.deg_KX = C.toCurveMorphismData.degree * C.toCurveMorphismData.deg_KY + C.toCurveMorphismData.deg_R

The packaged CurveMorphismData of a CurveCovering satisfies the Riemann–Hurwitz identity deg K_X = n · deg K_Y + deg R.

theorem CurveCovering.ellipticIdentity_morphismData : ellipticIdentity.toCurveMorphismData.degree = 1 ∧ ellipticIdentity.toCurveMorphismData.deg_R = 0

For the elliptic identity covering, the morphism data has degree 1 and ramification divisor of degree 0.

theorem CurveCovering.ellipticIdentity_toCurveMorphismData_RH : ellipticIdentity.toCurveMorphismData.deg_KX = ellipticIdentity.toCurveMorphismData.degree * ellipticIdentity.toCurveMorphismData.deg_KY + ellipticIdentity.toCurveMorphismData.deg_R

The Riemann–Hurwitz identity instantiated on the elliptic identity covering.

noncomputable def CurveCovering.toCurveCoverData (C : CurveCovering) : RiemannHurwitzDegree.CurveCoverData

Package a CurveCovering as CurveCoverData, combining the morphism data with the source and target curves.

theorem CurveCovering.toCurveCoverData_satisfies_decomp (C : CurveCovering) : C.toCurveCoverData.morphism.deg_KX = C.toCurveCoverData.morphism.degree * C.toCurveCoverData.morphism.deg_KY + C.toCurveCoverData.morphism.deg_R

The cover data of a CurveCovering satisfies the canonical-divisor decomposition underlying the Riemann–Hurwitz formula.

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

Riemann–Hurwitz genus form derived via the cover-data bridge: 2g_X - 2 = n · (2g_Y - 2) + deg R.

theorem CurveCovering.genus_lower_bound_via_bridge (C : CurveCovering) : 2 * C.X.g - 2 ≥ C.n * (2 * C.Y.g - 2)

Lower bound on the genus arising from a covering, obtained from the bridge: 2g_X - 2 ≥ n · (2g_Y - 2) (since deg R ≥ 0).

theorem CurveCovering.bridge_agrees_with_direct (C : CurveCovering) : ⋯ = ⋯

The genus formula proved via the bridge agrees with the direct Riemann–Hurwitz formula.