Local degrees of the filled cover over the three punctures

Let p : E → ℂ ∖ {0, 1} be a covering map whose fibre over 1/2 is numbered by ν : p ⁻¹' {1/2} ≃ Fin n, with monodromy triple (σ0, σ1, σinf). The points that TauCeti.FilledCover p adds over a puncture q ∈ {0, 1, ∞} are the connected components of p ⁻¹' D_q*, and each has a local degree TauCeti.FilledCover.degree, the exponent e for which p is w ↦ w ^ e near it. This file proves that over each puncture the multiset of these local degrees is the full cycle type of the corresponding permutation, a partition of n, so the local degrees over each puncture sum to n. Once p is extended to a branched cover of the Riemann sphere, these local degrees are its ramification indices over 0, 1 and ∞, and the three multisets are its ramification partitions.

Summing over all added points gives the combinatorial form of the Riemann–Hurwitz formula: the total ramification ∑ (e - 1) is 2 n - χ, where χ is the Euler characteristic of the monodromy triple, so for a connected cover of genus g it is 2 n + 2 g - 2.

Main results

• TauCeti.FilledCover.map_degree_overZero, TauCeti.FilledCover.map_degree_overOne, TauCeti.FilledCover.map_degree_overInf: the local degrees over 0, 1 and ∞ are the full cycle types of σ0, σ1 and σinf.
• TauCeti.FilledCover.sum_degree_overZero, TauCeti.FilledCover.sum_degree_overOne, TauCeti.FilledCover.sum_degree_overInf: over each puncture the local degrees sum to n.
• TauCeti.FilledCover.sum_degree: the local degrees of all added points sum to 3 n.
• TauCeti.FilledCover.sum_degree_sub_one: the total ramification is 2 n - χ.
• TauCeti.FilledCover.two_mul_genus_sub_two: the Riemann–Hurwitz formula 2 g - 2 = -2 n + ∑ (e - 1) for a connected cover.

References

• 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 and §4.2 (the cycle lengths of the monodromy are the ramification indices).
• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §17, Theorem 17.14 (the Riemann–Hurwitz formula).

theorem TauCeti.FilledCover.map_degree_overZero {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero))] : Multiset.map (fun (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero)) => degree p (FilledPoint.overZero p c)) Finset.univ.val = (hp.monodromyTriple ν).σ0.fullCycleType

The ramification partition over 0. The local degrees of the points added over 0 are the cycle lengths of σ0, fixed points included.

theorem TauCeti.FilledCover.map_degree_overOne {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne))] : Multiset.map (fun (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne)) => degree p (FilledPoint.overOne p c)) Finset.univ.val = (hp.monodromyTriple ν).σ1.fullCycleType

The ramification partition over 1. The local degrees of the points added over 1 are the cycle lengths of σ1, fixed points included.

theorem TauCeti.FilledCover.map_degree_overInf {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf))] : Multiset.map (fun (c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf)) => degree p (FilledPoint.overInf p c)) Finset.univ.val = (hp.monodromyTriple ν).σinf.fullCycleType

The ramification partition over ∞. The local degrees of the points added over ∞ are the cycle lengths of σinf, fixed points included.

theorem TauCeti.FilledCover.sum_degree_overZero {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero))] : ∑ c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodZero), degree p (FilledPoint.overZero p c) = n

The local degrees of the points added over 0 sum to the degree of the cover.

theorem TauCeti.FilledCover.sum_degree_overOne {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne))] : ∑ c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodOne), degree p (FilledPoint.overOne p c) = n

The local degrees of the points added over 1 sum to the degree of the cover.

theorem TauCeti.FilledCover.sum_degree_overInf {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf))] : ∑ c : ConnectedComponents ↑(p ⁻¹' ThricePuncturedSphere.puncturedNeighborhoodInf), degree p (FilledPoint.overInf p c) = n

The local degrees of the points added over ∞ sum to the degree of the cover.

theorem TauCeti.FilledCover.sum_degree {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (FilledPoint p)] : ∑ i : FilledPoint p, degree p i = 3 * n

The local degrees of all the added points sum to three times the degree of the cover, n over each of the three punctures.

theorem TauCeti.FilledCover.sum_degree_sub_one {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [Fintype (FilledPoint p)] : ∑ i : FilledPoint p, (↑(degree p i) - 1) = 2 * ↑n - (hp.monodromyTriple ν).eulerChar

The total ramification. Summed over all the added points, e - 1 adds up to 2 n - χ, where e is the local degree and χ is the Euler characteristic of the monodromy triple.

theorem TauCeti.FilledCover.two_mul_genus_sub_two {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ} (ν : ↑(p ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) [PathConnectedSpace E] [Fintype (FilledPoint p)] : 2 * ↑(hp.monodromyTriple ν).genus - 2 = -2 * ↑n + ∑ i : FilledPoint p, (↑(degree p i) - 1)

The Riemann–Hurwitz formula for a filled cover. For a connected cover of degree n, whose monodromy triple has genus g, the total ramification ∑ (e - 1) over the added points satisfies 2 g - 2 = -2 n + ∑ (e - 1). This is the shape of the Riemann–Hurwitz formula for a degree-n branched cover of the Riemann sphere, which has genus 0.