The peripheral loops of the thrice-punctured sphere

The fundamental group of the thrice-punctured sphere ℂ ∖ {0, 1} at the basepoint b = 1/2 is generated by loops around the punctures. This file fixes the two loops that serve as its free generators and the three peripheral elements of the fundamental group built from them. The monodromy of a three-point cover along these elements is the permutation triple of the cover.

• γ0 t = (1/2)·exp(2πit) is the circle of radius 1/2 about the puncture 0, and γ1 t = 1 − (1/2)·exp(2πit) is the circle of radius 1/2 about the puncture 1. Both start and end at b, and both run counterclockwise in the affine coordinate z.
• The circle γ0 lies in the open set A = {re z < 1} of the standard two-set cover, and γ1 lies in B = {0 < re z}. The two circles are externally tangent: the distance between their centres is the sum of their radii, and they meet only at b.
• The involution z ↦ 1 − z carries γ0 to γ1 and back, pointwise on the unit interval. As it fixes b, no connecting path is needed to compare the two loops.
• periph0 and periph1 are the classes of γ0 and γ1 in the fundamental group, and periphInf := (periph1 * periph0)⁻¹, so that periphInf * periph1 * periph0 = 1 holds by definition. In FundamentalGroup, γ * δ is the class of the path traversing δ first, so periph1 * periph0 is the class of "γ0, then γ1".
• Transporting these elements to another basepoint depends on a path, but their conjugacy classes do not. The classes periph0Class, periph1Class, and periphInfClass therefore make the peripheral data available canonically at every basepoint.

Main declarations

• TauCeti.ThricePuncturedSphere.γ0, TauCeti.ThricePuncturedSphere.γ1: the two loops at b.
• norm_coe_γ0, norm_coe_γ1_sub_one: γ0 runs on the circle |z| = 1/2 and γ1 on the circle |z − 1| = 1/2.
• γ0_mem_leftOpen, γ1_mem_rightOpen: γ0 stays in A and γ1 stays in B.
• range_γ0_inter_range_γ1: the two loops meet only at the basepoint.
• mob01_basePt, mob01_γ0, mob01_γ1: z ↦ 1 − z fixes the basepoint and exchanges the two loops.
• periph0, periph1, periphInf, periphInf_mul_periph1_mul_periph0: the peripheral elements of the fundamental group and their product relation.
• periph0Class, periph1Class, periphInfClass: the three peripheral conjugacy classes at an arbitrary basepoint, together with their path-transport rules.
• homeomorphMulEquivOfEq_mob01_periph0, homeomorphMulEquivOfEq_mob01_periph1, homeomorphMulEquivOfEq_mob01_periphInf: the automorphism of the fundamental group induced by z ↦ 1 − z exchanges periph0 and periph1 and conjugates periphInf by periph1.

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 (the loops around the three punctures of the sphere and their product relation).

noncomputable def TauCeti.ThricePuncturedSphere.γ0 : Path basePt basePt

The peripheral loop around the puncture 0: the circle t ↦ (1/2)·exp(2πit) of radius 1/2 about 0, based at b = 1/2 and traversed counterclockwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ThricePuncturedSphere.γ1 : Path basePt basePt

The peripheral loop around the puncture 1: the circle t ↦ 1 − (1/2)·exp(2πit) of radius 1/2 about 1, based at b = 1/2 and traversed counterclockwise.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_γ0 (t : ↑unitInterval) : ↑(γ0 t) = circleMap 0 (1 / 2) (2 * Real.pi * ↑t)

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_γ1 (t : ↑unitInterval) : ↑(γ1 t) = circleMap 1 (-(1 / 2)) (2 * Real.pi * ↑t)

theorem TauCeti.ThricePuncturedSphere.coe_γ0_eq_exp (t : ↑unitInterval) : ↑(γ0 t) = 1 / 2 * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑t)

The loop γ0 is t ↦ (1/2)·exp(2πit).

theorem TauCeti.ThricePuncturedSphere.coe_γ1_eq_exp (t : ↑unitInterval) : ↑(γ1 t) = 1 - 1 / 2 * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑t)

The loop γ1 is t ↦ 1 − (1/2)·exp(2πit).

theorem TauCeti.ThricePuncturedSphere.norm_coe_γ0 (t : ↑unitInterval) : ‖↑(γ0 t)‖ = 1 / 2

The loop γ0 lies on the circle of radius 1/2 about 0.

theorem TauCeti.ThricePuncturedSphere.norm_coe_γ1_sub_one (t : ↑unitInterval) : ‖↑(γ1 t) - 1‖ = 1 / 2

The loop γ1 lies on the circle of radius 1/2 about 1.

theorem TauCeti.ThricePuncturedSphere.γ0_mem_leftOpen (t : ↑unitInterval) : γ0 t ∈ leftOpen

The loop γ0 lies in the open set A = {re z < 1} of the standard cover.

theorem TauCeti.ThricePuncturedSphere.γ1_mem_rightOpen (t : ↑unitInterval) : γ1 t ∈ rightOpen

The loop γ1 lies in the open set B = {0 < re z} of the standard cover.

theorem TauCeti.ThricePuncturedSphere.range_γ0_inter_range_γ1 : Set.range ⇑γ0 ∩ Set.range ⇑γ1 = {basePt}

The two peripheral loops meet only at the basepoint: the circles |z| = 1/2 and |z − 1| = 1/2 are externally tangent at 1/2.

@[simp]

theorem TauCeti.ThricePuncturedSphere.mob01_basePt : mob01 basePt = basePt

The involution z ↦ 1 − z fixes the basepoint 1/2.

@[simp]

theorem TauCeti.ThricePuncturedSphere.mob01_γ0 (t : ↑unitInterval) : mob01 (γ0 t) = γ1 t

The involution z ↦ 1 − z carries the loop around 0 to the loop around 1, pointwise on the unit interval.

@[simp]

theorem TauCeti.ThricePuncturedSphere.mob01_γ1 (t : ↑unitInterval) : mob01 (γ1 t) = γ0 t

The involution z ↦ 1 − z carries the loop around 1 to the loop around 0, pointwise on the unit interval.

The peripheral elements of the fundamental group

noncomputable def TauCeti.ThricePuncturedSphere.periph0 : FundamentalGroup ThricePuncturedSphere basePt

The peripheral element at the puncture 0: the class of the loop γ0.

Equations

• TauCeti.ThricePuncturedSphere.periph0 = FundamentalGroup.fromPath ⟦TauCeti.ThricePuncturedSphere.γ0⟧

noncomputable def TauCeti.ThricePuncturedSphere.periph1 : FundamentalGroup ThricePuncturedSphere basePt

The peripheral element at the puncture 1: the class of the loop γ1.

Equations

• TauCeti.ThricePuncturedSphere.periph1 = FundamentalGroup.fromPath ⟦TauCeti.ThricePuncturedSphere.γ1⟧

noncomputable def TauCeti.ThricePuncturedSphere.periphInf : FundamentalGroup ThricePuncturedSphere basePt

The peripheral element at the puncture ∞, defined as (periph1 * periph0)⁻¹ so that the three peripheral elements have product one.

Equations

• TauCeti.ThricePuncturedSphere.periphInf = (TauCeti.ThricePuncturedSphere.periph1 * TauCeti.ThricePuncturedSphere.periph0)⁻¹

theorem TauCeti.ThricePuncturedSphere.periph0_def : periph0 = FundamentalGroup.fromPath ⟦γ0⟧

theorem TauCeti.ThricePuncturedSphere.periph1_def : periph1 = FundamentalGroup.fromPath ⟦γ1⟧

theorem TauCeti.ThricePuncturedSphere.periphInf_def : periphInf = (periph1 * periph0)⁻¹

theorem TauCeti.ThricePuncturedSphere.periphInf_mul_periph1_mul_periph0 : periphInf * periph1 * periph0 = 1

The product relation of the three peripheral elements.

Peripheral conjugacy classes at arbitrary basepoints

noncomputable def TauCeti.ThricePuncturedSphere.periph0Class (x : ThricePuncturedSphere) : ConjClasses (FundamentalGroup ThricePuncturedSphere x)

The conjugacy class of a peripheral loop around 0, canonically transported from basePt to the basepoint x.

Equations

• x.periph0Class = (FundamentalGroup.conjClassesEquivOfPathConnected TauCeti.ThricePuncturedSphere.basePt x) (ConjClasses.mk TauCeti.ThricePuncturedSphere.periph0)

noncomputable def TauCeti.ThricePuncturedSphere.periph1Class (x : ThricePuncturedSphere) : ConjClasses (FundamentalGroup ThricePuncturedSphere x)

The conjugacy class of a peripheral loop around 1, canonically transported from basePt to the basepoint x.

Equations

• x.periph1Class = (FundamentalGroup.conjClassesEquivOfPathConnected TauCeti.ThricePuncturedSphere.basePt x) (ConjClasses.mk TauCeti.ThricePuncturedSphere.periph1)

noncomputable def TauCeti.ThricePuncturedSphere.periphInfClass (x : ThricePuncturedSphere) : ConjClasses (FundamentalGroup ThricePuncturedSphere x)

The conjugacy class of a peripheral loop around ∞, canonically transported from basePt to the basepoint x.

Equations

• x.periphInfClass = (FundamentalGroup.conjClassesEquivOfPathConnected TauCeti.ThricePuncturedSphere.basePt x) (ConjClasses.mk TauCeti.ThricePuncturedSphere.periphInf)

@[simp]

theorem TauCeti.ThricePuncturedSphere.periph0Class_basePt : basePt.periph0Class = ConjClasses.mk periph0

At the standard basepoint, the canonical peripheral class around 0 is the class of periph0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.periph1Class_basePt : basePt.periph1Class = ConjClasses.mk periph1

At the standard basepoint, the canonical peripheral class around 1 is the class of periph1.

@[simp]

theorem TauCeti.ThricePuncturedSphere.periphInfClass_basePt : basePt.periphInfClass = ConjClasses.mk periphInf

At the standard basepoint, the canonical peripheral class around ∞ is the class of periphInf.

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_mk_periph0 {x : ThricePuncturedSphere} (γ : Path basePt x) : (FundamentalGroup.conjClassesEquivOfPath γ) (ConjClasses.mk periph0) = x.periph0Class

Transport along any path from basePt carries periph0 to a representative of the canonical peripheral conjugacy class around 0.

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_mk_periph1 {x : ThricePuncturedSphere} (γ : Path basePt x) : (FundamentalGroup.conjClassesEquivOfPath γ) (ConjClasses.mk periph1) = x.periph1Class

Transport along any path from basePt carries periph1 to a representative of the canonical peripheral conjugacy class around 1.

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_mk_periphInf {x : ThricePuncturedSphere} (γ : Path basePt x) : (FundamentalGroup.conjClassesEquivOfPath γ) (ConjClasses.mk periphInf) = x.periphInfClass

Transport along any path from basePt carries periphInf to a representative of the canonical peripheral conjugacy class around ∞.

@[simp]

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_periph0Class {x y : ThricePuncturedSphere} (γ : Path x y) : (FundamentalGroup.conjClassesEquivOfPath γ) x.periph0Class = y.periph0Class

The peripheral conjugacy class around 0 is preserved by basepoint change.

@[simp]

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_periph1Class {x y : ThricePuncturedSphere} (γ : Path x y) : (FundamentalGroup.conjClassesEquivOfPath γ) x.periph1Class = y.periph1Class

The peripheral conjugacy class around 1 is preserved by basepoint change.

@[simp]

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_periphInfClass {x y : ThricePuncturedSphere} (γ : Path x y) : (FundamentalGroup.conjClassesEquivOfPath γ) x.periphInfClass = y.periphInfClass

The peripheral conjugacy class around ∞ is preserved by basepoint change.

The involution z ↦ 1 − z on the fundamental group

Since mob01 fixes the basepoint, it induces an automorphism of π₁(ℂ ∖ {0, 1}, 1/2) with no choice of connecting path. It exchanges the two peripheral loops on the nose, so it exchanges periph0 and periph1, and it carries periphInf to its conjugate by periph1. These are the values that make the pullback of a cover along z ↦ 1 − z exchange the roles of 0 and 1 in its monodromy triple. The three lemmas are not simp lemmas: homeomorphMulEquivOfEq_apply already rewrites their left-hand sides to FundamentalGroup.mapOfEq, so they are used by rw.

theorem TauCeti.ThricePuncturedSphere.homeomorphMulEquivOfEq_mob01_periph0 : (FundamentalGroup.homeomorphMulEquivOfEq mob01 mob01_basePt) periph0 = periph1

The automorphism of the fundamental group induced by z ↦ 1 − z sends periph0 to periph1.

theorem TauCeti.ThricePuncturedSphere.homeomorphMulEquivOfEq_mob01_periph1 : (FundamentalGroup.homeomorphMulEquivOfEq mob01 mob01_basePt) periph1 = periph0

The automorphism of the fundamental group induced by z ↦ 1 − z sends periph1 to periph0.

theorem TauCeti.ThricePuncturedSphere.homeomorphMulEquivOfEq_mob01_periphInf : (FundamentalGroup.homeomorphMulEquivOfEq mob01 mob01_basePt) periphInf = periph1⁻¹ * periphInf * periph1

The automorphism of the fundamental group induced by z ↦ 1 − z sends periphInf to its conjugate periph1⁻¹ * periphInf * periph1, the third component of the branch-point operation exchanging 0 and 1.