Documentation

TauCeti.AlgebraicTopology.ThricePuncturedSphere.FilledCover.AnalyticBelyiPair

The filled cover as an analytic Belyi pair #

Let p : E → ℂ ∖ {0, 1} be a covering map with finite fibres. Its filled cover TauCeti.FilledCover p is a compact Riemann surface for the charts TauCeti.FilledCover.chartedSpace: the charts of ℂ pulled back along p on E, and at the added point of each component of p ⁻¹' D_q* the inverse of the filled disc of its filling chart. This file proves that the extension TauCeti.FilledCover.fillMap p : FilledCover p → OnePoint ℂ of p is holomorphic for these charts and the two charts of the Riemann sphere. Read in the chart at a point of E, it is the inclusion ℂ → OnePoint ℂ; read in the chart at the added point of a component of local degree e over the puncture q, it is w ↦ w ^ e followed by the inverse q.sphereCoordInv of the standard coordinate at q, which is holomorphic even at w = 0 (TauCeti.ThricePuncturedSphere.Puncture.contMDiff_sphereCoordInv).

Consequently the filled cover of a connected degree-n cover C of ℂ ∖ {0, 1}, with its extended projection, is an analytic Belyi pair of degree n (TauCeti.ConnectedCover.toAnalyticBelyiPair): fillMap is a covering map off {0, 1, ∞} (TauCeti.FilledCover.isCoveringMapOn_fillMap) and is onto the sphere. This is the construction of an analytic Belyi pair from a finite cover of the thrice-punctured sphere, hence from a connected permutation triple, on which analytic Riemann existence for three-point covers rests. Its underlying topological branched cover is the filled cover TauCeti.ConnectedCover.toTopBranchedCover (TauCeti.ConnectedCover.toTopBranchedCoverIsoClass_toAnalyticBelyiPair).

Since a homeomorphism over the sphere between analytic Belyi pairs is holomorphic (TauCeti.AnalyticBelyiPair.Iso.ofHomeomorph), the filled pair is well defined on isomorphism classes of covers (TauCeti.ConnectedCoverClass.toAnalyticBelyiPair). With the uniqueness of the compactification (TauCeti.TopBranchedCover.IsoClass.restrict_bijective) it follows that every topological branched cover of the sphere with branch values in {0, 1, ∞} carries a complex structure making it an analytic Belyi pair, unique up to isomorphism (TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_bijective). Equivalently, analytic Belyi pairs of degree n up to isomorphism correspond to connected degree-n covers of ℂ ∖ {0, 1} up to isomorphism, by restriction and filling (TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass). Composing with the classification of covers by their triples, analytic Belyi pairs of degree n up to isomorphism correspond to connected permutation triples of degree n up to isomorphism, a pair going to its monodromy triple (TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass); so two pairs are isomorphic exactly when their monodromy triples are (TauCeti.AnalyticBelyiPair.nonempty_iso_iff_isoClass_monodromyTriple_eq).

The ramification of a Belyi map is read off its monodromy triple: over 0, 1 and ∞ the local multiplicities of β at the points of the fibre are the cycle lengths of σ0, σ1 and σinf, fixed points included (TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_zero). This is the topological statement for the underlying branched cover, whose local degrees are the local multiplicities. In particular β is unramified over 0, 1 or ∞ exactly when σ0, σ1 or σinf is the identity (TauCeti.AnalyticBelyiPair.monodromyTriple_σ1_eq_one_iff).

Main results #

References #

source
theorem TauCeti.FilledCover.contMDiff_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) :
ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (fillMap p)

The extended projection of the filled cover is holomorphic, indeed analytic, for the charts TauCeti.FilledCover.chartedSpace of the filled cover and the charts of the Riemann sphere.

source
theorem TauCeti.FilledCover.mdifferentiable_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) :
MDiff (fillMap p)

The extended projection of the filled cover is holomorphic, as a map from the filled cover with its charts TauCeti.FilledCover.chartedSpace to the Riemann sphere.

source
noncomputable def TauCeti.ConnectedCover.toAnalyticBelyiPair {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
AnalyticBelyiPair

The filled cover as an analytic Belyi pair. The filled cover of a connected degree-n cover C of ℂ ∖ {0, 1}, with its charts TauCeti.FilledCover.chartedSpace and the extension TauCeti.FilledCover.fillMap of the projection of C, is an analytic Belyi pair, of degree n (TauCeti.ConnectedCover.degree_toAnalyticBelyiPair).

Instances For
    source
    @[simp]
    theorem TauCeti.ConnectedCover.coe_β_toAnalyticBelyiPair {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
    ↑C.toAnalyticBelyiPair.β = FilledCover.fillMap ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))

    The Belyi map of the filled cover is the extension of the projection of C.

    source
    @[simp]
    theorem TauCeti.ConnectedCover.degree_toAnalyticBelyiPair {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
    RiemannSurface.degree ↑C.toAnalyticBelyiPair.β = n

    The analytic Belyi pair of a connected degree-n cover has degree n.

    source
    theorem TauCeti.ConnectedCover.toTopBranchedCoverIsoClass_toAnalyticBelyiPair {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
    AnalyticBelyiPair.toTopBranchedCoverIsoClass n ⟦⟨C.toAnalyticBelyiPair, ⋯⟩⟧ = TopBranchedCover.IsoClass.mk C.toTopBranchedCover

    The topological branched cover underlying the filled analytic Belyi pair of a connected degree-n cover C of ℂ ∖ {0, 1} is the filled branched cover TauCeti.ConnectedCover.toTopBranchedCover of C.

    Isomorphism classes #

    source
    noncomputable def TauCeti.ConnectedCoverClass.toAnalyticBelyiPair {n : ℕ} :
    ConnectedCoverClass ThricePuncturedSphere.basePt n → Quotient (AnalyticBelyiPair.isoSetoid n)

    The filled analytic Belyi pair of an isomorphism class of covers. Filling the punctures of a connected degree-n cover of ℂ ∖ {0, 1} is well defined on isomorphism classes: an isomorphism of covers extends to a homeomorphism of filled covers over the sphere (TauCeti.ConnectedCover.toTopBranchedCoverIso), which is holomorphic.

    Instances For
      source
      @[simp]
      theorem TauCeti.ConnectedCoverClass.toAnalyticBelyiPair_mk {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
      (mk C).toAnalyticBelyiPair = ⟦⟨C.toAnalyticBelyiPair, ⋯⟩⟧

      The filled analytic Belyi pair of the class of C is the class of the filled pair of C.

      source
      @[simp]
      theorem TauCeti.ConnectedCoverClass.toTopBranchedCoverIsoClass_toAnalyticBelyiPair {n : ℕ} (c : ConnectedCoverClass ThricePuncturedSphere.basePt n) :
      AnalyticBelyiPair.toTopBranchedCoverIsoClass n c.toAnalyticBelyiPair = c.toTopBranchedCover

      The topological branched cover underlying the filled analytic Belyi pair of a class of covers is the filled branched cover of that class.

      source
      theorem TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_surjective (n : ℕ) :
      Function.Surjective (toTopBranchedCoverIsoClass n)

      Every topological branched cover of the sphere with branch values in {0, 1, ∞} comes from an analytic Belyi pair: up to isomorphism, it is the underlying branched cover of the filled pair of its unbranched part.

      source
      theorem TauCeti.AnalyticBelyiPair.toTopBranchedCoverIsoClass_bijective (n : ℕ) :
      Function.Bijective (toTopBranchedCoverIsoClass n)

      Analytic Belyi pairs are topological branched covers. Forgetting the complex structure is a bijection from isomorphism classes of analytic Belyi pairs of degree n to isomorphism classes of topological branched covers of the sphere of degree n with branch values in {0, 1, ∞}: every such branched cover carries a complex structure making it an analytic Belyi pair, unique up to isomorphism.

      source
      noncomputable def TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass (n : ℕ) :
      Quotient (isoSetoid n) ≃ ConnectedCoverClass ThricePuncturedSphere.basePt n

      Analytic Belyi pairs are classified by finite covers of the thrice-punctured sphere. Restricting the Belyi map over ℂ ∖ {0, 1} and filling the punctures are inverse bijections between isomorphism classes of analytic Belyi pairs of degree n and isomorphism classes of connected degree-n covers of ℂ ∖ {0, 1}.

      Instances For
        source
        @[simp]
        theorem TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass_apply {n : ℕ} (P : Quotient (isoSetoid n)) :
        (isoClassEquivConnectedCoverClass n) P = (toTopBranchedCoverIsoClass n P).restrict

        The equivalence TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass restricts the underlying topological branched cover over ℂ ∖ {0, 1}.

        source
        @[simp]
        theorem TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass_symm_apply {n : ℕ} (c : ConnectedCoverClass ThricePuncturedSphere.basePt n) :
        (isoClassEquivConnectedCoverClass n).symm c = c.toAnalyticBelyiPair

        The inverse of TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass is the filled analytic Belyi pair.

        Classification by permutation triples #

        source
        noncomputable def TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass (n : ℕ) :
        Quotient (isoSetoid n) ≃ ConnectedIsoClass n

        Analytic Belyi pairs are classified by their permutation triples. Isomorphism classes of analytic Belyi pairs of degree n correspond to isomorphism classes of connected permutation triples of degree n: the class of a pair goes to the class of the monodromy triple of the cover of ℂ ∖ {0, 1} attached to it (TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass_mk).

        Instances For
          source
          theorem TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass_apply {n : ℕ} (P : Quotient (isoSetoid n)) :
          (isoClassEquivConnectedIsoClass n) P = ((isoClassEquivConnectedCoverClass n) P).isoClass

          The classification TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass is the classification of the class of covers of ℂ ∖ {0, 1} attached to a class of pairs by TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass.

          source
          theorem TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass_mk {n : ℕ} (P : { P : AnalyticBelyiPair // RiemannSurface.degree ↑P.β = n }) (ν : ↑((↑P).restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          (isoClassEquivConnectedIsoClass n) ⟦P⟧ = ConnectedIsoClass.mk ⟨⋯.monodromyTriple ν, ⋯⟩

          The classification TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass sends the class of a pair to the class of its monodromy triple, for any numbering of its fibre over 1/2.

          source
          @[simp]
          theorem TauCeti.AnalyticBelyiPair.forget_isoClassEquivConnectedIsoClass {n : ℕ} (P : Quotient (isoSetoid n)) :
          ((isoClassEquivConnectedIsoClass n) P).forget = toIsoClass n P

          Forgetting connectedness, the classification TauCeti.AnalyticBelyiPair.isoClassEquivConnectedIsoClass is the permutation triple TauCeti.AnalyticBelyiPair.toIsoClass of a class of pairs.

          source
          theorem TauCeti.AnalyticBelyiPair.toIsoClass_injective (n : ℕ) :
          Function.Injective (toIsoClass n)

          An analytic Belyi pair is determined up to isomorphism by its permutation triple.

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

          Two analytic Belyi pairs are isomorphic exactly when their monodromy triples are, for any numberings of their fibres over 1/2 by the same Fin n.

          Ramification over 0, 1 and ∞ #

          source
          theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_zero (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          Multiset.map (RiemannSurface.localMultiplicity ↑P.β) ⋯.toFinset.val = (⋯.monodromyTriple ν).σ0.fullCycleType

          The ramification of a Belyi map over 0. The local multiplicities of the Belyi map of an analytic Belyi pair at the points over 0 are the cycle lengths of σ0 in the monodromy triple of the pair, fixed points included.

          source
          theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_one (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          Multiset.map (RiemannSurface.localMultiplicity ↑P.β) ⋯.toFinset.val = (⋯.monodromyTriple ν).σ1.fullCycleType

          The ramification of a Belyi map over 1. The local multiplicities of the Belyi map of an analytic Belyi pair at the points over 1 are the cycle lengths of σ1 in the monodromy triple of the pair, fixed points included.

          source
          theorem TauCeti.AnalyticBelyiPair.map_localMultiplicity_fiber_inf (P : AnalyticBelyiPair) {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          Multiset.map (RiemannSurface.localMultiplicity ↑P.β) ⋯.toFinset.val = (⋯.monodromyTriple ν).σinf.fullCycleType

          The ramification of a Belyi map over ∞. The local multiplicities of the Belyi map of an analytic Belyi pair at the points over ∞ are the cycle lengths of σinf in the monodromy triple of the pair, fixed points included.

          source
          theorem TauCeti.AnalyticBelyiPair.monodromyTriple_σ0_eq_one_iff {P : AnalyticBelyiPair} {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          (⋯.monodromyTriple ν).σ0 = 1 ↔ ↑0 ∉ P.β.branchValues

          A Belyi map is unramified over 0 exactly when σ0 is the identity, in the monodromy triple of the pair for any numbering of its fibre over 1/2.

          source
          theorem TauCeti.AnalyticBelyiPair.monodromyTriple_σ1_eq_one_iff {P : AnalyticBelyiPair} {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          (⋯.monodromyTriple ν).σ1 = 1 ↔ ↑1 ∉ P.β.branchValues

          A Belyi map is unramified over 1 exactly when σ1 is the identity, in the monodromy triple of the pair for any numbering of its fibre over 1/2.

          source
          theorem TauCeti.AnalyticBelyiPair.monodromyTriple_σinf_eq_one_iff {P : AnalyticBelyiPair} {n : ℕ} (ν : ↑(P.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          (⋯.monodromyTriple ν).σinf = 1 ↔ OnePoint.infty ∉ P.β.branchValues

          A Belyi map is unramified over ∞ exactly when σinf is the identity, in the monodromy triple of the pair for any numbering of its fibre over 1/2.

          The filled pair of a cover #

          source
          theorem TauCeti.ConnectedCover.isoClass_monodromyTriple_toAnalyticBelyiPair {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) (ν : ↑(C.toAnalyticBelyiPair.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) (ν' : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover)) ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) :
          PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν) = PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν')

          The filled pair of a cover has the monodromy of the cover: the monodromy triple of the filled analytic Belyi pair of C is isomorphic to the monodromy triple of C, for any numberings of the two fibres over 1/2.

          source
          noncomputable def TauCeti.ConnectedCover.deckMulEquivIso {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) :
          ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) ≃* C.toAnalyticBelyiPair.Iso C.toAnalyticBelyiPair

          The deck transformations of a cover are the automorphisms of its filled pair. A deck transformation h of a connected degree-n cover C of ℂ ∖ {0, 1} extends to an automorphism of the filled analytic Belyi pair of C, which is h on the total space of C (TauCeti.ConnectedCover.deckMulEquivIso_apply_incl), and every automorphism of the pair is the extension of exactly one deck transformation.

          Instances For
            source
            @[simp]
            theorem TauCeti.ConnectedCover.deckMulEquivIso_apply_incl {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) (h : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover)))) (x : ↑C.cover.obj.left) :
            (C.deckMulEquivIso h) (PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) x) = PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) (h • x)

            The automorphism TauCeti.ConnectedCover.deckMulEquivIso h of the filled pair is the deck transformation h on the total space of C.