The positive local generators at 0 and 1

The standard punctured neighborhoods of the finite punctures are the punctured discs D₀* = {z | ‖z‖ < 1/2} and D₁* = {z | ‖z - 1‖ < 1/2}. Their fundamental groups are infinite cyclic, and this file names a positive generator of each and identifies it with the peripheral element of the thrice-punctured sphere at the same puncture:

• δZero is the counterclockwise circle of radius 1/4 about 0, based at 1/4, and δOne is the counterclockwise circle of radius 1/4 about 1, based at 3/4;
• each generates the fundamental group of its punctured disc (zpowers_δZero, zpowers_δOne);
• included into ℂ ∖ {0, 1} and transported to the basepoint 1/2 along the real segments αZero and αOne, they are exactly periph0 and periph1 (transport_δZero_eq_periph0, transport_δOne_eq_periph1).

The peripheral loops γ0 and γ1 themselves run on the boundary circles of D₀* and D₁*, so they cannot serve as local loops. The comparison goes through the larger punctured discs of radius 1 about each puncture, which avoid the other puncture and contain both the peripheral loop and the local one. The direction from the puncture is injective on their fundamental groups, and both loops wind once around the puncture, so they are conjugate along the segment (Circle.homotopic_trans_of_degree_map_eq).

This identifies the local monodromy used to fill a cover at 0 and at 1 with the first two permutations of its triple, including their orientation. The puncture at infinity is treated in TauCeti.AlgebraicTopology.ThricePuncturedSphere.InfinityGenerator.

References

• A. Hatcher, Algebraic Topology, Theorem 1.7 and Proposition 1.18.
• 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, §1.2.7, for the punctured discs about the branch values.

The direction from a finite puncture

The puncture 0

noncomputable def TauCeti.ThricePuncturedSphere.zeroBasePt : ↑puncturedNeighborhoodZero

The point 1/4 of the punctured neighborhood of 0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_zeroBasePt : ↑↑zeroBasePt = 1 / 4

noncomputable def TauCeti.ThricePuncturedSphere.δZero : Path zeroBasePt zeroBasePt

The counterclockwise circle t ↦ (1/4)·exp(2πit) of radius 1/4 about 0, based at 1/4, as a loop in the punctured neighborhood of 0.

@[simp]

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

noncomputable def TauCeti.ThricePuncturedSphere.αZero : Path basePt ↑zeroBasePt

The real segment t ↦ 1/2 - t/4 from the basepoint 1/2 to 1/4.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_αZero (t : ↑unitInterval) : ↑(αZero t) = ↑(1 / 2 - ↑t / 4)

theorem TauCeti.ThricePuncturedSphere.isPathConnected_puncturedNeighborhoodZero : IsPathConnected puncturedNeighborhoodZero

The standard punctured neighborhood of 0 is path connected.

@[simp]

theorem TauCeti.ThricePuncturedSphere.zpowers_δZero : Subgroup.zpowers (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δZero)) = ⊤

The counterclockwise circle δZero generates the fundamental group of the punctured neighborhood of 0.

theorem TauCeti.ThricePuncturedSphere.transport_δZero_eq_periph0 : (FundamentalGroup.fundamentalGroupMulEquivOfPath αZero).symm ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } zeroBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δZero))) = periph0

Include the local generator at 0 and transport it along αZero.symm: the result is periph0.

The puncture 1

noncomputable def TauCeti.ThricePuncturedSphere.oneBasePt : ↑puncturedNeighborhoodOne

The point 3/4 of the punctured neighborhood of 1.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_oneBasePt : ↑↑oneBasePt = 3 / 4

noncomputable def TauCeti.ThricePuncturedSphere.δOne : Path oneBasePt oneBasePt

The counterclockwise circle t ↦ 1 - (1/4)·exp(2πit) of radius 1/4 about 1, based at 3/4, as a loop in the punctured neighborhood of 1.

@[simp]

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

noncomputable def TauCeti.ThricePuncturedSphere.αOne : Path basePt ↑oneBasePt

The real segment t ↦ 1/2 + t/4 from the basepoint 1/2 to 3/4.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_αOne (t : ↑unitInterval) : ↑(αOne t) = ↑(1 / 2 + ↑t / 4)

theorem TauCeti.ThricePuncturedSphere.isPathConnected_puncturedNeighborhoodOne : IsPathConnected puncturedNeighborhoodOne

The standard punctured neighborhood of 1 is path connected.

@[simp]

theorem TauCeti.ThricePuncturedSphere.zpowers_δOne : Subgroup.zpowers (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δOne)) = ⊤

The counterclockwise circle δOne generates the fundamental group of the punctured neighborhood of 1.

theorem TauCeti.ThricePuncturedSphere.transport_δOne_eq_periph1 : (FundamentalGroup.fundamentalGroupMulEquivOfPath αOne).symm ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } oneBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δOne))) = periph1

Include the local generator at 1 and transport it along αOne.symm: the result is periph1.