Every curve over an algebraic extension of ℚ admits a Belyi map

Belyi's theorem, existence direction: let k be a field algebraic over ℚ, such as a number field or an algebraic closure of ℚ, and let F / k be a function field with exact constant field k. Then F admits a Belyi map: there is β ∈ F transcendental over k such that F / k(β) is unramified outside β = 0, β = 1 and β = ∞, that is, F over k(t) with t ↦ β is an algebraic Belyi pair. Moreover β can be taken to be q(x) for any transcendental x ∈ F and a suitable nonconstant polynomial q with rational coefficients.

The proof composes the map x : F → ℙ¹ with a polynomial. The extension F / k(x) is ramified over only finitely many places (TauCeti.Place.finite_setOf_ramificationIdx_ne_one), and at each of them x either has a pole or takes a value algebraic over k, hence over ℚ. Polynomial Belyification of algebraic numbers (TauCeti.exists_polynomial_aeval_mem_criticalValues_subset) gives a nonconstant q ∈ ℚ[X] carrying these finitely many values into {0, 1} and whose critical values all lie in {0, 1}. Then t = q(x) works: k(x) / k(t) is a Belyi pair (TauCeti.IsAlgebraicBelyiPair.of_criticalValues_subset), and above a place of k(t) outside 0, 1 and ∞ the function x is regular with a value not sent into {0, 1}, so F / k(x) is unramified there. Ramification indices multiply in the tower k(t) ⊆ k(x) ⊆ F (TauCeti.IsAlgebraicBelyiPair.of_isScalarTower).

Main results

• TauCeti.IsFunctionField.exists_polynomial_isAlgebraicBelyiPair: for every transcendental x ∈ F there is a nonconstant q ∈ ℚ[X] such that t ↦ q(x) is a Belyi map.
• TauCeti.IsFunctionField.exists_isAlgebraicBelyiPair: F admits a Belyi map.

References

• G. V. Belyi, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276.
• B. Köck, Belyi's theorem revisited, Beiträge zur Algebra und Geometrie 45 (2004), 253–265, §3.
• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, LMS Student Texts 79, Cambridge University Press, 2012, §3.1.

theorem TauCeti.IsFunctionField.exists_polynomial_isAlgebraicBelyiPair {k : Type u} {F : Type v} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra.IsAlgebraic ℚ k] (hF : IsFunctionField k F) (hc : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) : ∃ (q : Polynomial ℚ), 0 < q.natDegree ∧ ∀ [inst : Algebra (RatFunc k) F] [inst_1 : IsScalarTower k (RatFunc k) F] [inst_2 : FiniteDimensional (RatFunc k) F], (algebraMap (RatFunc k) F) RatFunc.X = (Polynomial.aeval x) (Polynomial.map (algebraMap ℚ k) q) → IsAlgebraicBelyiPair k F

Belyi's theorem, existence direction, for a given function: over a field k algebraic over ℚ, let F / k be a function field with exact constant field k and x ∈ F transcendental over k. Then there is a nonconstant polynomial q with rational coefficients such that F is an algebraic Belyi pair over k(t) for every structure in which t acts as q(x): the composite of x with q is a Belyi map. Such a structure exists, see TauCeti.IsFunctionField.exists_isAlgebraicBelyiPair.

theorem TauCeti.IsFunctionField.exists_isAlgebraicBelyiPair {k : Type u} {F : Type v} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra.IsAlgebraic ℚ k] (hF : IsFunctionField k F) (hc : IsIntegrallyClosedIn k F) : ∃ (β : F) (hβ : Transcendental k β), IsAlgebraicBelyiPair k F

Belyi's theorem, existence direction: over a field k algebraic over ℚ, such as an algebraic closure of ℚ or a number field, every function field F / k with exact constant field k admits a Belyi map: there is β ∈ F transcendental over k such that F over k(t), with t acting as β, is an algebraic Belyi pair.