The positive local generator at infinity

The standard punctured neighborhood of infinity is D∞* = {z | 2 < ‖z‖}. Its coordinate w = 1/z identifies it with the punctured disc of radius 1/2, so it is path connected (isPathConnected_puncturedNeighborhoodInf). Taking the direction of w and then the degree of a circle loop identifies its fundamental group with ℤ.

The clockwise large-circle loop δ.symm, restricted to D∞*, has degree +1 in this coordinate. It therefore generates the local fundamental group. Under inclusion into the thrice-punctured sphere and transport to the global basepoint along αPlus.symm, it is exactly periphInf. Transport along any other path has the same conjugacy class. This identifies the local monodromy used to fill a cover at infinity with the third permutation of its triple, including its orientation.

The computation reuses StarConvex.fundamentalGroup_map_directionFrom_bijective, Circle.fundamentalGroupMulEquiv_fromPath, and the large-circle identity periphInf_eq_fromPath.

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, pp. 125–126, for the peripheral loops around the three punctures.

noncomputable def TauCeti.ThricePuncturedSphere.directionAtInf : C(↑puncturedNeighborhoodInf, Circle)

The direction of the local coordinate w = 1/z at infinity.

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_directionAtInf (z : ↑puncturedNeighborhoodInf) : ↑(directionAtInf z) = 1 / ↑↑z / ↑‖1 / ↑↑z‖

The local direction at infinity is the normalization of 1/z.

theorem TauCeti.ThricePuncturedSphere.map_directionAtInf_bijective (z : ↑puncturedNeighborhoodInf) : Function.Bijective ⇑(FundamentalGroup.map directionAtInf z)

The local direction induces a bijection on fundamental groups at every local basepoint.

noncomputable def TauCeti.ThricePuncturedSphere.infFundamentalGroupMulEquivInt (z : ↑puncturedNeighborhoodInf) : FundamentalGroup (↑puncturedNeighborhoodInf) z ≃* Multiplicative ℤ

Winding number in the coordinate w = 1/z identifies π₁(D∞*, z) with ℤ.

Equations

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

theorem TauCeti.ThricePuncturedSphere.infFundamentalGroupMulEquivInt_fromPath {z : ↑puncturedNeighborhoodInf} (γ : Path z z) : (infFundamentalGroupMulEquivInt z) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)) = Multiplicative.ofAdd (Circle.degree (γ.map ⋯))

The local winding number of a loop is the degree of its direction in the infinity chart.

theorem TauCeti.ThricePuncturedSphere.isPathConnected_puncturedNeighborhoodInf : IsPathConnected puncturedNeighborhoodInf

The standard punctured neighborhood of infinity is path connected: in the coordinate w = 1/z it is a punctured disc, which is homotopy equivalent to a circle.

theorem TauCeti.ThricePuncturedSphere.pPlus_mem_puncturedNeighborhoodInf : pPlus ∈ puncturedNeighborhoodInf

The point pPlus lies in the standard punctured neighborhood of infinity.

@[reducible, inline]

noncomputable abbrev TauCeti.ThricePuncturedSphere.infBasePt : ↑puncturedNeighborhoodInf

The basepoint pPlus viewed inside the local neighborhood of infinity.

Equations

• TauCeti.ThricePuncturedSphere.infBasePt = ⟨TauCeti.ThricePuncturedSphere.pPlus, TauCeti.ThricePuncturedSphere.pPlus_mem_puncturedNeighborhoodInf⟩

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_infBasePt : ↑infBasePt = pPlus

noncomputable def TauCeti.ThricePuncturedSphere.δInf : Path infBasePt infBasePt

The clockwise circle δ.symm, as a loop in the punctured neighborhood of infinity.

Equations

• TauCeti.ThricePuncturedSphere.δInf = TauCeti.ThricePuncturedSphere.δ.symm.codRestrict TauCeti.ThricePuncturedSphere.δInf._proof_1✝

@[simp]

theorem TauCeti.ThricePuncturedSphere.map_val_δInf : δInf.map ⋯ = δ.symm

Inclusion of the local loop into the thrice-punctured sphere is the clockwise large circle.

@[simp]

theorem TauCeti.ThricePuncturedSphere.coe_δInf (t : ↑unitInterval) : ↑↑(δInf t) = circleMap 0 3 (Real.arccos (1 / 6) + 2 * Real.pi * (1 - ↑t))

The local loop has the same affine values as the clockwise large circle.

@[simp]

theorem TauCeti.ThricePuncturedSphere.directionAtInf_δInf (t : ↑unitInterval) : directionAtInf (δInf t) = Circle.exp (-Real.arccos (1 / 6) + 2 * Real.pi * ↑t)

In the coordinate at infinity, the direction of δInf has angle -arccos(1/6) + 2πt, increasing by one full turn.

@[simp]

theorem TauCeti.ThricePuncturedSphere.infFundamentalGroupMulEquivInt_δInf : (infFundamentalGroupMulEquivInt infBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δInf)) = Multiplicative.ofAdd 1

The clockwise affine circle is the positive generator in the infinity chart.

@[simp]

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

The local fundamental group at infinity is generated by the clockwise large circle.

theorem TauCeti.ThricePuncturedSphere.transport_δInf_eq_periphInf : (FundamentalGroup.fundamentalGroupMulEquivOfPath αPlus).symm ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } infBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δInf))) = periphInf

Include the local generator and transport along αPlus.symm: the result is periphInf.

theorem TauCeti.ThricePuncturedSphere.conjClassesEquivOfPath_δInf {x : ThricePuncturedSphere} (γ : Path pPlus x) : (FundamentalGroup.conjClassesEquivOfPath γ) (ConjClasses.mk ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } infBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk δInf)))) = x.periphInfClass

Transporting the included positive local generator along any path gives the peripheral conjugacy class at infinity. Thus the class is independent of the transporting path.