The fundamental groups of the two open sets of the standard cover

The thrice-punctured sphere ℂ ∖ {0, 1} is covered by the two open sets A = {z | re z < 1} and B = {z | 0 < re z}. In ℂ, the set A is the convex half-plane re z < 1 punctured at 0, and B is the convex half-plane 0 < re z punctured at 1. The fundamental group of a punctured convex domain is infinite cyclic, generated by a small circle about the puncture (StarConvex.fundamentalGroupMulEquivInt_sphereLoop). This file records the two instances, with their generators named:

• π₁(A, 1/2) ≃* ℤ, sending the class periph0Left of the peripheral loop γ0 in A to 1;
• π₁(B, 1/2) ≃* ℤ, sending the class periph1Right of the peripheral loop γ1 in B to 1.

The classes periph0Left and periph1Right are distinct from the peripheral elements periph0 and periph1 of π₁(ℂ ∖ {0, 1}, 1/2): they live in the fundamental groups of the two open sets, and the inclusions of A and B carry them to periph0 and periph1. The two isomorphisms, with their values on these generators, are the factors that the Seifert–van Kampen theorem for the cover {A, B} assembles into the fundamental group of ℂ ∖ {0, 1}.

The computation for A is the punctured star-convex computation with centre 0 and radius 1/2; the one for B is transported from it along the involution z ↦ 1 − z, which carries A onto B, fixes the basepoint and carries γ0 to γ1 pointwise, so both generators go to +1.

Main declarations

• TauCeti.ThricePuncturedSphere.periph0Left, TauCeti.ThricePuncturedSphere.periph1Right: the classes of γ0 in A and of γ1 in B, with map_val_periph0Left and map_val_periph1Right identifying their images in ℂ ∖ {0, 1}.
• TauCeti.ThricePuncturedSphere.leftOpenFundamentalGroupMulEquivInt, TauCeti.ThricePuncturedSphere.rightOpenFundamentalGroupMulEquivInt: π₁(A, 1/2) ≃* ℤ and π₁(B, 1/2) ≃* ℤ, with the value lemmas leftOpenFundamentalGroupMulEquivInt_periph0Left and rightOpenFundamentalGroupMulEquivInt_periph1Right.
• zpowers_periph0Left, zpowers_periph1Right: each class generates its fundamental group.
• isPathConnected_leftOpen, isPathConnected_rightOpen: A and B are path connected, being homotopy equivalent to a circle.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.7 (π₁(S¹) ≅ ℤ) and Proposition 1.18 (homotopy equivalences induce isomorphisms on π₁).

The peripheral classes in A and in B

noncomputable def TauCeti.ThricePuncturedSphere.periph0Left : FundamentalGroup ↑leftOpen ⟨basePt, basePt_mem_leftOpen⟩

The class of the peripheral loop γ0 in the fundamental group of A = {re z < 1}. The inclusion of A carries it to periph0 (map_val_periph0Left).

Equations

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

noncomputable def TauCeti.ThricePuncturedSphere.periph1Right : FundamentalGroup ↑rightOpen ⟨basePt, basePt_mem_rightOpen⟩

The class of the peripheral loop γ1 in the fundamental group of B = {0 < re z}. The inclusion of B carries it to periph1 (map_val_periph1Right).

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.map_val_periph0Left : (FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨basePt, basePt_mem_leftOpen⟩) periph0Left = periph0

The inclusion A ↪ ℂ ∖ {0, 1} carries the class of γ0 in A to the peripheral element periph0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.map_val_periph1Right : (FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨basePt, basePt_mem_rightOpen⟩) periph1Right = periph1

The inclusion B ↪ ℂ ∖ {0, 1} carries the class of γ1 in B to the peripheral element periph1.

π₁(A, 1/2)

noncomputable def TauCeti.ThricePuncturedSphere.leftOpenFundamentalGroupMulEquivInt : FundamentalGroup ↑leftOpen ⟨basePt, basePt_mem_leftOpen⟩ ≃* Multiplicative ℤ

The fundamental group of A = {re z < 1} is infinite cyclic: π₁(A, 1/2) ≃* ℤ. It is the punctured star-convex computation for the half-plane re z < 1 punctured at 0, and it sends the class of γ0 to 1 (leftOpenFundamentalGroupMulEquivInt_periph0Left).

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.leftOpenFundamentalGroupMulEquivInt_periph0Left : leftOpenFundamentalGroupMulEquivInt periph0Left = Multiplicative.ofAdd 1

The isomorphism π₁(A, 1/2) ≃* ℤ sends the class of the counterclockwise loop γ0 to 1.

π₁(B, 1/2)

noncomputable def TauCeti.ThricePuncturedSphere.rightOpenFundamentalGroupMulEquivInt : FundamentalGroup ↑rightOpen ⟨basePt, basePt_mem_rightOpen⟩ ≃* Multiplicative ℤ

The fundamental group of B = {0 < re z} is infinite cyclic: π₁(B, 1/2) ≃* ℤ. It is transported from leftOpenFundamentalGroupMulEquivInt along the involution z ↦ 1 − z, which carries A onto B and fixes the basepoint, and it sends the class of γ1 to 1 (rightOpenFundamentalGroupMulEquivInt_periph1Right).

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.rightOpenFundamentalGroupMulEquivInt_periph1Right : rightOpenFundamentalGroupMulEquivInt periph1Right = Multiplicative.ofAdd 1

The isomorphism π₁(B, 1/2) ≃* ℤ sends the class of the counterclockwise loop γ1 to 1.

Path-connectedness

theorem TauCeti.ThricePuncturedSphere.isPathConnected_leftOpen : IsPathConnected leftOpen

A = {re z < 1} is path connected: it is homotopy equivalent to the circle |z| = 1/2.

theorem TauCeti.ThricePuncturedSphere.isPathConnected_rightOpen : IsPathConnected rightOpen

B = {0 < re z} is path connected, being homeomorphic to A by z ↦ 1 − z.

Generation

@[simp]

theorem TauCeti.ThricePuncturedSphere.zpowers_periph0Left : Subgroup.zpowers periph0Left = ⊤

The class of γ0 generates π₁(A, 1/2).

@[simp]

theorem TauCeti.ThricePuncturedSphere.zpowers_periph1Right : Subgroup.zpowers periph1Right = ⊤

The class of γ1 generates π₁(B, 1/2).