The superelliptic cover y ^ 4 = t (t - 1) of the thrice-punctured sphere

The affine curve y ^ 4 = t (t - 1) maps to the t-line, and over the thrice-punctured sphere U = ℂ ∖ {0, 1} its points form the space TauCeti.ThricePuncturedSphere.superellipticCurve of pairs (t, y) with t ∈ U. The projection (t, y) ↦ t is the unbranched part of the Belyi map β = t of the compact superelliptic curve, a curve of genus one. This file reads off the topology of this cover directly from the equation, and identifies its monodromy with the Euclidean torus triple TauCeti.PermutationTriple.torusTriple.

• A four-sheeted cover. Over t ∈ U the radicand t (t - 1) is nonzero, so the quartic Y ^ 4 - t (t - 1) is separable and the fibre is its four roots. The projection is therefore a covering map, as the root space of a separable family of polynomials.
• The cyclic deck action. The fourth roots of unity act by y ↦ ζ y over U, freely and transitively on each fibre, so the projection is the quotient covering by this action.
• One sheet over 0 and over 1. Over the standard punctured disc 0 < |t| < 1/2, the map w ↦ (w ^ 4 / 2, c w (1 - w ^ 4 / 2) ^ (1/4)), for a constant c with c ^ 4 = -1/2, parametrises the whole preimage by the punctured unit disc, so the preimage is path connected: the exponent 1 of t in the radicand is coprime to 4. The substitution t ↦ 1 - t fixes the radicand and gives the same over 1. Since the components of these preimages are the cycles of σ0 and σ1, both are 4-cycles.
• At most two sheets over ∞. Over |t| > 2 the radicand is t ^ 2 (1 - 1/t), of order -2 at ∞, and gcd(4, 2) = 2: the preimage is covered by the two connected images of v ↦ (2 / v ^ 2, ζ c v⁻¹ (1 - v ^ 2 / 2) ^ (1/4)) for ζ = 1, i and c ^ 4 = 4.
• Connectedness and regularity. A single cycle of σ0 makes the monodromy transitive, so the cover is path connected. Its deck group is then the group of fourth roots of unity, of order the degree, and the monodromy triple is regular.
• The torus triple. In a regular triple a nontrivial element of the monodromy group has no fixed point. Among the cycle data of connected triples of degree four with σ0 and σ1 both 4-cycles, the only one with σinf fixed-point-free is [4], [4], [2, 2], and these cycle data determine the torus triple among connected triples of degree four.

Main declarations

• TauCeti.ThricePuncturedSphere.superellipticCurve: the points (t, y) with t ∈ U and y ^ 4 = t (t - 1), with the projection superellipticProj.
• TauCeti.ThricePuncturedSphere.isCoveringMap_superellipticProj: the projection is a covering map.
• TauCeti.ThricePuncturedSphere.isQuotientCoveringMap_superellipticProj: it is the quotient covering by the fourth roots of unity, acting by y ↦ ζ y.
• TauCeti.ThricePuncturedSphere.natCard_superellipticProj_preimage_singleton: its fibres have four points.
• isPathConnected_superellipticProj_preimage_puncturedNeighborhoodZero and isPathConnected_superellipticProj_preimage_puncturedNeighborhoodOne: one sheet over each of the punctured discs about 0 and 1.
• TauCeti.ThricePuncturedSphere.superellipticCurve.instPathConnectedSpace: the cover is path connected.
• TauCeti.ThricePuncturedSphere.superellipticDeckMulEquiv: its deck group is the group of fourth roots of unity, cyclic of order 4.
• TauCeti.ThricePuncturedSphere.isRegular_monodromyTriple_superellipticProj: its monodromy triple is regular.
• TauCeti.ThricePuncturedSphere.cycleData_monodromyTriple_superellipticProj: its cycle data are [4], [4], [2, 2].
• TauCeti.ThricePuncturedSphere.isoClass_monodromyTriple_superellipticProj_eq_torusTriple: its monodromy triple is isomorphic to the torus triple.

References

• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §8 (the Riemann surface of an algebraic function, whose unbranched part is the root space of a separable family).
• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press, 2012, §1.2.7 (one point of the compactification for each component over a puncture) and §2.7 (monodromy, deck groups and regular covers).

The cover and its projection

def TauCeti.ThricePuncturedSphere.superellipticCurve : Set (ThricePuncturedSphere × ℂ)

The points of the superelliptic curve y ^ 4 = t (t - 1) lying over the thrice-punctured sphere: the pairs (t, y) with t ∈ ℂ ∖ {0, 1} and y ^ 4 = t (t - 1).

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_superellipticCurve {q : ThricePuncturedSphere × ℂ} : q ∈ superellipticCurve ↔ q.2 ^ 4 = ↑q.1 * (↑q.1 - 1)

def TauCeti.ThricePuncturedSphere.superellipticProj (q : ↑superellipticCurve) : ThricePuncturedSphere

The projection (t, y) ↦ t of the superelliptic curve to the thrice-punctured sphere.

@[simp]

theorem TauCeti.ThricePuncturedSphere.superellipticProj_apply (q : ↑superellipticCurve) : superellipticProj q = (↑q).1

theorem TauCeti.ThricePuncturedSphere.snd_ne_zero_of_mem_superellipticCurve {q : ThricePuncturedSphere × ℂ} (hq : q ∈ superellipticCurve) : q.2 ≠ 0

The y-coordinate of a point of the superelliptic curve over the thrice-punctured sphere is nonzero.

theorem TauCeti.ThricePuncturedSphere.isCoveringMap_superellipticProj : IsCoveringMap superellipticProj

The superelliptic curve is a covering space of the thrice-punctured sphere. It is the root space of the family of quartics Y ^ 4 - t (t - 1), which are separable because the radicand does not vanish over ℂ ∖ {0, 1}.

The action of the fourth roots of unity

@[instance_reducible]

instance TauCeti.ThricePuncturedSphere.superellipticCurve.instMulAction : MulAction ↥(rootsOfUnity 4 ℂ) ↑superellipticCurve

The fourth roots of unity act on the superelliptic curve by y ↦ ζ y, over the thrice-punctured sphere.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_rootsOfUnity_smul_superellipticCurve (ζ : ↥(rootsOfUnity 4 ℂ)) (q : ↑superellipticCurve) : ↑(ζ • q) = ((↑q).1, ζ • (↑q).2)

instance TauCeti.ThricePuncturedSphere.superellipticCurve.instContinuousConstSMul : ContinuousConstSMul ↥(rootsOfUnity 4 ℂ) ↑superellipticCurve

Multiplication of the y-coordinate by a fourth root of unity is continuous.

instance TauCeti.ThricePuncturedSphere.superellipticCurve.instIsCancelSMul : IsCancelSMul ↥(rootsOfUnity 4 ℂ) ↑superellipticCurve

The fourth roots of unity act freely on the superelliptic curve, whose y-coordinates are nonzero over the thrice-punctured sphere.

theorem TauCeti.ThricePuncturedSphere.isQuotientCoveringMap_superellipticProj : IsQuotientCoveringMap superellipticProj ↥(rootsOfUnity 4 ℂ)

The superelliptic curve is the quotient covering by the fourth roots of unity. Two points lie over the same t exactly when their y-coordinates have the same fourth power, that is, when they differ by a fourth root of unity.

theorem TauCeti.ThricePuncturedSphere.natCard_superellipticProj_preimage_singleton (t : ThricePuncturedSphere) : Nat.card ↑(superellipticProj ⁻¹' {t}) = 4

The superelliptic curve is a four-sheeted cover: each fibre is a torsor under the fourth roots of unity.

The sheets over the punctured discs about 0 and 1

theorem TauCeti.ThricePuncturedSphere.isPathConnected_superellipticProj_preimage_puncturedNeighborhoodZero : IsPathConnected (superellipticProj ⁻¹' puncturedNeighborhoodZero)

The superelliptic curve has one sheet over the punctured disc about 0: the preimage of 0 < |t| < 1/2 is path connected, being parametrised by w ↦ (w ^ 4 / 2, c w (1 - w ^ 4 / 2) ^ (1/4)) on the punctured unit disc.

theorem TauCeti.ThricePuncturedSphere.isPathConnected_superellipticProj_preimage_puncturedNeighborhoodOne : IsPathConnected (superellipticProj ⁻¹' puncturedNeighborhoodOne)

The superelliptic curve has one sheet over the punctured disc about 1: the preimage of 0 < |t - 1| < 1/2 is path connected.

At most two sheets over the punctured neighbourhood of ∞

Connectedness, the deck group and regularity

theorem TauCeti.ThricePuncturedSphere.isConnected_monodromyTriple_superellipticProj {n : ℕ} (ν : ↑(superellipticProj ⁻¹' {basePt}) ≃ Fin n) : (isCoveringMap_superellipticProj.monodromyTriple ν).IsConnected

The monodromy triple of the superelliptic curve is connected: its monodromy group already contains the single cycle σ0.

instance TauCeti.ThricePuncturedSphere.superellipticCurve.instPathConnectedSpace : PathConnectedSpace ↑superellipticCurve

The superelliptic curve over the thrice-punctured sphere is path connected.

noncomputable def TauCeti.ThricePuncturedSphere.superellipticDeckMulEquiv : ↥(rootsOfUnity 4 ℂ) ≃* ↥(deck superellipticProj)

The deck group of the superelliptic curve is the group of fourth roots of unity, acting by y ↦ ζ y (superellipticDeckMulEquiv_apply).

@[simp]

theorem TauCeti.ThricePuncturedSphere.superellipticDeckMulEquiv_apply (ζ : ↥(rootsOfUnity 4 ℂ)) (q : ↑superellipticCurve) : ↑(superellipticDeckMulEquiv ζ) q = ζ • q

instance TauCeti.ThricePuncturedSphere.isCyclic_deck_superellipticProj : IsCyclic ↥(deck superellipticProj)

The deck group of the superelliptic curve is cyclic.

theorem TauCeti.ThricePuncturedSphere.natCard_deck_superellipticProj : Nat.card ↥(deck superellipticProj) = 4

The deck group of the superelliptic curve has order 4.

theorem TauCeti.ThricePuncturedSphere.isRegular_monodromyTriple_superellipticProj {n : ℕ} (ν : ↑(superellipticProj ⁻¹' {basePt}) ≃ Fin n) : (isCoveringMap_superellipticProj.monodromyTriple ν).IsRegular

The superelliptic curve is a regular cover: its monodromy triple is regular, its automorphism group being the deck group, of order the degree 4.

The monodromy triple is the torus triple

theorem TauCeti.ThricePuncturedSphere.cycleData_monodromyTriple_superellipticProj {n : ℕ} (ν : ↑(superellipticProj ⁻¹' {basePt}) ≃ Fin n) : (isCoveringMap_superellipticProj.monodromyTriple ν).cycleData = ({4}, {4}, {2, 2})

The cycle data of the superelliptic curve are [4], [4], [2, 2]. Over 0 and 1 there is one sheet, so σ0 and σ1 are 4-cycles. Over ∞ there are at most two sheets, so σinf is not the identity, and in a regular triple a nontrivial monodromy element has no fixed point. Among connected triples of degree four with σ0 and σ1 both 4-cycles, σinf has cycle type [1, 1, 1, 1], [2, 2] or [3, 1], and only [2, 2] has no fixed point.

theorem TauCeti.ThricePuncturedSphere.isoClass_monodromyTriple_superellipticProj_eq_torusTriple (ν : ↑(superellipticProj ⁻¹' {basePt}) ≃ Fin 4) : PermutationTriple.IsoClass.mk (isCoveringMap_superellipticProj.monodromyTriple ν) = PermutationTriple.IsoClass.mk PermutationTriple.torusTriple

The monodromy triple of the superelliptic curve is the Euclidean torus triple, up to relabelling: both are connected of degree four with cycle data [4], [4], [2, 2], which classify connected triples in degree four.