Documentation

TauCeti.Analysis.Complex.RiemannSurface.Polynomial

Polynomial maps of the Riemann sphere #

A nonconstant complex polynomial p of degree d extends to the Riemann sphere OnePoint ℂ by sending ∞ to ∞; this extension is Mathlib's OnePoint.map. In the affine chart it is z ↦ p(z). In the inverted chart at ∞ it is w ↦ w ^ d / q(w), where q = p.reverse is the reversed polynomial, q(w) = w ^ d p(w⁻¹) for w ≠ 0, whose value at 0 is the leading coefficient of p. So the extension is holomorphic, and its local multiplicity is d at ∞. At a finite point z the local multiplicity is the multiplicity of z as a root of p - p(z), and it exceeds 1 exactly when z is a critical point of p, a root of the derivative.

The fibre over ∞ is the single point ∞, so the degree of the extension is d, and its branch values lie in ∞ together with the critical values of p. When d ≥ 2 they are exactly ∞ together with the critical values; when d = 1 the extension is a Möbius transformation and has no branch values. These are the polynomial branched covers of the sphere, among them the power maps z ↦ z ^ n and the polynomial Belyi maps.

Main declarations #

References #

source
theorem TauCeti.RiemannSurface.invChart_onePointMap_eval_invChart_symm {p : Polynomial ℂ} (hp : 0 < p.natDegree) (w : ℂ) :
↑OnePoint.invChart (OnePoint.map (fun (z : ℂ) => Polynomial.eval z p) (↑OnePoint.invChart.symm w)) = w ^ p.natDegree / Polynomial.eval w p.reverse

In the inverted chart at ∞, the extension of a nonconstant polynomial p to the Riemann sphere is w ↦ w ^ d / p.reverse.eval w, where d is the degree of p.

source
theorem TauCeti.RiemannSurface.continuous_onePointMap_eval {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
Continuous (OnePoint.map fun (z : ℂ) => Polynomial.eval z p)

Polynomial maps of the Riemann sphere are continuous. The extension of a nonconstant polynomial to OnePoint ℂ, sending ∞ to ∞, is continuous: a polynomial tends to infinity at infinity.

source
theorem TauCeti.RiemannSurface.mdifferentiable_onePointMap_eval {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
MDiff (OnePoint.map fun (z : ℂ) => Polynomial.eval z p)

Polynomial maps of the Riemann sphere are holomorphic. The extension of a nonconstant polynomial to OnePoint ℂ, sending ∞ to ∞, is holomorphic.

source
theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_eval_coe {p : Polynomial ℂ} (hp : 0 < p.natDegree) (z : ℂ) :
localMultiplicity (OnePoint.map fun (z : ℂ) => Polynomial.eval z p) ↑z = Polynomial.rootMultiplicity z (p - Polynomial.C (Polynomial.eval z p))

At a finite point z, the local multiplicity of the extension of a nonconstant polynomial p to the Riemann sphere is the multiplicity of z as a root of p - p(z).

source
theorem TauCeti.RiemannSurface.one_lt_localMultiplicity_onePointMap_eval_coe_iff {p : Polynomial ℂ} (hp : 0 < p.natDegree) {z : ℂ} :
1 < localMultiplicity (OnePoint.map fun (z : ℂ) => Polynomial.eval z p) ↑z ↔ (Polynomial.derivative p).IsRoot z

At a finite point z, the extension of a nonconstant polynomial p to the Riemann sphere has local multiplicity greater than 1 exactly when z is a critical point of p.

source
theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_eval_coe_of_not_isRoot {p : Polynomial ℂ} (hp : 0 < p.natDegree) {z : ℂ} (hz : ¬(Polynomial.derivative p).IsRoot z) :
localMultiplicity (OnePoint.map fun (z : ℂ) => Polynomial.eval z p) ↑z = 1

Away from the critical points of a nonconstant polynomial p, its extension to the Riemann sphere has local multiplicity 1.

source
@[simp]
theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_eval_infty {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
localMultiplicity (OnePoint.map fun (z : ℂ) => Polynomial.eval z p) OnePoint.infty = p.natDegree

The extension of a nonconstant polynomial p to the Riemann sphere has local multiplicity the degree of p at ∞, where it is w ↦ w ^ d / p.reverse.eval w in the inverted chart.

source
noncomputable def TauCeti.RiemannSurface.FiniteHolomorphicMap.spherePolynomial {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
FiniteHolomorphicMap (OnePoint ℂ) (OnePoint ℂ)

The extension of a nonconstant polynomial p to the Riemann sphere, sending ∞ to ∞, as a finite holomorphic map.

Instances For
    source
    @[simp]
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.coe_spherePolynomial {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
    ↑(spherePolynomial hp) = OnePoint.map fun (z : ℂ) => Polynomial.eval z p
    source
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues_spherePolynomial_subset {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
    (spherePolynomial hp).branchValues ⊆ insert OnePoint.infty (OnePoint.some '' Polynomial.criticalValues ℂ p)

    The branch values of the extension of a nonconstant polynomial p to the Riemann sphere lie in {∞} together with the critical values of p.

    source
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues_spherePolynomial {p : Polynomial ℂ} (hp : 1 < p.natDegree) :
    (spherePolynomial ⋯).branchValues = insert OnePoint.infty (OnePoint.some '' Polynomial.criticalValues ℂ p)

    The branch values of a polynomial map of the Riemann sphere. For a polynomial p of degree at least 2, the branch values of its extension to the Riemann sphere are exactly ∞, where the local multiplicity is the degree, together with the critical values of p.

    source
    @[simp]
    theorem TauCeti.RiemannSurface.degree_onePointMap_eval {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
    degree (OnePoint.map fun (z : ℂ) => Polynomial.eval z p) = p.natDegree

    The extension of a nonconstant polynomial p to the Riemann sphere has degree the degree of p: its fibre over ∞ is the single point ∞, of local multiplicity the degree of p.