Critical values of polynomials

The critical values of a polynomial p with coefficients in R, computed in an R-algebra S that is a domain, are the values p(x) at the roots x ∈ S of the derivative p′. Over an algebraically closed field of characteristic zero they are the finite branch values of the map x ↦ p(x) of the projective line; the point at infinity, over which a polynomial of degree at least two is always ramified, is not part of this set.

Following Mathlib's Polynomial.rootSet, the roots of the zero polynomial form the empty set, so a polynomial with vanishing derivative has no critical values.

The chain rule (p ∘ q)′ = (p′ ∘ q) · q′ gives the bookkeeping for composites used in Belyi's construction: the critical values of p ∘ q lie in the image under p of the critical values of q together with the critical values of p, with equality over an algebraically closed field of characteristic zero when p and q are nonconstant.

Main declarations

• Polynomial.criticalValues: the critical values of p in S.
• Polynomial.mem_criticalValues_self_iff: membership in the critical values of a polynomial over a domain, computed in the domain itself, via roots of p′.
• Polynomial.criticalValues_comp_subset: the critical values of a composite.
• Polynomial.criticalValues_comp: equality for nonconstant polynomials over a field of characteristic zero, computed in an algebraically closed field.
• Polynomial.algebraMap_mem_criticalValues_of_isAlgClosed: a critical value lying in the coefficient field, attained in some field extension, is attained in every algebraically closed one.

References

• Joseph H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009, Exercise 1.12 and its hint.
• Bernhard Köck, Belyi's theorem revisited, Beiträge zur Algebra und Geometrie 45 (2004), 253–265, §3.

noncomputable def Polynomial.criticalValues {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (p : Polynomial R) : Set S

The critical values of p in S: the values of p at the roots of its derivative in S. When S is an algebraically closed field of characteristic zero, these are the finite branch values of p regarded as a self-map of the projective line.

theorem Polynomial.criticalValues_def {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (p : Polynomial R) : criticalValues S p = (fun (x : S) => (aeval x) p) '' (derivative p).rootSet S

The critical values of p are the image of the roots of p′ under x ↦ p(x).

@[simp]

theorem Polynomial.mem_criticalValues {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {p : Polynomial R} {y : S} : y ∈ criticalValues S p ↔ ∃ x ∈ (derivative p).rootSet S, (aeval x) p = y

theorem Polynomial.mem_criticalValues_self_iff {S : Type u_2} [CommRing S] [IsDomain S] {p : Polynomial S} (hp : derivative p ≠ 0) {y : S} : y ∈ criticalValues S p ↔ ∃ (x : S), (derivative p).IsRoot x ∧ eval x p = y

For a polynomial over a domain with nonzero derivative, its critical values in the domain itself are the values p(x) at the roots x of p′.

theorem Polynomial.aeval_mem_criticalValues {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {p : Polynomial R} {x : S} (hx : x ∈ (derivative p).rootSet S) : (aeval x) p ∈ criticalValues S p

theorem Polynomial.criticalValues_finite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (p : Polynomial R) : (criticalValues S p).Finite

theorem Polynomial.criticalValues_eq_empty_of_natDegree_le_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {p : Polynomial R} (hp : p.natDegree ≤ 1) : criticalValues S p = ∅

A polynomial of degree at most one has no critical values.

@[simp]

theorem Polynomial.criticalValues_C {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (a : R) : criticalValues S (C a) = ∅

@[simp]

theorem Polynomial.criticalValues_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] : criticalValues S X = ∅

@[simp]

theorem Polynomial.criticalValues_map {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {T : Type u_3} [CommRing T] [Algebra R T] [Algebra T S] [IsScalarTower R T S] (p : Polynomial R) : criticalValues S (map (algebraMap R T) p) = criticalValues S p

Critical values are unchanged by first extending the coefficients along a scalar tower.

theorem Polynomial.criticalValues_comp_subset {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (p q : Polynomial R) : criticalValues S (p.comp q) ⊆ (fun (y : S) => (aeval y) p) '' criticalValues S q ∪ criticalValues S p

The critical values of p ∘ q lie in the image under p of the critical values of q, together with the critical values of p.

theorem Polynomial.criticalValues_comp {K : Type u_3} {L : Type u_4} [Field K] [CharZero K] [Field L] [IsAlgClosed L] [Algebra K L] {p q : Polynomial K} (hp : 0 < p.natDegree) (hq : 0 < q.natDegree) : criticalValues L (p.comp q) = (fun (y : L) => (aeval y) p) '' criticalValues L q ∪ criticalValues L p

Over a field of characteristic zero, computed in an algebraically closed field, the critical values of a composite of nonconstant polynomials are the image under p of the critical values of q, together with the critical values of p.

theorem Polynomial.algebraMap_mem_criticalValues_of_isAlgClosed {K : Type u_3} {L : Type u_4} {Ω : Type u_5} [Field K] [Field L] [Field Ω] [IsAlgClosed Ω] [Algebra K L] [Algebra K Ω] {p : Polynomial K} {c : K} (h : (algebraMap K L) c ∈ criticalValues L p) : (algebraMap K Ω) c ∈ criticalValues Ω p

A critical value of p ∈ K[X] that lies in K and is attained at a critical point in some field extension L of K is also a critical value of p in every algebraically closed field extension Ω of K.