The compact superelliptic curve y ^ 4 = t (t - 1) as an analytic Belyi pair

Over the thrice-punctured sphere ℂ ∖ {0, 1} the points of the affine curve y ^ 4 = t (t - 1) form a connected four-sheeted cover TauCeti.ThricePuncturedSphere.superellipticProj of the t-line. Filling its punctures gives the compact Riemann surface of the algebraic function y = (t ^ 2 - t) ^ (1/4), and the extension of t to it is a Belyi map. This file builds this analytic Belyi pair TauCeti.AnalyticBelyiPair.superelliptic and computes its invariants from the cover, that is from the equation:

• Degree. The Belyi map β = t has degree 4, the number of fourth roots of t (t - 1).
• Ramification. Over 0 and over 1 there is a single point, of local multiplicity 4, and over ∞ there are two points, each of local multiplicity 2. Indeed the components of the cover over the punctured discs about 0, 1 and ∞ are the cycles of the monodromy permutations σ0, σ1 and σinf of the cover, whose cycle data are [4], [4], [2, 2], and these cycle lengths are the local multiplicities of β. All three of 0, 1 and ∞ are branch values.
• Genus. The monodromy triple of the pair has one cycle over each of 0 and 1 and two over ∞, so its Euler characteristic is 1 + 1 + 2 - 4 = 0 and its genus is 1: this is the Riemann–Hurwitz count 2 g - 2 = 4 · (-2) + (3 + 3 + 1 + 1) = 0.
• Automorphisms. The automorphisms y ↦ ζ y of the cover, for ζ a fourth root of unity, extend to the compact curve, and they are all the automorphisms of the pair: the automorphism group is cyclic of order 4, equal to the degree, so the pair is regular.

Since an analytic Belyi pair is determined up to isomorphism by the isomorphism class of its monodromy triple, the superelliptic curve is, up to isomorphism, the unique analytic Belyi pair whose monodromy triple is the Euclidean torus triple TauCeti.PermutationTriple.torusTriple (TauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff).

Main declarations

• TauCeti.ThricePuncturedSphere.superellipticConnectedCover: the superelliptic curve over ℂ ∖ {0, 1} as a connected cover of degree 4.
• TauCeti.AnalyticBelyiPair.superelliptic: its filled analytic Belyi pair, with Belyi map t (TauCeti.AnalyticBelyiPair.β_superelliptic_incl).
• TauCeti.AnalyticBelyiPair.degree_β_superelliptic: the Belyi map has degree 4.
• TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_zero_superelliptic, map_localMultiplicity_fiber_one_superelliptic, map_localMultiplicity_fiber_inf_superelliptic: the ramification partitions [4], [4] and [2, 2].
• TauCeti.AnalyticBelyiPair.branchValues_β_superelliptic: the branch values are 0, 1, ∞.
• TauCeti.AnalyticBelyiPair.genus_monodromyTriple_superelliptic: genus one.
• TauCeti.AnalyticBelyiPair.superellipticIsoMulEquiv: the automorphism group of the pair is the group of fourth roots of unity, acting by y ↦ ζ y.
• TauCeti.AnalyticBelyiPair.isRegular_monodromyTriple_superelliptic: the pair is regular.
• TauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff: the superelliptic curve is the analytic Belyi pair of 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, Theorem 8.9) and §17 (the Riemann–Hurwitz formula, Theorem 17.14).
• 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 (filling the punctures of a finite cover) and §2.7 (deck groups and regular covers).

noncomputable def TauCeti.ThricePuncturedSphere.superellipticConnectedCover : ConnectedCover basePt 4

The superelliptic curve y ^ 4 = t (t - 1) over ℂ ∖ {0, 1}, as a connected cover of degree 4. Its total space is TauCeti.ThricePuncturedSphere.superellipticCurve and its projection is (t, y) ↦ t (TauCeti.ThricePuncturedSphere.superellipticConnectedCover_proj).

@[simp]

theorem TauCeti.ThricePuncturedSphere.superellipticConnectedCover_proj : ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj superellipticConnectedCover.cover)) = superellipticProj

The projection of the superelliptic cover is (t, y) ↦ t.

noncomputable def TauCeti.AnalyticBelyiPair.superelliptic : AnalyticBelyiPair

The compact superelliptic curve y ^ 4 = t (t - 1), with Belyi map β = t. It is the filled analytic Belyi pair of the superelliptic cover of ℂ ∖ {0, 1}: the compact Riemann surface of the algebraic function (t ^ 2 - t) ^ (1/4), with the extension of t (TauCeti.AnalyticBelyiPair.β_superelliptic_incl).

@[simp]

theorem TauCeti.AnalyticBelyiPair.β_superelliptic_incl (q : ↑ThricePuncturedSphere.superellipticCurve) : ↑superelliptic.β (PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ThricePuncturedSphere.superellipticConnectedCover.cover))) q) = ↑↑(↑q).1

The Belyi map of the superelliptic curve is t on the points (t, y) of the affine curve over ℂ ∖ {0, 1}, which are points of the compact curve by the inclusion of the superelliptic cover into its filled cover.

@[simp]

theorem TauCeti.AnalyticBelyiPair.degree_β_superelliptic : RiemannSurface.degree ↑superelliptic.β = 4

The Belyi map of the superelliptic curve has degree 4.

theorem TauCeti.AnalyticBelyiPair.cycleData_monodromyTriple_superelliptic {n : ℕ} (ν : ↑(superelliptic.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (⋯.monodromyTriple ν).cycleData = ({4}, {4}, {2, 2})

The cycle data of the monodromy triple of the superelliptic curve are [4], [4], [2, 2], for any numbering of its fibre over 1/2: these are the cycle data of the cover, computed from the equation in TauCeti.ThricePuncturedSphere.cycleData_monodromyTriple_superellipticProj.

theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_zero_superelliptic : Multiset.map (RiemannSurface.localMultiplicity ↑superelliptic.β) ⋯.toFinset.val = {4}

The ramification of the superelliptic curve over 0 is [4]: a single point, of local multiplicity 4.

theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_one_superelliptic : Multiset.map (RiemannSurface.localMultiplicity ↑superelliptic.β) ⋯.toFinset.val = {4}

The ramification of the superelliptic curve over 1 is [4]: a single point, of local multiplicity 4.

theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_inf_superelliptic : Multiset.map (RiemannSurface.localMultiplicity ↑superelliptic.β) ⋯.toFinset.val = {2, 2}

The ramification of the superelliptic curve over ∞ is [2, 2]: two points, each of local multiplicity 2.

@[simp]

theorem TauCeti.AnalyticBelyiPair.branchValues_β_superelliptic : superelliptic.β.branchValues = {↑0, ↑1, OnePoint.infty}

The branch values of the superelliptic curve are 0, 1 and ∞.

theorem TauCeti.AnalyticBelyiPair.genus_monodromyTriple_superelliptic {n : ℕ} (ν : ↑(superelliptic.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (⋯.monodromyTriple ν).genus = 1

The superelliptic curve has genus one: the genus of its monodromy triple is 1, for any numbering of its fibre over 1/2. The cycles of the triple are the points over 0, 1 and ∞, with lengths the local multiplicities [4], [4], [2, 2], so its Euler characteristic is 1 + 1 + 2 - 4 = 0. This is the Riemann–Hurwitz count 2 g - 2 = 4 · (-2) + (3 + 3 + 1 + 1).

noncomputable def TauCeti.AnalyticBelyiPair.superellipticIsoMulEquiv : ↥(rootsOfUnity 4 ℂ) ≃* superelliptic.Iso superelliptic

The automorphisms of the superelliptic curve are y ↦ ζ y for the fourth roots of unity ζ: these automorphisms of the cover over ℂ ∖ {0, 1} extend to the compact curve (TauCeti.AnalyticBelyiPair.superellipticIsoMulEquiv_apply_incl), and they are all its automorphisms over the Riemann sphere.

@[simp]

theorem TauCeti.AnalyticBelyiPair.superellipticIsoMulEquiv_apply_incl (ζ : ↥(rootsOfUnity 4 ℂ)) (q : ↑ThricePuncturedSphere.superellipticCurve) : (superellipticIsoMulEquiv ζ) (PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ThricePuncturedSphere.superellipticConnectedCover.cover))) q) = PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ThricePuncturedSphere.superellipticConnectedCover.cover))) (ζ • q)

The automorphism TauCeti.AnalyticBelyiPair.superellipticIsoMulEquiv ζ of the superelliptic curve is (t, y) ↦ (t, ζ y) on the affine curve over ℂ ∖ {0, 1}.

instance TauCeti.AnalyticBelyiPair.isCyclic_iso_superelliptic : IsCyclic (superelliptic.Iso superelliptic)

The automorphism group of the superelliptic curve is cyclic.

theorem TauCeti.AnalyticBelyiPair.natCard_iso_superelliptic : Nat.card (superelliptic.Iso superelliptic) = 4

The superelliptic curve has four automorphisms, as many as its degree.

theorem TauCeti.AnalyticBelyiPair.isRegular_monodromyTriple_superelliptic {n : ℕ} (ν : ↑(superelliptic.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (⋯.monodromyTriple ν).IsRegular

The superelliptic curve is a regular Belyi pair: its monodromy triple is regular, for any numbering of its fibre over 1/2.

theorem TauCeti.AnalyticBelyiPair.isoClass_monodromyTriple_superelliptic_eq_torusTriple (ν : ↑(superelliptic.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin 4) : PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν) = PermutationTriple.IsoClass.mk PermutationTriple.torusTriple

The monodromy triple of the superelliptic curve is the torus triple, up to relabelling, for any numbering of its fibre over 1/2.

theorem TauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff {P : AnalyticBelyiPair} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin 4) : Nonempty (P.Iso superelliptic) ↔ PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν) = PermutationTriple.IsoClass.mk PermutationTriple.torusTriple

The superelliptic curve is the analytic Belyi pair of the torus triple: an analytic Belyi pair is isomorphic to the superelliptic curve exactly when its monodromy triple is isomorphic to TauCeti.PermutationTriple.torusTriple, for any numbering of its fibre over 1/2.