Documentation

TauCeti.AlgebraicTopology.ThricePuncturedSphere.Anharmonic

The anharmonic self-homeomorphisms of the thrice-punctured sphere #

The six Möbius transformations permuting the three punctures {0, 1, ∞} of the Riemann sphere restrict to self-homeomorphisms of the thrice-punctured sphere U = ℂ ∖ {0, 1}:

mapformulapuncturesimage of b = 1/2
identityz()1/2
mob011 − z(0 1)1/2
mob1Infz / (z − 1)(1 ∞)−1
mob0Inf1 / z(0 ∞)2
mobRot1 / (1 − z)(0 1 ∞)2
mobRotInv(z − 1) / z(0 ∞ 1)−1

The identity is Homeomorph.refl, and mob01 is defined with the thrice-punctured sphere itself. The two involutions mob01 and mob1Inf generate the other four: mobRot and mobRotInv are defined as their two composites, and mob0Inf is the composite mob01 ∘ mob1Inf ∘ mob01, which is also mob1Inf ∘ mob01 ∘ mob1Inf (the braid relation of S₃).

Pulling covers back along these maps is the topological counterpart of the action of S₃ on permutation triples by permuting the branch points. The identity and mob01 fix the basepoint b = 1/2; among the nonidentity maps, only mob01 does. The other four maps move it, so they induce maps between fundamental groups at different basepoints. A connecting path identifies these with automorphisms at b, up to inner conjugacy. This choice is separate from their canonical pullback action on covers.

The puncture permutations are recorded by identifying each map with the restriction of a Möbius transformation of the Riemann sphere OnePoint ℂ, that is, with the action of an element of GL (Fin 2) ℂ (Mathlib's OnePoint.instGLAction). The matrices of the two generators are mob01GL = !![-1, 1; 0, 1] and mob1InfGL = !![1, 0; 1, -1], and the value lemmas mob01GL_smul_* and mob1InfGL_smul_* record where each sends 0, 1 and ∞.

Main definitions #

Main results #

References #

The generators and their composites #

source
noncomputable def TauCeti.ThricePuncturedSphere.mob1Inf :
ThricePuncturedSphere ≃ₜ ThricePuncturedSphere

The self-homeomorphism z ↦ z / (z − 1) of the thrice-punctured sphere. It is the anharmonic transformation exchanging the punctures 1 and ∞ and fixing 0; it moves the basepoint 1/2 to −1.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.coe_mob1Inf (z : ThricePuncturedSphere) :
    ↑(mob1Inf z) = ↑z / (↑z - 1)

    mob1Inf has the formula z ↦ z / (z - 1).

    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.mob1Inf_mob1Inf (z : ThricePuncturedSphere) :
    mob1Inf (mob1Inf z) = z

    z ↦ z / (z − 1) is an involution.

    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.symm_mob1Inf :
    mob1Inf.symm = mob1Inf

    mob1Inf is its own inverse.

    source
    noncomputable def TauCeti.ThricePuncturedSphere.mobRot :
    ThricePuncturedSphere ≃ₜ ThricePuncturedSphere

    The self-homeomorphism z ↦ 1 / (1 − z) of the thrice-punctured sphere, the composite mob01 ∘ mob1Inf. It is the anharmonic transformation rotating the punctures 0 ↦ 1 ↦ ∞ ↦ 0; it moves the basepoint 1/2 to 2.

    Equations
    Instances For
      source
      noncomputable def TauCeti.ThricePuncturedSphere.mobRotInv :
      ThricePuncturedSphere ≃ₜ ThricePuncturedSphere

      The self-homeomorphism z ↦ (z − 1) / z of the thrice-punctured sphere, the composite mob1Inf ∘ mob01. It is the anharmonic transformation rotating the punctures 0 ↦ ∞ ↦ 1 ↦ 0, inverse to mobRot; it moves the basepoint 1/2 to −1.

      Equations
      Instances For
        source
        theorem TauCeti.ThricePuncturedSphere.mobRot_apply (z : ThricePuncturedSphere) :
        mobRot z = mob01 (mob1Inf z)

        mobRot is mob01 ∘ mob1Inf.

        source
        theorem TauCeti.ThricePuncturedSphere.mobRotInv_apply (z : ThricePuncturedSphere) :
        mobRotInv z = mob1Inf (mob01 z)

        mobRotInv is mob1Inf ∘ mob01.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.coe_mobRot (z : ThricePuncturedSphere) :
        ↑(mobRot z) = 1 / (1 - ↑z)

        mobRot has the formula z ↦ 1 / (1 - z).

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.coe_mobRotInv (z : ThricePuncturedSphere) :
        ↑(mobRotInv z) = (↑z - 1) / ↑z

        mobRotInv has the formula z ↦ (z - 1) / z.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.mobRot_mobRotInv (z : ThricePuncturedSphere) :
        mobRot (mobRotInv z) = z

        mobRot and mobRotInv are inverse when composed in this order.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.mobRotInv_mobRot (z : ThricePuncturedSphere) :
        mobRotInv (mobRot z) = z

        mobRotInv and mobRot are inverse when composed in this order.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.symm_mobRot :
        mobRot.symm = mobRotInv

        The inverse of mobRot is mobRotInv.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.symm_mobRotInv :
        mobRotInv.symm = mobRot

        The inverse of mobRotInv is mobRot.

        source
        @[simp]
        theorem TauCeti.ThricePuncturedSphere.mobRot_mobRot (z : ThricePuncturedSphere) :
        mobRot (mobRot z) = mobRotInv z

        The square of the rotation mobRot is its inverse.

        source
        theorem TauCeti.ThricePuncturedSphere.mobRot_mobRot_mobRot (z : ThricePuncturedSphere) :
        mobRot (mobRot (mobRot z)) = z

        The rotation mobRot has order three.

        source
        noncomputable def TauCeti.ThricePuncturedSphere.mob0Inf :
        ThricePuncturedSphere ≃ₜ ThricePuncturedSphere

        The self-homeomorphism z ↦ 1 / z of the thrice-punctured sphere, the composite mob01 ∘ mob1Inf ∘ mob01. It is the anharmonic transformation exchanging the punctures 0 and ∞ and fixing 1; it moves the basepoint 1/2 to 2.

        Equations
        Instances For
          source
          theorem TauCeti.ThricePuncturedSphere.mob01_mob1Inf_mob01 (z : ThricePuncturedSphere) :
          mob01 (mob1Inf (mob01 z)) = mob0Inf z

          mob0Inf is mob01 ∘ mob1Inf ∘ mob01.

          source
          @[simp]
          theorem TauCeti.ThricePuncturedSphere.coe_mob0Inf (z : ThricePuncturedSphere) :
          ↑(mob0Inf z) = 1 / ↑z

          mob0Inf has the formula z ↦ 1 / z.

          source
          theorem TauCeti.ThricePuncturedSphere.mob1Inf_mob01_mob1Inf (z : ThricePuncturedSphere) :
          mob1Inf (mob01 (mob1Inf z)) = mob0Inf z

          The braid relation of S₃: mob0Inf is also mob1Inf ∘ mob01 ∘ mob1Inf.

          source
          @[simp]
          theorem TauCeti.ThricePuncturedSphere.mob0Inf_mob0Inf (z : ThricePuncturedSphere) :
          mob0Inf (mob0Inf z) = z

          z ↦ 1 / z is an involution.

          source
          @[simp]
          theorem TauCeti.ThricePuncturedSphere.symm_mob0Inf :
          mob0Inf.symm = mob0Inf

          mob0Inf is its own inverse.

          The images of the basepoint #

          source
          theorem TauCeti.ThricePuncturedSphere.coe_mob1Inf_basePt :
          ↑(mob1Inf basePt) = -1

          mob1Inf sends the basepoint to -1.

          source
          theorem TauCeti.ThricePuncturedSphere.coe_mob0Inf_basePt :
          ↑(mob0Inf basePt) = 2

          mob0Inf sends the basepoint to 2.

          source
          theorem TauCeti.ThricePuncturedSphere.coe_mobRot_basePt :
          ↑(mobRot basePt) = 2

          mobRot sends the basepoint to 2.

          source
          theorem TauCeti.ThricePuncturedSphere.coe_mobRotInv_basePt :
          ↑(mobRotInv basePt) = -1

          mobRotInv sends the basepoint to -1.

          The Möbius transformations of the Riemann sphere #

          source
          noncomputable def TauCeti.ThricePuncturedSphere.mob01GL :
          GL (Fin 2) ℂ

          The matrix !![-1, 1; 0, 1] of the Möbius transformation z ↦ 1 − z, which restricts to mob01 on the thrice-punctured sphere.

          Equations
          Instances For
            source
            noncomputable def TauCeti.ThricePuncturedSphere.mob1InfGL :
            GL (Fin 2) ℂ

            The matrix !![1, 0; 1, -1] of the Möbius transformation z ↦ z / (z − 1), which restricts to mob1Inf on the thrice-punctured sphere.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.coe_mob01GL :
              ↑mob01GL = !![-1, 1; 0, 1]
              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.coe_mob1InfGL :
              ↑mob1InfGL = !![1, 0; 1, -1]
              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob01GL_smul_zero :
              mob01GL • ↑0 = ↑1

              The Möbius transformation of mob01GL sends 0 to 1.

              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob01GL_smul_one :
              mob01GL • ↑1 = ↑0

              The Möbius transformation of mob01GL sends 1 to 0.

              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob01GL_smul_infty :
              mob01GL • OnePoint.infty = OnePoint.infty

              The Möbius transformation of mob01GL fixes ∞.

              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob1InfGL_smul_zero :
              mob1InfGL • ↑0 = ↑0

              The Möbius transformation of mob1InfGL fixes 0.

              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob1InfGL_smul_one :
              mob1InfGL • ↑1 = OnePoint.infty

              The Möbius transformation of mob1InfGL sends 1 to ∞.

              source
              @[simp]
              theorem TauCeti.ThricePuncturedSphere.mob1InfGL_smul_infty :
              mob1InfGL • OnePoint.infty = ↑1

              The Möbius transformation of mob1InfGL sends ∞ to 1.

              source
              theorem TauCeti.ThricePuncturedSphere.toOnePoint_mob01 (z : ThricePuncturedSphere) :
              (mob01 z).toOnePoint = mob01GL • z.toOnePoint

              mob01 is the restriction of the Möbius transformation of mob01GL to the thrice-punctured sphere.

              source
              theorem TauCeti.ThricePuncturedSphere.toOnePoint_mob1Inf (z : ThricePuncturedSphere) :
              (mob1Inf z).toOnePoint = mob1InfGL • z.toOnePoint

              mob1Inf is the restriction of the Möbius transformation of mob1InfGL to the thrice-punctured sphere.

              source
              theorem TauCeti.ThricePuncturedSphere.toOnePoint_mobRot (z : ThricePuncturedSphere) :
              (mobRot z).toOnePoint = (mob01GL * mob1InfGL) • z.toOnePoint

              mobRot is the restriction of the Möbius transformation of mob01GL * mob1InfGL to the thrice-punctured sphere.

              source
              theorem TauCeti.ThricePuncturedSphere.toOnePoint_mobRotInv (z : ThricePuncturedSphere) :
              (mobRotInv z).toOnePoint = (mob1InfGL * mob01GL) • z.toOnePoint

              mobRotInv is the restriction of the Möbius transformation of mob1InfGL * mob01GL to the thrice-punctured sphere.

              source
              theorem TauCeti.ThricePuncturedSphere.toOnePoint_mob0Inf (z : ThricePuncturedSphere) :
              (mob0Inf z).toOnePoint = (mob01GL * mob1InfGL * mob01GL) • z.toOnePoint

              mob0Inf is the restriction of the Möbius transformation of mob01GL * mob1InfGL * mob01GL to the thrice-punctured sphere.