The map z ↦ 4z(1 - z) of the Riemann sphere

The polynomial 4X(1 - X) has degree 2, so its extension to the Riemann sphere OnePoint ℂ, sending ∞ to ∞, is a holomorphic map of degree 2. Its only finite critical point is 1/2, with critical value 1, so its branch values are 1 and ∞. Its fibre over 0 is the two points 0 and 1, where it is unramified; its fibres over 1 and ∞ are the single points 1/2 and ∞, where it is ramified of index 2. So its ramification partitions over 0, 1 and ∞ are [1, 1], [2] and [2]. All of this is read off from the general facts about polynomial maps of the sphere in TauCeti.Analysis.Complex.RiemannSurface.Polynomial.

This is the map z ↦ (1 - T₂(1 - 2z)) / 2 for the Chebyshev polynomial T₂ = 2x² - 1, one of the basic examples of a Belyi map.

Main declarations

• TauCeti.RiemannSurface.degree_onePointMap_four_mul_mul_one_sub: the map has degree 2.
• TauCeti.RiemannSurface.preimage_onePointMap_four_mul_mul_one_sub_zero and TauCeti.RiemannSurface.preimage_onePointMap_four_mul_mul_one_sub_one: its fibres are {0, 1} over 0 and {1/2} over 1.
• TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_coe_of_ne, TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_half and TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_infty: its local multiplicity is 1 away from 1/2 and ∞, and 2 at those two points.
• TauCeti.RiemannSurface.branchValues_spherePolynomial_four_mul_X_mul_one_sub_X: its branch values are 1 and ∞.

theorem TauCeti.RiemannSurface.natDegree_four_mul_X_mul_one_sub_X : (Polynomial.C 4 * Polynomial.X * (1 - Polynomial.X)).natDegree = 2

The polynomial 4X(1 - X) has degree 2.

theorem TauCeti.RiemannSurface.natDegree_four_mul_X_mul_one_sub_X_pos : 0 < (Polynomial.C 4 * Polynomial.X * (1 - Polynomial.X)).natDegree

The polynomial 4X(1 - X) is nonconstant.

theorem TauCeti.RiemannSurface.onePointMap_eval_four_mul_X_mul_one_sub_X : (OnePoint.map fun (z : ℂ) => Polynomial.eval z (Polynomial.C 4 * Polynomial.X * (1 - Polynomial.X))) = OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)

The extension of 4X(1 - X) to the Riemann sphere is the extension of z ↦ 4z(1 - z).

theorem TauCeti.RiemannSurface.isRoot_derivative_four_mul_X_mul_one_sub_X_iff {z : ℂ} : (Polynomial.derivative (Polynomial.C 4 * Polynomial.X * (1 - Polynomial.X))).IsRoot z ↔ z = 2⁻¹

The derivative 4 - 8z of 4z(1 - z) vanishes only at 1/2.

@[simp]

theorem TauCeti.RiemannSurface.degree_onePointMap_four_mul_mul_one_sub : degree (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) = 2

The map z ↦ 4z(1 - z) of the Riemann sphere has degree 2.

theorem TauCeti.RiemannSurface.preimage_onePointMap_four_mul_mul_one_sub_zero : (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) ⁻¹' {↑0} = {↑0, ↑1}

The fibre of z ↦ 4z(1 - z) over 0 consists of the two points 0 and 1.

theorem TauCeti.RiemannSurface.preimage_onePointMap_four_mul_mul_one_sub_one : (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) ⁻¹' {↑1} = {↑2⁻¹}

The fibre of z ↦ 4z(1 - z) over 1 is the single point 1/2.

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_coe_of_ne {z : ℂ} (hz : z ≠ 2⁻¹) : localMultiplicity (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) ↑z = 1

The map z ↦ 4z(1 - z) is unramified away from 1/2 and ∞, in particular at the two points 0 and 1 over 0.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_half : localMultiplicity (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) ↑2⁻¹ = 2

The map z ↦ 4z(1 - z) is ramified of index 2 at 1/2, the only point over 1.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_four_mul_mul_one_sub_infty : localMultiplicity (OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)) OnePoint.infty = 2

The map z ↦ 4z(1 - z) is ramified of index 2 at ∞, the only point over ∞.

theorem TauCeti.RiemannSurface.branchValues_spherePolynomial_four_mul_X_mul_one_sub_X : (FiniteHolomorphicMap.spherePolynomial natDegree_four_mul_X_mul_one_sub_X_pos).branchValues = {↑1, OnePoint.infty}

The branch values of z ↦ 4z(1 - z) are exactly 1 and ∞: its only finite critical point is 1/2, with critical value 1.