The thrice-punctured sphere

The thrice-punctured sphere ℙ¹(ℂ) ∖ {0, 1, ∞} is the base of the three-point covers classified by permutation triples and dessins d'enfants. This file fixes its affine model TauCeti.ThricePuncturedSphere := {z : ℂ // z ≠ 0 ∧ z ≠ 1}, together with the point-set facts the computation of its fundamental group and the classification of its finite covers run on.

• The space. It is an open subset of ℂ, hence Hausdorff, second countable, strongly locally contractible, locally path-connected and semilocally simply connected; it is path-connected because the complement of a countable set in ℂ is. The inclusion into the Riemann sphere OnePoint ℂ is an open embedding whose range is the complement of {0, 1, ∞}, which is what makes the name honest.
• The basepoint and its symmetry. The basepoint is b = 1/2, on the real segment between the punctures 0 and 1; the involution z ↦ 1 − z fixes it.
• The standard two-set cover by A = {z | re z < 1} and B = {z | 0 < re z}. The set A is the convex half-plane re z < 1 with the puncture 0 removed, B is the half-plane 0 < re z with the puncture 1 removed, and A ∩ B is the open vertical strip 0 < re z < 1, with no point removed because both punctures lie on its boundary lines. The strip is convex, so A ∩ B is path-connected and simply connected, and it contains b. These are the hypotheses on the intersection in the Seifert–van Kampen theorem for two open sets with simply connected intersection, through which π₁ of the thrice-punctured sphere is computed to be free of rank two.

Main declarations

• TauCeti.ThricePuncturedSphere: the space ℂ ∖ {0, 1}.
• TauCeti.ThricePuncturedSphere.range_coe, TauCeti.ThricePuncturedSphere.isOpenEmbedding_coe: the open embedding into ℂ, with range {0, 1}ᶜ.
• TauCeti.ThricePuncturedSphere.toOnePoint, isOpenEmbedding_toOnePoint, range_toOnePoint: the open embedding into the Riemann sphere, with range {0, 1, ∞}ᶜ.
• TauCeti.ThricePuncturedSphere.basePt: the basepoint 1/2.
• TauCeti.ThricePuncturedSphere.mob01: the self-homeomorphism z ↦ 1 − z.
• TauCeti.ThricePuncturedSphere.leftOpen, TauCeti.ThricePuncturedSphere.rightOpen: the open sets A and B of the standard cover, with leftOpen_union_rightOpen, image_coe_leftOpen, image_coe_rightOpen, image_coe_leftOpen_inter_rightOpen, isSimplyConnected_leftOpen_inter_rightOpen and isPathConnected_leftOpen_inter_rightOpen.

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, §2.4 (the thrice-punctured sphere as the base of three-point covers).
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.20 (the Seifert–van Kampen theorem whose hypotheses the standard cover satisfies).

@[reducible, inline]

abbrev TauCeti.ThricePuncturedSphere : Type

The thrice-punctured sphere ℙ¹(ℂ) ∖ {0, 1, ∞}, in its affine model ℂ ∖ {0, 1}. The point ∞ is removed by working in ℂ; TauCeti.ThricePuncturedSphere.range_toOnePoint identifies it with the complement of {0, 1, ∞} in the Riemann sphere OnePoint ℂ.

Equations

• TauCeti.ThricePuncturedSphere = { z : ℂ // z ≠ 0 ∧ z ≠ 1 }

@[simp]

theorem TauCeti.ThricePuncturedSphere.ne_zero (z : ThricePuncturedSphere) : ↑z ≠ 0

A point of the thrice-punctured sphere is not the puncture 0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.ne_one (z : ThricePuncturedSphere) : ↑z ≠ 1

A point of the thrice-punctured sphere is not the puncture 1.

theorem TauCeti.ThricePuncturedSphere.range_coe : Set.range Subtype.val = {0, 1}ᶜ

The points of ℂ underlying the thrice-punctured sphere are those other than 0 and 1.

theorem TauCeti.ThricePuncturedSphere.isOpenEmbedding_coe : Topology.IsOpenEmbedding Subtype.val

The inclusion of the thrice-punctured sphere into ℂ is an open embedding.

instance TauCeti.ThricePuncturedSphere.instStronglyLocallyContractibleSpace : StronglyLocallyContractibleSpace ThricePuncturedSphere

The thrice-punctured sphere is strongly locally contractible, being an open subset of ℂ. In particular it is locally path-connected and semilocally simply connected.

instance TauCeti.ThricePuncturedSphere.instPathConnectedSpace : PathConnectedSpace ThricePuncturedSphere

The thrice-punctured sphere is path-connected: the complement of a countable set in ℂ is path-connected, since ℂ has real dimension two.

The Riemann sphere

def TauCeti.ThricePuncturedSphere.toOnePoint (z : ThricePuncturedSphere) : OnePoint ℂ

The inclusion of the thrice-punctured sphere into the Riemann sphere OnePoint ℂ.

Equations

• z.toOnePoint = ↑↑z

@[simp]

theorem TauCeti.ThricePuncturedSphere.toOnePoint_apply (z : ThricePuncturedSphere) : z.toOnePoint = ↑↑z

theorem TauCeti.ThricePuncturedSphere.isOpenEmbedding_toOnePoint : Topology.IsOpenEmbedding toOnePoint

The thrice-punctured sphere is an open subspace of the Riemann sphere.

theorem TauCeti.ThricePuncturedSphere.range_toOnePoint : Set.range toOnePoint = {↑0, ↑1, OnePoint.infty}ᶜ

The range of the inclusion into the Riemann sphere is the complement of the three punctures 0, 1 and ∞.

The basepoint

noncomputable def TauCeti.ThricePuncturedSphere.basePt : ThricePuncturedSphere

The basepoint b = 1/2 of the thrice-punctured sphere, on the real segment between the punctures 0 and 1.

Equations

• TauCeti.ThricePuncturedSphere.basePt = ⟨1 / 2, TauCeti.ThricePuncturedSphere.basePt._proof_2✝⟩

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_basePt : ↑basePt = 1 / 2

The standard two-set cover

def TauCeti.ThricePuncturedSphere.leftOpen : Set ThricePuncturedSphere

The open set A = {z | re z < 1} of the standard two-set cover of the thrice-punctured sphere: the half-plane re z < 1 with the puncture 0 removed.

Equations

• TauCeti.ThricePuncturedSphere.leftOpen = {z : TauCeti.ThricePuncturedSphere | (↑z).re < 1}

def TauCeti.ThricePuncturedSphere.rightOpen : Set ThricePuncturedSphere

The open set B = {z | 0 < re z} of the standard two-set cover of the thrice-punctured sphere: the half-plane 0 < re z with the puncture 1 removed.

Equations

• TauCeti.ThricePuncturedSphere.rightOpen = {z : TauCeti.ThricePuncturedSphere | 0 < (↑z).re}

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_leftOpen {z : ThricePuncturedSphere} : z ∈ leftOpen ↔ (↑z).re < 1

@[simp]

theorem TauCeti.ThricePuncturedSphere.mem_rightOpen {z : ThricePuncturedSphere} : z ∈ rightOpen ↔ 0 < (↑z).re

theorem TauCeti.ThricePuncturedSphere.isOpen_leftOpen : IsOpen leftOpen

The set leftOpen is open in the thrice-punctured sphere.

theorem TauCeti.ThricePuncturedSphere.isOpen_rightOpen : IsOpen rightOpen

The set rightOpen is open in the thrice-punctured sphere.

@[simp]

theorem TauCeti.ThricePuncturedSphere.leftOpen_union_rightOpen : leftOpen ∪ rightOpen = Set.univ

The two open sets A and B cover the thrice-punctured sphere: a point with re z < 1 lies in A, and otherwise re z ≥ 1 > 0 puts it in B.

theorem TauCeti.ThricePuncturedSphere.image_coe_leftOpen : Subtype.val '' leftOpen = {z : ℂ | z.re < 1} \ {0}

In ℂ, the set A is the half-plane re z < 1 with the puncture 0 removed. The point 1 is not removed, as it does not lie in the half-plane.

theorem TauCeti.ThricePuncturedSphere.image_coe_rightOpen : Subtype.val '' rightOpen = {z : ℂ | 0 < z.re} \ {1}

In ℂ, the set B is the half-plane 0 < re z with the puncture 1 removed. The point 0 is not removed, as it does not lie in the half-plane.

theorem TauCeti.ThricePuncturedSphere.image_coe_leftOpen_inter_rightOpen : Subtype.val '' (leftOpen ∩ rightOpen) = {z : ℂ | 0 < z.re ∧ z.re < 1}

In ℂ, the intersection A ∩ B is the open vertical strip 0 < re z < 1, with no point removed: both punctures lie on the boundary lines of the strip.

theorem TauCeti.ThricePuncturedSphere.isSimplyConnected_leftOpen_inter_rightOpen : IsSimplyConnected (leftOpen ∩ rightOpen)

The intersection A ∩ B of the standard two-set cover is simply connected: it is homeomorphic to the open vertical strip 0 < re z < 1, which is convex and nonempty, hence contractible.

theorem TauCeti.ThricePuncturedSphere.isPathConnected_leftOpen_inter_rightOpen : IsPathConnected (leftOpen ∩ rightOpen)

The intersection A ∩ B of the standard two-set cover is path-connected.

theorem TauCeti.ThricePuncturedSphere.basePt_mem_leftOpen : basePt ∈ leftOpen

The basepoint 1/2 lies in leftOpen.

theorem TauCeti.ThricePuncturedSphere.basePt_mem_rightOpen : basePt ∈ rightOpen

The basepoint 1/2 lies in rightOpen.

theorem TauCeti.ThricePuncturedSphere.basePt_mem_leftOpen_inter_rightOpen : basePt ∈ leftOpen ∩ rightOpen

The basepoint 1/2 lies in the strip A ∩ B.

noncomputable def TauCeti.ThricePuncturedSphere.mob01 : ThricePuncturedSphere ≃ₜ ThricePuncturedSphere

The self-homeomorphism z ↦ 1 − z of the thrice-punctured sphere. It is the anharmonic transformation exchanging the punctures 0 and 1 and fixing ∞, and among the six anharmonic transformations it is the only nonidentity one fixing the basepoint 1/2.

Equations

• TauCeti.ThricePuncturedSphere.mob01 = (IsometryEquiv.subLeft 1).toHomeomorph.subtype TauCeti.ThricePuncturedSphere.mob01._proof_3✝

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_mob01 (z : ThricePuncturedSphere) : ↑(mob01 z) = 1 - ↑z

@[simp]

theorem TauCeti.ThricePuncturedSphere.mob01_mob01 (z : ThricePuncturedSphere) : mob01 (mob01 z) = z

z ↦ 1 − z is an involution.

@[simp]

theorem TauCeti.ThricePuncturedSphere.symm_mob01 : mob01.symm = mob01

mob01 is its own inverse.