Belyi's degree reduction

Let F be a perfect field, for instance ℚ. Every finite set S of elements algebraic over F is carried into F by a polynomial q ∈ F[X] with nonzero derivative whose critical values, the values of q at the roots of q′ in any field extension, also lie in F. This is the first half of Belyi's construction of a Belyi map on a curve over AlgebraicClosure ℚ. A polynomial also fixes ∞, so a finite subset of ℙ¹(AlgebraicClosure ℚ) is carried into ℙ¹(ℚ) together with the critical values of q.

Main results

• TauCeti.exists_irreducible_finset_dvd_comp: the degree-reduction step.
• TauCeti.exists_forall_dvd_sub_C: for a finite set P of irreducible polynomials, a polynomial q with q′ ≠ 0 that is constant modulo every member of P and modulo every irreducible factor of q′.
• TauCeti.exists_polynomial_aeval_mem_range: the same statement for a finite set of algebraic elements of a field extension, with the critical values of q taken in an arbitrary field extension.

Implementation notes

The set S is replaced by the finite set of minimal polynomials of its elements, which records its closure under conjugation over F. A root of an irreducible r ∈ F[X] is mapped by a polynomial μ into the root set of an irreducible p' exactly when r ∣ p'.comp μ, and q takes a value c ∈ F at the roots of r exactly when r ∣ q - C c. All statements are made in these terms over F and transferred to elements of field extensions at the end.

The degree-reduction step: if μ has the largest degree d ≥ 2 among the polynomials in such a set P, then μ maps the roots of P, together with the roots of μ′, into the roots of a new finite set P' of irreducible polynomials of degree at most d, with strictly fewer of degree exactly d. Indeed the roots of μ go to 0, every root of any polynomial in P goes to a point of no larger degree, and the roots of μ′ have degree at most d - 1 since μ′ ≠ 0 (here perfectness is used). The well-founded measure of the induction is therefore the pair (largest degree d, number of members of degree d), ordered lexicographically. The cardinality of the root set alone need not drop: X ^ 2 - 2 sends {√2, -√2} to {0} and adds its critical value -2.

References

• G. V. Belyi, On Galois extensions of a maximal cyclotomic field, Math. USSR Izv. 14 (1980).
• B. Köck, Belyi's theorem revisited, Beiträge Algebra Geom. 45 (2004), Lemma 3.5.

theorem TauCeti.exists_irreducible_finset_dvd_comp {F : Type u_1} [Field F] {P : Finset (Polynomial F)} (hP : ∀ p ∈ P, Irreducible p) {μ : Polynomial F} (hμ : μ ∈ P) (hμ' : Polynomial.derivative μ ≠ 0) (hdeg : ∀ p ∈ P, p.natDegree ≤ μ.natDegree) (hμ2 : 2 ≤ μ.natDegree) : ∃ (P' : Finset (Polynomial F)), (∀ p ∈ P', Irreducible p) ∧ (∀ p ∈ P', p.natDegree ≤ μ.natDegree) ∧ {p ∈ P' | p.natDegree = μ.natDegree}.card < {p ∈ P | p.natDegree = μ.natDegree}.card ∧ (∀ p ∈ P, ∃ p' ∈ P', p ∣ p'.comp μ) ∧ ∀ (r : Polynomial F), Irreducible r → r ∣ Polynomial.derivative μ → ∃ p' ∈ P', r ∣ p'.comp μ

The degree-reduction step. Let P be a finite set of irreducible polynomials, and let μ ∈ P, with μ′ ≠ 0, have the largest degree d ≥ 2 in P. Then there is a finite set P' of irreducible polynomials of degree at most d, with fewer members of degree d than P, such that μ maps the roots of every member of P, and the roots of μ′, into the roots of members of P'. Over a perfect field the hypothesis μ′ ≠ 0 holds for every irreducible μ.

theorem TauCeti.exists_forall_dvd_sub_C {F : Type u_1} [Field F] [PerfectField F] {P : Finset (Polynomial F)} (hP : ∀ p ∈ P, Irreducible p) : ∃ (q : Polynomial F), Polynomial.derivative q ≠ 0 ∧ (∀ p ∈ P, ∃ (c : F), p ∣ q - Polynomial.C c) ∧ ∀ (r : Polynomial F), Irreducible r → r ∣ Polynomial.derivative q → ∃ (c : F), r ∣ q - Polynomial.C c

Belyi's degree reduction over F. For a finite set P of irreducible polynomials over a perfect field F, there is a polynomial q ∈ F[X] with q′ ≠ 0 that is constant modulo every member of P and modulo every irreducible factor of q′: at the roots of each of these, in any field extension, q takes a value in F.

theorem TauCeti.exists_polynomial_aeval_mem_range {F : Type u_1} [Field F] [PerfectField F] {K : Type u_2} [Field K] [Algebra F K] {S : Finset K} (hS : ∀ s ∈ S, IsIntegral F s) : ∃ (q : Polynomial F), Polynomial.derivative q ≠ 0 ∧ (∀ s ∈ S, (Polynomial.aeval s) q ∈ Set.range ⇑(algebraMap F K)) ∧ ∀ (L : Type w) [inst : Field L] [inst_1 : Algebra F L] (x : L), (Polynomial.aeval x) (Polynomial.derivative q) = 0 → (Polynomial.aeval x) q ∈ Set.range ⇑(algebraMap F L)

Belyi's degree reduction. Every finite set S of elements algebraic over a perfect field F, such as a finite subset of AlgebraicClosure ℚ, is carried into F by a polynomial q ∈ F[X] with q′ ≠ 0, in particular nonconstant, whose critical values in every field extension of F also lie in F.