Belyi polynomials and the three-point step of Belyi's theorem

For natural numbers m and n, the Belyi polynomial

B_{m,n} = ((m + n) ^ (m + n) / (m ^ m * n ^ n)) * X ^ m * (1 - X) ^ n

sends 0 and 1 to 0 (for m and n positive) and m / (m + n) to 1, and its derivative is a multiple of X ^ (m - 1) * (1 - X) ^ (n - 1) * (m - (m + n) * X). So its critical points lie in {0, 1, m / (m + n)} and its critical values lie in {0, 1}. The containment of critical points is strict when m = 1 or n = 1: B_{1,1} = 4 X (1 - X) has the single critical point 1 / 2.

Composing an affine normalization over ℚ with a Belyi polynomial sends three chosen rational points into {0, 1} without creating critical values outside {0, 1}. Inducting on the size of the set gives polynomial Belyification over ℚ: every finite set of rational numbers is carried into {0, 1} by a nonconstant polynomial with rational coefficients whose critical values, in every field of characteristic zero, lie in {0, 1}. Being a polynomial, it also fixes ∞.

Preceding it by Belyi's degree reduction (TauCeti.exists_polynomial_aeval_mem_range), which carries a finite set of algebraic numbers into ℚ by a polynomial over ℚ with rational critical values, gives polynomial Belyification of algebraic numbers: every finite set of elements algebraic over ℚ, such as a finite subset of AlgebraicClosure ℚ, is carried into {0, 1} by a nonconstant polynomial over ℚ with all its critical values in {0, 1}. In terms of the projective line, every finite S ⊆ ℙ¹(AlgebraicClosure ℚ) containing ∞ is sent into {0, 1, ∞} by a polynomial q ∈ ℚ[X], with q⁻¹(∞) = {∞} and every branch value of q in {0, 1, ∞}.

Main declarations

• TauCeti.belyiPolynomial: the Belyi polynomial B_{m,n} over a field; B_{1,1} is 4 X (1 - X) (TauCeti.belyiPolynomial_one_one), and in characteristic zero B_{m,0} is X ^ m (TauCeti.belyiPolynomial_zero_right).
• TauCeti.X_mul_one_sub_X_mul_derivative_belyiPolynomial: the derivative of B_{m,n}, multiplied by X (1 - X).
• TauCeti.rootSet_derivative_belyiPolynomial_subset: the critical points of B_{m,n} lie in {0, 1, m / (m + n)}.
• TauCeti.criticalValues_belyiPolynomial_subset: the critical values of B_{m,n} lie in {0, 1}.
• TauCeti.exists_polynomial_eval_mem_criticalValues_subset: polynomial Belyification of a finite set of rational numbers.
• TauCeti.exists_polynomial_aeval_mem_criticalValues_subset: polynomial Belyification of a finite set of algebraic numbers.

References

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

noncomputable def TauCeti.belyiPolynomial (K : Type u_1) [Field K] (m n : ℕ) : Polynomial K

The Belyi polynomial B_{m,n} = ((m + n) ^ (m + n) / (m ^ m * n ^ n)) * X ^ m * (1 - X) ^ n. In characteristic zero its normalizing constant makes its value at m / (m + n) equal to 1 (TauCeti.eval_div_belyiPolynomial).

@[simp]

theorem TauCeti.map_belyiPolynomial {K : Type u_1} [Field K] {L : Type u_2} [Field L] (f : K →+* L) (m n : ℕ) : Polynomial.map f (belyiPolynomial K m n) = belyiPolynomial L m n

The Belyi polynomial is preserved by every ring homomorphism of fields.

theorem TauCeti.belyiPolynomial_one_one {K : Type u_1} [Field K] : belyiPolynomial K 1 1 = Polynomial.C 4 * Polynomial.X * (1 - Polynomial.X)

The Belyi polynomial B_{1,1} is 4 X (1 - X).

theorem TauCeti.belyiPolynomial_zero_right {K : Type u_1} [Field K] [CharZero K] (m : ℕ) : belyiPolynomial K m 0 = Polynomial.X ^ m

In characteristic zero, the Belyi polynomial B_{m,0} is the power map X ^ m.

theorem TauCeti.eval_belyiPolynomial {K : Type u_1} [Field K] (m n : ℕ) (x : K) : Polynomial.eval x (belyiPolynomial K m n) = (↑m + ↑n) ^ (m + n) / (↑m ^ m * ↑n ^ n) * x ^ m * (1 - x) ^ n

The value of the Belyi polynomial at a point x.

@[simp]

theorem TauCeti.eval_zero_belyiPolynomial {K : Type u_1} [Field K] {m : ℕ} (hm : m ≠ 0) (n : ℕ) : Polynomial.eval 0 (belyiPolynomial K m n) = 0

For m ≠ 0, the Belyi polynomial vanishes at 0.

@[simp]

theorem TauCeti.eval_one_belyiPolynomial {K : Type u_1} [Field K] (m : ℕ) {n : ℕ} (hn : n ≠ 0) : Polynomial.eval 1 (belyiPolynomial K m n) = 0

For n ≠ 0, the Belyi polynomial vanishes at 1.

theorem TauCeti.X_mul_one_sub_X_mul_derivative_belyiPolynomial {K : Type u_1} [Field K] (m n : ℕ) : Polynomial.X * (1 - Polynomial.X) * Polynomial.derivative (belyiPolynomial K m n) = belyiPolynomial K m n * (Polynomial.C ↑m - Polynomial.C (↑m + ↑n) * Polynomial.X)

The derivative of the Belyi polynomial: X (1 - X) B′_{m,n} = B_{m,n} (m - (m + n) X). Multiplying by X (1 - X) avoids the exponents m - 1 and n - 1.

theorem TauCeti.belyiConstant_ne_zero {K : Type u_1} [Field K] [CharZero K] (m n : ℕ) : (↑m + ↑n) ^ (m + n) / (↑m ^ m * ↑n ^ n) ≠ 0

In characteristic zero, the normalizing constant (m + n) ^ (m + n) / (m ^ m * n ^ n) of the Belyi polynomial is nonzero.

@[simp]

theorem TauCeti.eval_div_belyiPolynomial {K : Type u_1} [Field K] [CharZero K] (m n : ℕ) : Polynomial.eval (↑m / (↑m + ↑n)) (belyiPolynomial K m n) = 1

In characteristic zero, the Belyi polynomial takes the value 1 at m / (m + n).

@[simp]

theorem TauCeti.natDegree_belyiPolynomial {K : Type u_1} [Field K] [CharZero K] (m n : ℕ) : (belyiPolynomial K m n).natDegree = m + n

In characteristic zero, the Belyi polynomial B_{m,n} has degree m + n.

theorem TauCeti.rootSet_derivative_belyiPolynomial_subset {K : Type u_1} [Field K] [CharZero K] (L : Type u_2) [Field L] [Algebra K L] (m n : ℕ) : (Polynomial.derivative (belyiPolynomial K m n)).rootSet L ⊆ {0, 1, ↑m / (↑m + ↑n)}

The critical points of the Belyi polynomial lie in {0, 1, m / (m + n)}. The containment is strict when m = 1 or n = 1.

theorem TauCeti.criticalValues_belyiPolynomial_subset {K : Type u_1} [Field K] [CharZero K] (L : Type u_2) [Field L] [Algebra K L] (m n : ℕ) : Polynomial.criticalValues L (belyiPolynomial K m n) ⊆ {0, 1}

The critical values of the Belyi polynomial lie in {0, 1}.

theorem TauCeti.exists_polynomial_eval_mem_criticalValues_subset (S : Finset ℚ) : ∃ (q : Polynomial ℚ), 0 < q.natDegree ∧ (∀ s ∈ S, Polynomial.eval s q ∈ {0, 1}) ∧ ∀ (L : Type u) [inst : Field L] [inst_1 : Algebra ℚ L], Polynomial.criticalValues L q ⊆ {0, 1}

Polynomial Belyification over ℚ. Every finite set S of rational numbers is carried into {0, 1} by a nonconstant polynomial q with rational coefficients whose critical values, in every field of characteristic zero, lie in {0, 1}.

theorem TauCeti.exists_polynomial_aeval_mem_criticalValues_subset {K : Type u_1} [Field K] [Algebra ℚ K] {S : Finset K} (hS : ∀ s ∈ S, IsIntegral ℚ s) : ∃ (q : Polynomial ℚ), 0 < q.natDegree ∧ (∀ s ∈ S, (Polynomial.aeval s) q ∈ {0, 1}) ∧ ∀ (L : Type u) [inst : Field L] [inst_1 : Algebra ℚ L], Polynomial.criticalValues L q ⊆ {0, 1}

Polynomial Belyification of algebraic numbers. Every finite set S of elements algebraic over ℚ in a field K, such as a finite subset of AlgebraicClosure ℚ, is carried into {0, 1} by a nonconstant polynomial q with rational coefficients whose critical values, in every field of characteristic zero, lie in {0, 1}.