Analytic Belyi pairs

An analytic Belyi pair (X, β) is a compact connected Riemann surface X together with a nonconstant holomorphic map β : X → ℙ¹(ℂ) to the Riemann sphere OnePoint ℂ whose branch values lie in {0, 1, ∞}; β is then a Belyi map. Equivalently, β is a covering map over the complement of {0, 1, ∞} (TauCeti.AnalyticBelyiPair.isCoveringMapOn, and the constructor TauCeti.AnalyticBelyiPair.ofIsCoveringMapOn), since a finite holomorphic map of a compact surface is a covering exactly away from its branch values.

Restricting β over the thrice-punctured sphere ℂ ∖ {0, 1} gives a finite covering map TauCeti.AnalyticBelyiPair.restrict, of degree the degree of β. Its total space, the surface X with the finitely many points over 0, 1 and ∞ removed, is path connected. Its monodromy triple, for any numbering of the fibre over the basepoint 1/2, is therefore a connected permutation triple of that degree, and its isomorphism class TauCeti.AnalyticBelyiPair.connectedIsoClass does not depend on the numbering. This is the combinatorial datum attached to the pair, the one through which analytic Belyi pairs are compared with permutation triples and dessins d'enfants.

An isomorphism of analytic Belyi pairs is a biholomorphism of their surfaces over the sphere (TauCeti.AnalyticBelyiPair.Iso). It restricts to an isomorphism of the attached covers of ℂ ∖ {0, 1}, so isomorphic pairs have the same degree and isomorphic monodromy triples, and the permutation triple is a well-defined function of the isomorphism class of a pair of degree n (TauCeti.AnalyticBelyiPair.toIsoClass). This is the map from analytic Belyi pairs to permutation triples through which the analytic Riemann existence theorem for three-point covers compares the two classifications.

An isomorphism of pairs is determined by the image of a single point over ℂ ∖ {0, 1} (TauCeti.AnalyticBelyiPair.Iso.eq_of_apply_eq): its restriction is a lift through the connected cover attached to the target, and the points over ℂ ∖ {0, 1} are dense in the surface. Hence there are at most as many isomorphisms P ≅ Q as the degree of Q, and the automorphisms of a pair form a finite group whose order divides its degree.

This group is the deck group of the pair in each of its guises. Since every homeomorphism over the sphere is holomorphic (see below), the automorphisms of a pair are the deck transformations of its Belyi map (TauCeti.AnalyticBelyiPair.isoMulEquivDeck). These restrict to the deck transformations of the attached cover of ℂ ∖ {0, 1} (TauCeti.AnalyticBelyiPair.isoMulEquivDeckRestrict), and those are the automorphisms of its monodromy triple. So the automorphism group of a pair is the automorphism group of its monodromy triple, for any numbering of the fibre over 1/2 (TauCeti.AnalyticBelyiPair.isoMulEquivAutomorphismGroup), and a pair has as many automorphisms as its degree exactly when its triple is regular.

Forgetting the complex structure turns a pair of degree n into a topological branched cover of degree n (TauCeti.AnalyticBelyiPair.toTopBranchedCover). The topological local degree is the analytic local multiplicity, and isomorphisms of pairs give isomorphisms of their underlying topological branched covers. Consequently this construction descends to isomorphism classes.

Conversely, the complex structure of a pair is determined by its Belyi map: every continuous map over the sphere between analytic Belyi pairs is holomorphic (TauCeti.AnalyticBelyiPair.mdifferentiable_of_β). Away from the points over 0, 1 and ∞ it lifts the Belyi map of the source through the Belyi map of the target, which is a local biholomorphism there; the finitely many remaining points are removable singularities. Hence a homeomorphism over the sphere is an isomorphism of pairs (TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph), and the passage to topological branched covers is injective on isomorphism classes (TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_injective).

A morphism of analytic Belyi pairs P → Q is a holomorphic map of surfaces over the sphere (TauCeti.AnalyticBelyiPair.Hom); as for isomorphisms, every continuous map over the sphere is one. A morphism is a finite holomorphic map, hence surjective, and the degrees multiply along it, so the degree of Q divides that of P. A morphism between pairs of the same degree has degree one, so it is an isomorphism (TauCeti.AnalyticBelyiPair.Hom.toIso). A morphism restricts to a map of the attached covers of ℂ ∖ {0, 1}, and so it intertwines the monodromy triples on the fibres over 1/2.

The basic examples live on the sphere itself: for n ≠ 0, the power map z ↦ z ^ n is a Belyi map of degree n, ramified of index n over 0 and ∞ and unramified over 1 (TauCeti.AnalyticBelyiPair.pow). For n = 1 this is the trivial pair, the identity of the sphere. It is terminal: the Belyi map of a pair is its unique morphism to the trivial pair (TauCeti.AnalyticBelyiPair.homPowOne). A pair of degree one is trivial, its Belyi map being a biholomorphism onto the sphere, so all pairs of degree one are isomorphic (TauCeti.AnalyticBelyiPair.isoOfDegreeEqOne). The polynomial z ↦ 4z(1 - z) is a Belyi map of degree 2, unramified over 0 and ramified of index 2 over 1 and ∞, so that its ramification partitions over 0, 1 and ∞ are [1, 1], [2] and [2] (TauCeti.AnalyticBelyiPair.chebyshev).

Main declarations

• TauCeti.AnalyticBelyiPair: the carrier, a compact connected Riemann surface with a finite holomorphic map to the sphere whose branch values lie in {0, 1, ∞}.
• TauCeti.AnalyticBelyiPair.ofIsCoveringMapOn: a nonconstant holomorphic map to the sphere that is a covering map over the complement of {0, 1, ∞} is a Belyi map.
• TauCeti.AnalyticBelyiPair.ncard_preimage_singleton: the fibres of β away from {0, 1, ∞} have as many points as the degree.
• TauCeti.AnalyticBelyiPair.restrict, TauCeti.AnalyticBelyiPair.isCoveringMap_restrict: the restriction of β over ℂ ∖ {0, 1} is a covering map, with TauCeti.AnalyticBelyiPair.ncard_restrict_preimage_singleton points in each fibre.
• TauCeti.AnalyticBelyiPair.instPathConnectedSpacePreimageRange: the total space of this cover is path connected.
• TauCeti.AnalyticBelyiPair.isoClass, TauCeti.AnalyticBelyiPair.isoClass_eq: the isomorphism class of the monodromy triple, computed by any numbering of the fibre over 1/2.
• TauCeti.AnalyticBelyiPair.connectedIsoClass, TauCeti.AnalyticBelyiPair.connectedIsoClass_eq: the same class among connected triples (TauCeti.AnalyticBelyiPair.isConnected_isoClass).
• TauCeti.AnalyticBelyiPair.Iso: isomorphisms of analytic Belyi pairs, with TauCeti.AnalyticBelyiPair.Iso.restrict the isomorphism of the attached covers of ℂ ∖ {0, 1}.
• TauCeti.AnalyticBelyiPair.Iso.degree_eq and TauCeti.AnalyticBelyiPair.Iso.isoClass_monodromyTriple_eq: isomorphic pairs have the same degree and isomorphic monodromy triples.
• TauCeti.AnalyticBelyiPair.isoSetoid, TauCeti.AnalyticBelyiPair.toIsoClass: isomorphism of pairs of degree n, and the permutation triple of an isomorphism class of such pairs.
• TauCeti.AnalyticBelyiPair.Iso.eq_of_apply_eq: an isomorphism of pairs is determined by the image of one point over ℂ ∖ {0, 1}.
• TauCeti.AnalyticBelyiPair.Iso.natCard_le_degree: there are finitely many isomorphisms of pairs P ≅ Q, at most the degree of Q.
• TauCeti.AnalyticBelyiPair.Iso.natCard_dvd_degree: the order of the automorphism group P.Iso P divides the degree of P.
• TauCeti.AnalyticBelyiPair.isoMulEquivDeck: the automorphisms of a pair are the deck transformations of its Belyi map.
• TauCeti.AnalyticBelyiPair.isoMulEquivDeckRestrict: the automorphisms of a pair are the deck transformations of its cover of ℂ ∖ {0, 1}.
• TauCeti.AnalyticBelyiPair.isoMulEquivAutomorphismGroup: the automorphism group of a pair is the automorphism group of its monodromy triple.
• TauCeti.AnalyticBelyiPair.isRegular_monodromyTriple_iff_natCard_iso: the monodromy triple is regular exactly when the pair has as many automorphisms as its degree.
• TauCeti.AnalyticBelyiPair.toTopBranchedCover: the underlying topological branched cover, whose ramification partitions are formed by the local multiplicities of the Belyi map (TauCeti.AnalyticBelyiPair.parts_ramificationPartition_toTopBranchedCover) and whose unbranched part has the monodromy of the pair (TauCeti.AnalyticBelyiPair.isoClass_monodromyTriple_toTopBranchedCover).
• TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass: the induced map on isomorphism classes.
• TauCeti.AnalyticBelyiPair.mdifferentiable_of_β: a continuous map over the sphere between analytic Belyi pairs is holomorphic.
• TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph: a homeomorphism over the sphere is an isomorphism of analytic Belyi pairs.
• TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_injective: analytic Belyi pairs with isomorphic underlying topological branched covers are isomorphic.
• TauCeti.AnalyticBelyiPair.pow: the power map z ↦ z ^ n of the sphere, of degree n (TauCeti.AnalyticBelyiPair.degree_β_pow), unramified over 1 (TauCeti.AnalyticBelyiPair.one_notMem_branchValues_β_pow).
• TauCeti.AnalyticBelyiPair.Hom: morphisms of analytic Belyi pairs, with TauCeti.AnalyticBelyiPair.Hom.ofContinuous, TauCeti.AnalyticBelyiPair.Hom.surjective, TauCeti.AnalyticBelyiPair.Hom.degree_β_eq_mul_degree (degrees multiply), TauCeti.AnalyticBelyiPair.Hom.toIso (a morphism between pairs of the same degree is an isomorphism) and TauCeti.AnalyticBelyiPair.Hom.semiconj_component_monodromyTriple (a morphism intertwines the monodromy triples).
• TauCeti.AnalyticBelyiPair.homPowOne: the Belyi map, as the unique morphism to the trivial pair.
• TauCeti.AnalyticBelyiPair.isoOfDegreeEqOne, TauCeti.AnalyticBelyiPair.degree_β_eq_one_iff_nonempty_iso: pairs of degree one are isomorphic to each other and to the trivial pair.
• TauCeti.AnalyticBelyiPair.chebyshev: the map z ↦ 4z(1 - z) of the sphere, of degree 2 (TauCeti.AnalyticBelyiPair.degree_β_chebyshev), with branch values 1 and ∞ (TauCeti.AnalyticBelyiPair.branchValues_β_chebyshev); its fibres and local multiplicities over 0, 1 and ∞ are TauCeti.RiemannSurface.preimage_onePointMap_four_mul_mul_one_sub_zero and its companions in TauCeti.Analysis.Complex.RiemannSurface.ChebyshevMap.

References

• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §8, Theorem 8.5 (uniqueness of the extension of an unbranched covering across a finite set).
• 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, §2.7 (the monodromy and the covering group of a morphism), Chapter 3 (Belyi functions and Belyi pairs) and §4.3 (the monodromy of a Belyi pair).
• L. Schneps, Dessins d'enfants on the Riemann sphere, in The Grothendieck Theory of Dessins d'Enfants, London Mathematical Society Lecture Note Series 200, Cambridge University Press, 1994.

structure TauCeti.AnalyticBelyiPair : Type (u + 1)

An analytic Belyi pair: a compact connected Riemann surface X, carried by the unbundled instances on its type, together with a finite holomorphic map β : X → OnePoint ℂ to the Riemann sphere, the Belyi map, all of whose branch values lie in {0, 1, ∞}.

On a compact connected surface every nonconstant holomorphic map is finite, so β is just a nonconstant holomorphic map (TauCeti.AnalyticBelyiPair.ofIsCoveringMapOn builds a pair from these data). The condition on the branch values says that β is a covering map over the complement of {0, 1, ∞} (TauCeti.AnalyticBelyiPair.isCoveringMapOn).

• X : Type u

  The Riemann surface of the pair.

• instTopologicalSpace : TopologicalSpace self.X
• instChartedSpace : ChartedSpace ℂ self.X
• instIsManifold : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ self.X
• instT2Space : T2Space self.X
• instCompactSpace : CompactSpace self.X
• instConnectedSpace : ConnectedSpace self.X
• β : RiemannSurface.FiniteHolomorphicMap self.X (OnePoint ℂ)

  The Belyi map of the pair.

• branchValues_subset : self.β.branchValues ⊆ {↑0, ↑1, OnePoint.infty}

  The Belyi map is unramified over every point other than 0, 1 and ∞.

Belyi maps as coverings

theorem TauCeti.AnalyticBelyiPair.isCoveringMapOn (P : AnalyticBelyiPair) : IsCoveringMapOn ↑P.β {↑0, ↑1, OnePoint.infty}ᶜ

The Belyi map of an analytic Belyi pair is a covering map over the complement of {0, 1, ∞}.

noncomputable def TauCeti.AnalyticBelyiPair.ofIsCoveringMapOn (X : Type u) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {f : X → OnePoint ℂ} (hf : MDiff f) (hne : ∃ (x : X) (x' : X), f x ≠ f x') (hcov : IsCoveringMapOn f {↑0, ↑1, OnePoint.infty}ᶜ) : AnalyticBelyiPair

An analytic Belyi pair from a nonconstant holomorphic map f from a compact connected Riemann surface to the sphere which is a covering map over the complement of {0, 1, ∞}.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_β_ofIsCoveringMapOn (X : Type u) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {f : X → OnePoint ℂ} (hf : MDiff f) (hne : ∃ (x : X) (x' : X), f x ≠ f x') (hcov : IsCoveringMapOn f {↑0, ↑1, OnePoint.infty}ᶜ) : ↑(ofIsCoveringMapOn X hf hne hcov).β = f

theorem TauCeti.AnalyticBelyiPair.ncard_preimage_singleton (P : AnalyticBelyiPair) {y : OnePoint ℂ} (hy : y ∉ {↑0, ↑1, OnePoint.infty}) : (↑P.β ⁻¹' {y}).ncard = RiemannSurface.degree ↑P.β

Away from {0, 1, ∞}, every fibre of the Belyi map has as many points as its degree.

The underlying topological branched cover

theorem TauCeti.AnalyticBelyiPair.isLocalPowerAt_localMultiplicity (P : AnalyticBelyiPair) (z : P.X) : IsLocalPowerAt (↑P.β) z (RiemannSurface.localMultiplicity (↑P.β) z)

A Belyi map is locally the power map whose exponent is its analytic local multiplicity.

def TauCeti.AnalyticBelyiPair.toTopBranchedCover (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) : TopBranchedCover n

The topological branched cover underlying an analytic Belyi pair. The supplied equality records the degree in the index. Its local power models are the holomorphic local normal forms, and its topological local degree agrees with analytic local multiplicity (TauCeti.AnalyticBelyiPair.localDegree_toTopBranchedCover).

@[simp]

theorem TauCeti.AnalyticBelyiPair.toTopBranchedCover_π_apply (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) (z : P.X) : (P.toTopBranchedCover hdegree).π z = ↑P.β z

The projection of the topological branched cover underlying a pair is its Belyi map.

@[simp]

theorem TauCeti.AnalyticBelyiPair.localDegree_toTopBranchedCover (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) (z : P.X) : (P.toTopBranchedCover hdegree).localDegree z = RiemannSurface.localMultiplicity (↑P.β) z

The topological local degree underlying an analytic Belyi pair is the analytic local multiplicity of its Belyi map.

theorem TauCeti.AnalyticBelyiPair.parts_ramificationPartition_toTopBranchedCover (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) (y : OnePoint ℂ) : ((P.toTopBranchedCover hdegree).ramificationPartition y).parts = Multiset.map (RiemannSurface.localMultiplicity ↑P.β) ⋯.toFinset.val

The ramification partition over y of the topological branched cover underlying a pair is formed by the analytic local multiplicities of its Belyi map at the points over y.

Maps over the sphere are holomorphic

theorem TauCeti.AnalyticBelyiPair.mdifferentiable_of_β {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {f : P.X → Q.X} (hf : Continuous f) (hβ : ∀ (x : P.X), ↑Q.β (f x) = ↑P.β x) : MDiff f

A continuous map over the sphere between analytic Belyi pairs is holomorphic. Away from the points over 0, 1 and ∞, f lifts the Belyi map of P through that of Q, which is a local biholomorphism there; the finitely many points over 0, 1 and ∞ are removable singularities. So the complex structure of a pair is determined by its Belyi map.

The cover of the thrice-punctured sphere

noncomputable def TauCeti.AnalyticBelyiPair.restrict (P : AnalyticBelyiPair) : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) → ThricePuncturedSphere

The Belyi map restricted to the points of X over the thrice-punctured sphere ℂ ∖ {0, 1}, as a map to ℂ ∖ {0, 1}: this is the finite cover of the thrice-punctured sphere attached to the pair (TauCeti.AnalyticBelyiPair.isCoveringMap_restrict).

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_restrict_apply (P : AnalyticBelyiPair) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑↑(P.restrict x) = ↑P.β ↑x

The restricted Belyi map agrees with the Belyi map, read in the Riemann sphere.

theorem TauCeti.AnalyticBelyiPair.isCoveringMap_restrict (P : AnalyticBelyiPair) : IsCoveringMap P.restrict

The cover attached to an analytic Belyi pair. The Belyi map restricted over the thrice-punctured sphere ℂ ∖ {0, 1} is a covering map.

@[simp]

theorem TauCeti.AnalyticBelyiPair.restrict_toTopBranchedCover (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) : (P.toTopBranchedCover hdegree).restrict = P.restrict

The unbranched cover of the topological branched cover underlying a pair is the cover of ℂ ∖ {0, 1} attached to the pair.

theorem TauCeti.AnalyticBelyiPair.image_val_restrict_preimage_singleton (P : AnalyticBelyiPair) (z : ThricePuncturedSphere) : Subtype.val '' P.restrict ⁻¹' {z} = ↑P.β ⁻¹' {z.toOnePoint}

The points of X over a point z of ℂ ∖ {0, 1} are the fibre of the Belyi map over z.

theorem TauCeti.AnalyticBelyiPair.finite_restrict_preimage_singleton (P : AnalyticBelyiPair) (z : ThricePuncturedSphere) : (P.restrict ⁻¹' {z}).Finite

Every fibre of the cover of ℂ ∖ {0, 1} attached to an analytic Belyi pair is finite.

theorem TauCeti.AnalyticBelyiPair.ncard_restrict_preimage_singleton (P : AnalyticBelyiPair) (z : ThricePuncturedSphere) : (P.restrict ⁻¹' {z}).ncard = RiemannSurface.degree ↑P.β

The cover of ℂ ∖ {0, 1} attached to an analytic Belyi pair has as many sheets as the degree of the Belyi map.

theorem TauCeti.AnalyticBelyiPair.degree_β_eq_of_restrict_preimage_singleton_equiv (P : AnalyticBelyiPair) {z : ThricePuncturedSphere} {n : ℕ} (ν : ↑(P.restrict ⁻¹' {z}) ≃ Fin n) : RiemannSurface.degree ↑P.β = n

A numbering of a fibre of the cover of ℂ ∖ {0, 1} attached to an analytic Belyi pair by Fin n determines the degree of the pair: it is n.

theorem TauCeti.AnalyticBelyiPair.nonempty_restrict_preimage_singleton_equiv (P : AnalyticBelyiPair) (z : ThricePuncturedSphere) : Nonempty (↑(P.restrict ⁻¹' {z}) ≃ Fin (RiemannSurface.degree ↑P.β))

Every fibre of the cover of ℂ ∖ {0, 1} attached to an analytic Belyi pair can be numbered by Fin (degree P.β).

The monodromy triple

noncomputable def TauCeti.AnalyticBelyiPair.isoClass (P : AnalyticBelyiPair) : PermutationTriple.IsoClass (RiemannSurface.degree ↑P.β)

The permutation triple of an analytic Belyi pair, up to isomorphism: the isomorphism class of the monodromy triple of the cover of ℂ ∖ {0, 1} attached to the pair. It is computed by any numbering of the fibre over 1/2 (TauCeti.AnalyticBelyiPair.isoClass_eq).

theorem TauCeti.AnalyticBelyiPair.isoClass_eq (P : AnalyticBelyiPair) (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin (RiemannSurface.degree ↑P.β)) : P.isoClass = PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν)

The permutation triple of an analytic Belyi pair is the class of the monodromy triple for any numbering of the fibre over 1/2.

theorem TauCeti.AnalyticBelyiPair.isoClass_monodromyTriple_toTopBranchedCover (P : AnalyticBelyiPair) {n : ℕ} (hdegree : RiemannSurface.degree ↑P.β = n) (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (ν' : ↑((P.toTopBranchedCover hdegree).restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν') = PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν)

The cover of ℂ ∖ {0, 1} attached to a pair and the unbranched part of the topological branched cover underlying the pair have isomorphic monodromy triples, whatever the numberings of their fibres.

Connectedness of the cover

instance TauCeti.AnalyticBelyiPair.instPathConnectedSpacePreimageRange (P : AnalyticBelyiPair) : PathConnectedSpace ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The cover attached to an analytic Belyi pair is path connected. Its total space is the connected surface X with the finitely many points over 0, 1 and ∞ removed.

theorem TauCeti.AnalyticBelyiPair.isConnected_isoClass (P : AnalyticBelyiPair) : P.isoClass.IsConnected

The permutation triple of an analytic Belyi pair is connected.

noncomputable def TauCeti.AnalyticBelyiPair.connectedIsoClass (P : AnalyticBelyiPair) : ConnectedIsoClass (RiemannSurface.degree ↑P.β)

The connected permutation triple of an analytic Belyi pair, up to isomorphism: the class TauCeti.AnalyticBelyiPair.isoClass, as a class of connected triples. It is computed by any numbering of the fibre over 1/2 (TauCeti.AnalyticBelyiPair.connectedIsoClass_eq).

@[simp]

theorem TauCeti.AnalyticBelyiPair.forget_connectedIsoClass (P : AnalyticBelyiPair) : P.connectedIsoClass.forget = P.isoClass

Forgetting connectedness, the connected permutation triple of a pair is its permutation triple.

theorem TauCeti.AnalyticBelyiPair.connectedIsoClass_eq (P : AnalyticBelyiPair) (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin (RiemannSurface.degree ↑P.β)) : P.connectedIsoClass = ConnectedIsoClass.mk ⟨⋯.monodromyTriple ν, ⋯⟩

The connected permutation triple of an analytic Belyi pair is the class of the monodromy triple for any numbering of the fibre over 1/2.

The power maps

noncomputable def TauCeti.AnalyticBelyiPair.pow {n : ℕ} (hn : n ≠ 0) : AnalyticBelyiPair

The power maps are Belyi maps. For n ≠ 0, the Riemann sphere with the power map z ↦ z ^ n is an analytic Belyi pair; it is ramified of index n over 0 and ∞ and unramified elsewhere. For n = 1 it is the trivial pair, the identity of the sphere.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_β_pow {n : ℕ} (hn : n ≠ 0) : ↑(pow hn).β = OnePoint.map fun (z : ℂ) => z ^ n

theorem TauCeti.AnalyticBelyiPair.degree_β_pow {n : ℕ} (hn : n ≠ 0) : RiemannSurface.degree ↑(pow hn).β = n

The power map z ↦ z ^ n of the sphere is a Belyi map of degree n.

theorem TauCeti.AnalyticBelyiPair.one_notMem_branchValues_β_pow {n : ℕ} (hn : n ≠ 0) : ↑1 ∉ (pow hn).β.branchValues

The power map z ↦ z ^ n is unramified over 1.

noncomputable def TauCeti.AnalyticBelyiPair.chebyshev : AnalyticBelyiPair

The map z ↦ 4z(1 - z) is a Belyi map. The Riemann sphere with the map z ↦ 4z(1 - z), sending ∞ to ∞, is an analytic Belyi pair of degree 2. It is unramified over 0, whose preimages are 0 and 1, and ramified of index 2 over 1, at 1/2, and over ∞, at ∞, so its ramification partitions over 0, 1 and ∞ are [1, 1], [2] and [2]. The map is z ↦ (1 - T₂(1 - 2z)) / 2 for the Chebyshev polynomial T₂ = 2x² - 1.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_β_chebyshev : ↑chebyshev.β = OnePoint.map fun (z : ℂ) => 4 * z * (1 - z)

The Belyi map of chebyshev is the map z ↦ 4z(1 - z) of the sphere.

theorem TauCeti.AnalyticBelyiPair.degree_β_chebyshev : RiemannSurface.degree ↑chebyshev.β = 2

The Belyi map z ↦ 4z(1 - z) has degree 2.

@[simp]

theorem TauCeti.AnalyticBelyiPair.branchValues_β_chebyshev : chebyshev.β.branchValues = {↑1, OnePoint.infty}

The branch values of z ↦ 4z(1 - z) are exactly 1 and ∞: it is unramified over 0.

Isomorphisms of analytic Belyi pairs

structure TauCeti.AnalyticBelyiPair.Iso (P Q : AnalyticBelyiPair) : Type u

An isomorphism of analytic Belyi pairs P ≅ Q: a biholomorphism of the Riemann surfaces P.X ≃ Q.X lying over the Riemann sphere, that is, carrying the Belyi map of Q back to the Belyi map of P.

• toDiffeomorph : Diffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) P.X Q.X ↑⊤

  The underlying biholomorphism of Riemann surfaces.

• β_toDiffeomorph (x : P.X) : ↑Q.β (self.toDiffeomorph x) = ↑P.β x

  The biholomorphism lies over the Riemann sphere.

@[instance_reducible]

noncomputable instance TauCeti.AnalyticBelyiPair.Iso.instEquivLikeX {P Q : AnalyticBelyiPair} : EquivLike (P.Iso Q) P.X Q.X

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_toDiffeomorph {P Q : AnalyticBelyiPair} (e : P.Iso Q) : ⇑e.toDiffeomorph = ⇑e

theorem TauCeti.AnalyticBelyiPair.Iso.ext {P Q : AnalyticBelyiPair} {e e' : P.Iso Q} (h : ∀ (x : P.X), e x = e' x) : e = e'

theorem TauCeti.AnalyticBelyiPair.Iso.ext_iff {P Q : AnalyticBelyiPair} {e e' : P.Iso Q} : e = e' ↔ ∀ (x : P.X), e x = e' x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.β_apply {P Q : AnalyticBelyiPair} (e : P.Iso Q) (x : P.X) : ↑Q.β (e x) = ↑P.β x

An isomorphism of analytic Belyi pairs lies over the Riemann sphere.

theorem TauCeti.AnalyticBelyiPair.Iso.β_comp {P Q : AnalyticBelyiPair} (e : P.Iso Q) : ↑Q.β ∘ ⇑e = ↑P.β

An isomorphism of analytic Belyi pairs lies over the Riemann sphere.

noncomputable def TauCeti.AnalyticBelyiPair.Iso.refl (P : AnalyticBelyiPair) : P.Iso P

The identity isomorphism of an analytic Belyi pair.

noncomputable def TauCeti.AnalyticBelyiPair.Iso.symm {P Q : AnalyticBelyiPair} (e : P.Iso Q) : Q.Iso P

The inverse of an isomorphism of analytic Belyi pairs.

noncomputable def TauCeti.AnalyticBelyiPair.Iso.trans {P Q R : AnalyticBelyiPair} (e : P.Iso Q) (e' : Q.Iso R) : P.Iso R

The composite of two isomorphisms of analytic Belyi pairs.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.refl_apply {P : AnalyticBelyiPair} (x : P.X) : (Iso.refl P) x = x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.trans_apply {P Q R : AnalyticBelyiPair} (e : P.Iso Q) (e' : Q.Iso R) (x : P.X) : (e.trans e') x = e' (e x)

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.symm_apply_apply {P Q : AnalyticBelyiPair} (e : P.Iso Q) (x : P.X) : e.symm (e x) = x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.apply_symm_apply {P Q : AnalyticBelyiPair} (e : P.Iso Q) (y : Q.X) : e (e.symm y) = y

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.symm_symm {P Q : AnalyticBelyiPair} (e : P.Iso Q) : e.symm.symm = e

theorem TauCeti.AnalyticBelyiPair.Iso.trans_assoc {P Q R : AnalyticBelyiPair} (e : P.Iso Q) (e' : Q.Iso R) {S : AnalyticBelyiPair} (e'' : R.Iso S) : (e.trans e').trans e'' = e.trans (e'.trans e'')

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.trans_refl {P Q : AnalyticBelyiPair} (e : P.Iso Q) : e.trans (Iso.refl Q) = e

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.refl_trans {P Q : AnalyticBelyiPair} (e : P.Iso Q) : (Iso.refl P).trans e = e

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.self_trans_symm {P Q : AnalyticBelyiPair} (e : P.Iso Q) : e.trans e.symm = Iso.refl P

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.symm_trans_self {P Q : AnalyticBelyiPair} (e : P.Iso Q) : e.symm.trans e = Iso.refl Q

noncomputable def TauCeti.AnalyticBelyiPair.Iso.toHomeomorph {P Q : AnalyticBelyiPair} (e : P.Iso Q) : P.X ≃ₜ Q.X

The homeomorphism of Riemann surfaces underlying an isomorphism of analytic Belyi pairs.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_toHomeomorph {P Q : AnalyticBelyiPair} (e : P.Iso Q) : ⇑e.toHomeomorph = ⇑e

noncomputable def TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph {P Q : AnalyticBelyiPair} (e : P.X ≃ₜ Q.X) (he : ∀ (x : P.X), ↑Q.β (e x) = ↑P.β x) : P.Iso Q

A homeomorphism over the sphere is an isomorphism of analytic Belyi pairs: it is holomorphic by TauCeti.AnalyticBelyiPair.mdifferentiable_of_β, hence so is its inverse.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_ofHomeomorph {P Q : AnalyticBelyiPair} (e : P.X ≃ₜ Q.X) (he : ∀ (x : P.X), ↑Q.β (e x) = ↑P.β x) : ⇑(ofHomeomorph e he) = ⇑e

noncomputable def TauCeti.AnalyticBelyiPair.Iso.restrict {P Q : AnalyticBelyiPair} (e : P.Iso Q) : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint) ≃ₜ ↑(↑Q.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The isomorphism of covers of ℂ ∖ {0, 1} underlying an isomorphism of analytic Belyi pairs: its restriction to the points over the thrice-punctured sphere, which commutes with the restricted Belyi maps (TauCeti.AnalyticBelyiPair.Iso.restrict_restrict).

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_restrict_apply {P Q : AnalyticBelyiPair} (e : P.Iso Q) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(e.restrict x) = e ↑x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.restrict_restrict {P Q : AnalyticBelyiPair} (e : P.Iso Q) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : Q.restrict (e.restrict x) = P.restrict x

The restriction of an isomorphism of analytic Belyi pairs is a map of covers over ℂ ∖ {0, 1}.

theorem TauCeti.AnalyticBelyiPair.Iso.restrict_comp_restrict {P Q : AnalyticBelyiPair} (e : P.Iso Q) : Q.restrict ∘ ⇑e.restrict = P.restrict

The restriction of an isomorphism of analytic Belyi pairs is a map of covers over ℂ ∖ {0, 1}.

theorem TauCeti.AnalyticBelyiPair.Iso.degree_eq {P Q : AnalyticBelyiPair} (e : P.Iso Q) : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β

Isomorphic analytic Belyi pairs have the same degree.

noncomputable def TauCeti.AnalyticBelyiPair.Iso.toTopBranchedCover {P Q : AnalyticBelyiPair} (e : P.Iso Q) {n : ℕ} (hP : RiemannSurface.degree ↑P.β = n) (hQ : RiemannSurface.degree ↑Q.β = n) : (P.toTopBranchedCover hP).Iso (Q.toTopBranchedCover hQ)

An isomorphism of analytic Belyi pairs is an isomorphism of their underlying topological branched covers.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.toTopBranchedCover_toHomeomorph {P Q : AnalyticBelyiPair} (e : P.Iso Q) {n : ℕ} (hP : RiemannSurface.degree ↑P.β = n) (hQ : RiemannSurface.degree ↑Q.β = n) : (e.toTopBranchedCover hP hQ).toHomeomorph = e.toHomeomorph

The homeomorphism underlying the induced isomorphism of topological branched covers is the homeomorphism underlying the isomorphism of analytic Belyi pairs.

theorem TauCeti.AnalyticBelyiPair.Iso.isoClass_monodromyTriple_eq {P Q : AnalyticBelyiPair} {n : ℕ} (e : P.Iso Q) (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (ν' : ↑(Q.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν') = PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν)

Isomorphic analytic Belyi pairs have isomorphic monodromy triples, whatever the numberings of the fibres over 1/2.

Rigidity and finiteness of isomorphisms

theorem TauCeti.AnalyticBelyiPair.Iso.eq_of_apply_eq {P Q : AnalyticBelyiPair} {e e' : P.Iso Q} (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) (h : e ↑x = e' ↑x) : e = e'

An isomorphism of analytic Belyi pairs is determined by the image of one point over ℂ ∖ {0, 1}.

instance TauCeti.AnalyticBelyiPair.Iso.instFinite {P Q : AnalyticBelyiPair} : Finite (P.Iso Q)

There are only finitely many isomorphisms between two analytic Belyi pairs.

theorem TauCeti.AnalyticBelyiPair.Iso.natCard_le_degree {P Q : AnalyticBelyiPair} : Nat.card (P.Iso Q) ≤ RiemannSurface.degree ↑Q.β

There are at most as many isomorphisms between two analytic Belyi pairs as the degree.

The automorphism group

@[instance_reducible]

noncomputable instance TauCeti.AnalyticBelyiPair.Iso.instGroup {P : AnalyticBelyiPair} : Group (P.Iso P)

The automorphism group of an analytic Belyi pair: its automorphisms form a group under composition, e * e' being e' followed by e. It is finite, with order dividing the degree (TauCeti.AnalyticBelyiPair.Iso.natCard_dvd_degree).

theorem TauCeti.AnalyticBelyiPair.Iso.one_def {P : AnalyticBelyiPair} : 1 = Iso.refl P

theorem TauCeti.AnalyticBelyiPair.Iso.mul_def {P : AnalyticBelyiPair} (e e' : P.Iso P) : e * e' = e'.trans e

theorem TauCeti.AnalyticBelyiPair.Iso.inv_def {P : AnalyticBelyiPair} (e : P.Iso P) : e⁻¹ = e.symm

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.one_apply {P : AnalyticBelyiPair} (x : P.X) : 1 x = x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.mul_apply {P : AnalyticBelyiPair} (e e' : P.Iso P) (x : P.X) : (e * e') x = e (e' x)

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.inv_apply {P : AnalyticBelyiPair} (e : P.Iso P) (x : P.X) : e⁻¹ x = e.symm x

@[instance_reducible]

noncomputable instance TauCeti.AnalyticBelyiPair.Iso.instMulActionRestrictFiber (P : AnalyticBelyiPair) (b : ThricePuncturedSphere) : MulAction (P.Iso P) ↑(P.restrict ⁻¹' {b})

Automorphisms of an analytic Belyi pair act on every fibre of its restricted cover by evaluation.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_smul {P : AnalyticBelyiPair} (b : ThricePuncturedSphere) (e : P.Iso P) (x : ↑(P.restrict ⁻¹' {b})) : ↑↑(e • x) = e ↑↑x

On underlying points, the action on a fibre of the restricted cover is evaluation of the automorphism.

instance TauCeti.AnalyticBelyiPair.Iso.instIsCancelSMulRestrictFiber (P : AnalyticBelyiPair) (b : ThricePuncturedSphere) : IsCancelSMul (P.Iso P) ↑(P.restrict ⁻¹' {b})

The action of the automorphism group of an analytic Belyi pair on every fibre of its restricted cover is free.

theorem TauCeti.AnalyticBelyiPair.Iso.natCard_dvd_degree {P : AnalyticBelyiPair} : Nat.card (P.Iso P) ∣ RiemannSurface.degree ↑P.β

The order of the automorphism group of an analytic Belyi pair divides its degree.

Automorphisms, deck transformations and the monodromy triple

noncomputable def TauCeti.AnalyticBelyiPair.isoMulEquivDeck (P : AnalyticBelyiPair) : P.Iso P ≃* ↥(deck ↑P.β)

The automorphisms of an analytic Belyi pair are the deck transformations of its Belyi map, the homeomorphisms of the surface over the sphere: these are automatically biholomorphic (TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph).

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_isoMulEquivDeck_apply (P : AnalyticBelyiPair) (e : P.Iso P) : ⇑↑(P.isoMulEquivDeck e) = ⇑e

The deck transformation of an automorphism of a pair is the automorphism.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_isoMulEquivDeck_symm_apply (P : AnalyticBelyiPair) (φ : ↥(deck ↑P.β)) : ⇑(P.isoMulEquivDeck.symm φ) = ⇑↑φ

The automorphism of a pair given by a deck transformation of its Belyi map is the deck transformation.

noncomputable def TauCeti.AnalyticBelyiPair.isoMulEquivDeckRestrict (P : AnalyticBelyiPair) : P.Iso P ≃* ↥(deck P.restrict)

The automorphisms of an analytic Belyi pair are the deck transformations of its cover of ℂ ∖ {0, 1}. An automorphism goes to its restriction to the points over ℂ ∖ {0, 1} (TauCeti.AnalyticBelyiPair.coe_isoMulEquivDeckRestrict_apply). It is the composite of TauCeti.AnalyticBelyiPair.isoMulEquivDeck and the restriction of deck transformations of the underlying topological branched cover (TauCeti.TopBranchedCover.deckMulEquivDeckRestrict).

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_isoMulEquivDeckRestrict_apply (P : AnalyticBelyiPair) (e : P.Iso P) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(↑(P.isoMulEquivDeckRestrict e) x) = e ↑x

The deck transformation of the cover of ℂ ∖ {0, 1} attached to an automorphism of a pair is the automorphism.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_isoMulEquivDeckRestrict_symm_apply (P : AnalyticBelyiPair) (ψ : ↥(deck P.restrict)) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : (P.isoMulEquivDeckRestrict.symm ψ) ↑x = ↑(↑ψ x)

The automorphism of a pair attached to a deck transformation of its cover of ℂ ∖ {0, 1} is the deck transformation over ℂ ∖ {0, 1}.

noncomputable def TauCeti.AnalyticBelyiPair.isoMulEquivAutomorphismGroup (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : P.Iso P ≃* ↥(⋯.monodromyTriple ν).automorphismGroup

The automorphism group of an analytic Belyi pair is the automorphism group of its monodromy triple, for any numbering ν of the fibre over 1/2. An automorphism goes to the permutation it induces on the labels (TauCeti.AnalyticBelyiPair.coe_isoMulEquivAutomorphismGroup_apply). It is the composite of three identifications: automorphisms of the pair are the deck transformations of the Belyi map, these restrict to the deck transformations of the cover of ℂ ∖ {0, 1} attached to the pair (TauCeti.TopBranchedCover.deckMulEquivDeckRestrict), and those are the automorphisms of its monodromy triple (IsCoveringMap.deckMulEquivAutomorphismGroup).

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_isoMulEquivAutomorphismGroup_apply (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (e : P.Iso P) (i : Fin n) : ↑((P.isoMulEquivAutomorphismGroup ν) e) i = ν (e • ν.symm i)

The automorphism of the monodromy triple attached to an automorphism e of a pair sends the label i to the label of the image under e of the point labelled i.

@[simp]

theorem TauCeti.AnalyticBelyiPair.isoMulEquivAutomorphismGroup_symm_smul (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (τ : ↥(⋯.monodromyTriple ν).automorphismGroup) (i : Fin n) : (P.isoMulEquivAutomorphismGroup ν).symm τ • ν.symm i = ν.symm (↑τ i)

The automorphism of a pair attached to an automorphism τ of its monodromy triple sends the point labelled i to the point labelled τ i.

theorem TauCeti.AnalyticBelyiPair.isRegular_monodromyTriple_iff_natCard_iso {P : AnalyticBelyiPair} {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (⋯.monodromyTriple ν).IsRegular ↔ Nat.card (P.Iso P) = n

The monodromy triple of an analytic Belyi pair is regular exactly when the pair has as many automorphisms as its degree, the number n of points of the fibre over 1/2.

Isomorphism classes of analytic Belyi pairs

def TauCeti.AnalyticBelyiPair.isoSetoid (n : ℕ) : Setoid { P : AnalyticBelyiPair // RiemannSurface.degree ↑P.β = n }

Isomorphism of analytic Belyi pairs of degree n, as an equivalence relation.

theorem TauCeti.AnalyticBelyiPair.isoSetoid_r {n : ℕ} {P Q : { P : AnalyticBelyiPair // RiemannSurface.degree ↑P.β = n }} : (isoSetoid n) P Q ↔ Nonempty ((↑P).Iso ↑Q)

noncomputable def TauCeti.AnalyticBelyiPair.toIsoClass (n : ℕ) : Quotient (isoSetoid n) → PermutationTriple.IsoClass n

The permutation triple of an isomorphism class of analytic Belyi pairs of degree n: the isomorphism class of the monodromy triple of any representative, for any numbering of its fibre over 1/2 (TauCeti.AnalyticBelyiPair.toIsoClass_mk). It is well defined because isomorphic pairs have isomorphic monodromy triples (TauCeti.AnalyticBelyiPair.Iso.isoClass_monodromyTriple_eq).

def TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass (n : ℕ) : Quotient (isoSetoid n) → TopBranchedCover.IsoClass n

The topological branched cover of an isomorphism class of analytic Belyi pairs. This is the analytic-to-topological map in the classification of Belyi pairs: it forgets the complex structure and retains the same map to the sphere.

@[simp]

theorem TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_mk {n : ℕ} (P : { P : AnalyticBelyiPair // RiemannSurface.degree ↑P.β = n }) : toTopBranchedCoverIsoClass n ⟦P⟧ = TopBranchedCover.IsoClass.mk ((↑P).toTopBranchedCover ⋯)

The topological branched-cover class of a pair is represented by its underlying topological branched cover.

theorem TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_injective (n : ℕ) : Function.Injective (toTopBranchedCoverIsoClass n)

Analytic Belyi pairs are determined by their underlying topological branched covers: two analytic Belyi pairs of degree n whose topological branched covers are isomorphic are isomorphic, since a homeomorphism over the sphere is holomorphic (TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph).

theorem TauCeti.AnalyticBelyiPair.toIsoClass_mk {n : ℕ} (P : { P : AnalyticBelyiPair // RiemannSurface.degree ↑P.β = n }) (ν : ↑((↑P).restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : toIsoClass n ⟦P⟧ = PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν)

The permutation triple of the class of an analytic Belyi pair of degree n is the class of its monodromy triple, for any numbering of the fibre over 1/2.

Morphisms of analytic Belyi pairs

structure TauCeti.AnalyticBelyiPair.Hom (P : AnalyticBelyiPair) (Q : AnalyticBelyiPair) : Type (max u v)

A morphism of analytic Belyi pairs P → Q: a holomorphic map of Riemann surfaces P.X → Q.X lying over the Riemann sphere, that is, carrying the Belyi map of Q back to the Belyi map of P. Every continuous map over the sphere is one (TauCeti.AnalyticBelyiPair.Hom.ofContinuous).

• toFun : P.X → Q.X

  The underlying map of Riemann surfaces.

• holomorphic : MDiff self.toFun

  The map is holomorphic.

• β_toFun (x : P.X) : ↑Q.β (self.toFun x) = ↑P.β x

  The map lies over the Riemann sphere.

@[instance_reducible]

instance TauCeti.AnalyticBelyiPair.Hom.instFunLikeX {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} : FunLike (P.Hom Q) P.X Q.X

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.toFun_eq_coe {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : f.toFun = ⇑f

theorem TauCeti.AnalyticBelyiPair.Hom.ext {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {f g : P.Hom Q} (h : ∀ (x : P.X), f x = g x) : f = g

theorem TauCeti.AnalyticBelyiPair.Hom.ext_iff {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {f g : P.Hom Q} : f = g ↔ ∀ (x : P.X), f x = g x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.β_apply {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) (x : P.X) : ↑Q.β (f x) = ↑P.β x

A morphism of analytic Belyi pairs lies over the Riemann sphere.

theorem TauCeti.AnalyticBelyiPair.Hom.β_comp {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : ↑Q.β ∘ ⇑f = ↑P.β

A morphism of analytic Belyi pairs lies over the Riemann sphere.

theorem TauCeti.AnalyticBelyiPair.Hom.mdifferentiable {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : MDiff ⇑f

A morphism of analytic Belyi pairs is holomorphic.

theorem TauCeti.AnalyticBelyiPair.Hom.continuous {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : Continuous ⇑f

A morphism of analytic Belyi pairs is continuous.

def TauCeti.AnalyticBelyiPair.Hom.ofContinuous {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {f : P.X → Q.X} (hf : Continuous f) (hβ : ∀ (x : P.X), ↑Q.β (f x) = ↑P.β x) : P.Hom Q

A continuous map over the sphere is a morphism of analytic Belyi pairs: it is holomorphic by TauCeti.AnalyticBelyiPair.mdifferentiable_of_β.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_ofContinuous {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {f : P.X → Q.X} (hf : Continuous f) (hβ : ∀ (x : P.X), ↑Q.β (f x) = ↑P.β x) : ⇑(ofContinuous hf hβ) = f

def TauCeti.AnalyticBelyiPair.Hom.id (P : AnalyticBelyiPair) : P.Hom P

The identity morphism of an analytic Belyi pair.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_id {P : AnalyticBelyiPair} : ⇑(Hom.id P) = id

def TauCeti.AnalyticBelyiPair.Hom.comp {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {R : AnalyticBelyiPair} (g : Q.Hom R) (f : P.Hom Q) : P.Hom R

The composite of two morphisms of analytic Belyi pairs.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_comp {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {R : AnalyticBelyiPair} (g : Q.Hom R) (f : P.Hom Q) : ⇑(g.comp f) = ⇑g ∘ ⇑f

theorem TauCeti.AnalyticBelyiPair.Hom.comp_apply {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {R : AnalyticBelyiPair} (g : Q.Hom R) (f : P.Hom Q) (x : P.X) : (g.comp f) x = g (f x)

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.comp_id {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : f.comp (Hom.id P) = f

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.id_comp {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : (Hom.id Q).comp f = f

theorem TauCeti.AnalyticBelyiPair.Hom.comp_assoc {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {R : AnalyticBelyiPair} {S : AnalyticBelyiPair} (h : R.Hom S) (g : Q.Hom R) (f : P.Hom Q) : (h.comp g).comp f = h.comp (g.comp f)

def TauCeti.AnalyticBelyiPair.Hom.toFiniteHolomorphicMap {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : RiemannSurface.FiniteHolomorphicMap P.X Q.X

The finite holomorphic map underlying a morphism of analytic Belyi pairs: it takes two distinct values because the Belyi map of the source does.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_toFiniteHolomorphicMap {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : ↑f.toFiniteHolomorphicMap = ⇑f

theorem TauCeti.AnalyticBelyiPair.Hom.surjective {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : Function.Surjective ⇑f

A morphism of analytic Belyi pairs is surjective.

theorem TauCeti.AnalyticBelyiPair.Hom.degree_β_eq_mul_degree {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β * RiemannSurface.degree ⇑f

Degrees multiply along a morphism of analytic Belyi pairs: the degree of the Belyi map of the source is the degree of the Belyi map of the target times the degree of the morphism.

theorem TauCeti.AnalyticBelyiPair.Hom.degree_β_dvd {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : RiemannSurface.degree ↑Q.β ∣ RiemannSurface.degree ↑P.β

The degree of the target of a morphism of analytic Belyi pairs divides the degree of the source.

theorem TauCeti.AnalyticBelyiPair.Hom.degree_eq_one_iff {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : RiemannSurface.degree ⇑f = 1 ↔ RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β

A morphism of analytic Belyi pairs has degree one exactly when its source and target have the same degree.

noncomputable def TauCeti.AnalyticBelyiPair.Hom.toIso {P Q : AnalyticBelyiPair} (f : P.Hom Q) (h : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β) : P.Iso Q

A morphism between analytic Belyi pairs of the same degree is an isomorphism: it has degree one (TauCeti.AnalyticBelyiPair.Hom.degree_eq_one_iff), so it is a biholomorphism.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_toIso {P Q : AnalyticBelyiPair} (f : P.Hom Q) (h : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β) : ⇑(f.toIso h) = ⇑f

def TauCeti.AnalyticBelyiPair.Hom.restrict {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : C(↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint), ↑(↑Q.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint))

The map of covers of ℂ ∖ {0, 1} underlying a morphism of analytic Belyi pairs: its restriction to the points over the thrice-punctured sphere, which commutes with the restricted Belyi maps (TauCeti.AnalyticBelyiPair.Hom.restrict_restrict).

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.coe_restrict_apply {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : ↑(f.restrict x) = f ↑x

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.restrict_restrict {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) (x : ↑(↑P.β ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)) : Q.restrict (f.restrict x) = P.restrict x

The restriction of a morphism of analytic Belyi pairs is a map of covers over ℂ ∖ {0, 1}.

theorem TauCeti.AnalyticBelyiPair.Hom.restrict_comp_restrict {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (f : P.Hom Q) : Q.restrict ∘ ⇑f.restrict = P.restrict

The restriction of a morphism of analytic Belyi pairs is a map of covers over ℂ ∖ {0, 1}.

theorem TauCeti.AnalyticBelyiPair.Hom.semiconj_component_monodromyTriple {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} {n m : ℕ} (f : P.Hom Q) (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (ν' : ↑(Q.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin m) (j : Fin 3) : Function.Semiconj (⇑ν' ∘ Function.fiberMap ⇑f.restrict ⋯ ThricePuncturedSphere.basePt ∘ ⇑ν.symm) ⇑((⋯.monodromyTriple ν).component j) ⇑((⋯.monodromyTriple ν').component j)

A morphism of analytic Belyi pairs intertwines the monodromy triples. Read through numberings ν and ν' of the fibres over 1/2, the map a morphism f : P → Q induces between these fibres carries σ0, σ1 and σinf of the monodromy triple of P to those of Q.

theorem TauCeti.AnalyticBelyiPair.Hom.subsingleton_of_degree_eq_one {P : AnalyticBelyiPair} {Q : AnalyticBelyiPair} (hQ : RiemannSurface.degree ↑Q.β = 1) : Subsingleton (P.Hom Q)

Morphisms into a pair of degree one are unique: the Belyi map of the target is then injective, and every morphism lies over it.

noncomputable def TauCeti.AnalyticBelyiPair.Iso.toHom {P Q : AnalyticBelyiPair} (e : P.Iso Q) : P.Hom Q

The morphism of analytic Belyi pairs underlying an isomorphism.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.coe_toHom {P Q : AnalyticBelyiPair} (e : P.Iso Q) : ⇑e.toHom = ⇑e

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.toHom_refl (P : AnalyticBelyiPair) : (Iso.refl P).toHom = Hom.id P

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.toHom_trans {P Q R : AnalyticBelyiPair} (e : P.Iso Q) (e' : Q.Iso R) : (e.trans e').toHom = e'.toHom.comp e.toHom

@[simp]

theorem TauCeti.AnalyticBelyiPair.Hom.toHom_toIso {P Q : AnalyticBelyiPair} (f : P.Hom Q) (h : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β) : (f.toIso h).toHom = f

The isomorphism given by a morphism between pairs of the same degree has that morphism as its underlying morphism.

@[simp]

theorem TauCeti.AnalyticBelyiPair.Iso.toIso_toHom {P Q : AnalyticBelyiPair} (e : P.Iso Q) (h : RiemannSurface.degree ↑P.β = RiemannSurface.degree ↑Q.β) : e.toHom.toIso h = e

The isomorphism given by the morphism underlying an isomorphism is that isomorphism.

The trivial pair and pairs of degree one

def TauCeti.AnalyticBelyiPair.homPowOne (P : AnalyticBelyiPair) : P.Hom (pow ⋯)

The Belyi map of an analytic Belyi pair, as its morphism to the trivial pair pow one_ne_zero, the identity of the sphere. It is the unique such morphism, so the trivial pair is terminal.

@[simp]

theorem TauCeti.AnalyticBelyiPair.coe_homPowOne (P : AnalyticBelyiPair) : ⇑P.homPowOne = ↑P.β

@[instance_reducible]

instance TauCeti.AnalyticBelyiPair.instUniqueHomPow (P : AnalyticBelyiPair) : Unique (P.Hom (pow ⋯))

The trivial pair is terminal: the Belyi map is the unique morphism from an analytic Belyi pair to the trivial pair, the identity of the sphere.

noncomputable def TauCeti.AnalyticBelyiPair.isoOfDegreeEqOne {P Q : AnalyticBelyiPair} (hP : RiemannSurface.degree ↑P.β = 1) (hQ : RiemannSurface.degree ↑Q.β = 1) : P.Iso Q

Analytic Belyi pairs of degree one are isomorphic: each Belyi map is then a biholomorphism onto the sphere.

theorem TauCeti.AnalyticBelyiPair.degree_β_eq_one_iff_nonempty_iso {P : AnalyticBelyiPair} : RiemannSurface.degree ↑P.β = 1 ↔ Nonempty (P.Iso (pow ⋯))

An analytic Belyi pair has degree one exactly when it is trivial, that is, isomorphic to the identity of the sphere.

instance TauCeti.AnalyticBelyiPair.instSubsingletonQuotientSubtypeEqNatDegreeXOnePointComplexToFunβOfNatIsoSetoid : Subsingleton (Quotient (isoSetoid 1))

There is at most one isomorphism class of analytic Belyi pairs of degree one.

@[instance_reducible]

noncomputable instance TauCeti.AnalyticBelyiPair.instUniqueQuotientSubtypeEqNatDegreeXOnePointComplexToFunβOfNatIsoSetoid : Unique (Quotient (isoSetoid 1))

The class of the trivial pair is the only isomorphism class of analytic Belyi pairs of degree one.