Documentation

TauCeti.AlgebraicTopology.ThricePuncturedSphere.SphereCharts

Extending the puncture coordinates to the sphere #

The inverses of the standard puncture coordinates extend across zero to the Riemann sphere. At the finite punctures these maps are w / 2 and 1 - w / 2; at infinity the map is 2 / w, with zero sent to infinity. These continuous parametrisations express the power-map local models of a filled cover in the sphere, including their centres.

The inverted coordinate uses OnePoint.invChart, so continuity at infinity comes from the sphere's existing chart rather than a separate limit argument. For the same reason these maps are holomorphic for the complex structure of the sphere (Puncture.contMDiff_sphereCoordInv), which is what makes the local models of a filled cover holomorphic.

References #

source
def TauCeti.ThricePuncturedSphere.Puncture.toOnePoint :
Puncture → OnePoint ℂ

The point of the Riemann sphere corresponding to a puncture.

Instances For
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.Puncture.toOnePoint_zero :
    zero.toOnePoint = ↑0
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.Puncture.toOnePoint_one :
    one.toOnePoint = ↑1
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.Puncture.toOnePoint_inf :
    inf.toOnePoint = OnePoint.infty
    source
    noncomputable def TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv :
    Puncture → ℂ → OnePoint ℂ

    The inverse standard coordinate at a puncture, extended across zero into the sphere.

    Instances For
      source
      @[simp]
      theorem TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv_zero (w : ℂ) :
      zero.sphereCoordInv w = ↑(w / 2)
      source
      @[simp]
      theorem TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv_one (w : ℂ) :
      one.sphereCoordInv w = ↑(1 - w / 2)
      source
      @[simp]
      theorem TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv_inf (w : ℂ) :
      inf.sphereCoordInv w = ↑OnePoint.invChart.symm (w / 2)
      source
      @[simp]
      theorem TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv_apply_zero (q : Puncture) :
      q.sphereCoordInv 0 = q.toOnePoint

      The extended inverse coordinate takes zero to its puncture.

      source
      theorem TauCeti.ThricePuncturedSphere.Puncture.isOpenEmbedding_sphereCoordInv (q : Puncture) :
      Topology.IsOpenEmbedding q.sphereCoordInv

      Each extended inverse coordinate identifies the plane with an open neighbourhood of its puncture in the sphere.

      source
      theorem TauCeti.ThricePuncturedSphere.Puncture.continuous_sphereCoordInv (q : Puncture) :
      Continuous q.sphereCoordInv

      The inverse puncture coordinates are continuous even at the centre.

      source
      theorem TauCeti.ThricePuncturedSphere.Puncture.contMDiff_sphereCoordInv (q : Puncture) :
      ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ q.sphereCoordInv

      The inverse puncture coordinates are holomorphic maps into the Riemann sphere, even at the centre: at a finite puncture they are affine, and at infinity the inverse of the inverted chart of the sphere.

      source
      @[simp]
      theorem TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv_coord (q : Puncture) (z : ↑q.neighborhood) :
      q.sphereCoordInv ↑(q.coord z) = (↑z).toOnePoint

      Away from the centre, the extended coordinate inverse agrees with the inclusion of the standard punctured neighbourhood into the sphere.