The fundamental group of the thrice-punctured sphere

The thrice-punctured sphere ℂ ∖ {0, 1} is the union of the open sets A = {re z < 1} and B = {0 < re z}. Both are path connected, and so is their intersection, the open strip 0 < re z < 1, which contains the basepoint 1/2. By the generation half of the Seifert--van Kampen theorem (TauCeti.FundamentalGroup.range_map_subtypeVal_sup_eq_top), π₁(ℂ ∖ {0, 1}, 1/2) is generated by the images of π₁(A, 1/2) and π₁(B, 1/2). These are infinite cyclic, generated by the classes of the peripheral loops γ0 and γ1, whose images are periph0 and periph1. Hence periph0 and periph1 generate π₁(ℂ ∖ {0, 1}, 1/2).

In particular a homomorphism out of π₁(ℂ ∖ {0, 1}, 1/2) is determined by its values on periph0 and periph1. For the monodromy representation of a cover this says that the monodromy group, the image of π₁, is generated by the monodromy permutations around 0 and around 1, which is how a cover's permutation triple sees the transitivity of its monodromy.

The full Seifert--van Kampen theorem for the same cover (TauCeti.vanKampenEquiv, which applies because the strip A ∩ B is simply connected) identifies π₁(ℂ ∖ {0, 1}, 1/2) with the free product π₁(A, 1/2) ∗ π₁(B, 1/2) ≃* ℤ ∗ ℤ, so π₁(ℂ ∖ {0, 1}, 1/2) is the free group on the two generators periph0 and periph1. The element periphInf = (periph1 * periph0)⁻¹ is then the image of (of 1 * of 0)⁻¹, and any two elements of a group are the images of periph0 and periph1 under a unique homomorphism. This free universal property is how a permutation triple is turned into an action of the fundamental group.

Main declarations

• TauCeti.ThricePuncturedSphere.closure_periph0_periph1: periph0 and periph1 generate π₁(ℂ ∖ {0, 1}, 1/2).
• TauCeti.ThricePuncturedSphere.fundamentalGroup_hom_ext: a homomorphism out of π₁(ℂ ∖ {0, 1}, 1/2) is determined by its values on periph0 and periph1.
• TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup: π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2), sending periph0 to of 0 and periph1 to of 1.
• TauCeti.ThricePuncturedSphere.peripheralBasis: (periph0, periph1) as a free basis of π₁(ℂ ∖ {0, 1}, 1/2), whose FreeGroupBasis.lift realizes any pair of values.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.20.

@[simp]

theorem TauCeti.ThricePuncturedSphere.closure_periph0_periph1 : Subgroup.closure {periph0, periph1} = ⊤

The peripheral elements periph0 and periph1 generate π₁(ℂ ∖ {0, 1}, 1/2).

theorem TauCeti.ThricePuncturedSphere.fundamentalGroup_hom_ext {G : Type u_1} [Monoid G] {f g : FundamentalGroup ThricePuncturedSphere basePt →* G} (h0 : f periph0 = g periph0) (h1 : f periph1 = g periph1) : f = g

A homomorphism out of π₁(ℂ ∖ {0, 1}, 1/2) is determined by its values on the peripheral elements periph0 and periph1.

theorem TauCeti.ThricePuncturedSphere.fundamentalGroup_hom_ext_iff {G : Type u_1} [Monoid G] {f g : FundamentalGroup ThricePuncturedSphere basePt →* G} : f = g ↔ f periph0 = g periph0 ∧ f periph1 = g periph1

@[simp]

theorem TauCeti.ThricePuncturedSphere.closure_periph0_periph1_periphInf : Subgroup.closure {periph0, periph1, periphInf} = ⊤

The three peripheral elements periph0, periph1 and periphInf generate π₁(ℂ ∖ {0, 1}, 1/2). They do not generate it freely: they satisfy periphInf * periph1 * periph0 = 1.

The free group on the peripheral elements

noncomputable def TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup : FundamentalGroup ThricePuncturedSphere basePt ≃* FreeGroup (Fin 2)

The fundamental group of the thrice-punctured sphere is free of rank two: π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2), sending the peripheral elements periph0 and periph1 to the generators of 0 and of 1.

Equations

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

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_periph0 : fundamentalGroupMulEquivFreeGroup periph0 = FreeGroup.of 0

The isomorphism π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2) sends periph0 to of 0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_periph1 : fundamentalGroupMulEquivFreeGroup periph1 = FreeGroup.of 1

The isomorphism π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2) sends periph1 to of 1.

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_periphInf : fundamentalGroupMulEquivFreeGroup periphInf = (FreeGroup.of 1 * FreeGroup.of 0)⁻¹

The isomorphism π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2) sends the peripheral element at infinity periphInf to (of 1 * of 0)⁻¹.

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_symm_toMonoidHom : ↑fundamentalGroupMulEquivFreeGroup.symm = FreeGroup.lift ![periph0, periph1]

The inverse of π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2) is the homomorphism out of the free group sending of 0 to periph0 and of 1 to periph1.

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_symm_apply (w : FreeGroup (Fin 2)) : fundamentalGroupMulEquivFreeGroup.symm w = (FreeGroup.lift ![periph0, periph1]) w

The inverse of π₁(ℂ ∖ {0, 1}, 1/2) ≃* FreeGroup (Fin 2) evaluates a word in of 0 and of 1 at periph0 and periph1.

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_symm_of_zero : fundamentalGroupMulEquivFreeGroup.symm (FreeGroup.of 0) = periph0

The generator of 0 of FreeGroup (Fin 2) corresponds to periph0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_symm_of_one : fundamentalGroupMulEquivFreeGroup.symm (FreeGroup.of 1) = periph1

The generator of 1 of FreeGroup (Fin 2) corresponds to periph1.

noncomputable def TauCeti.ThricePuncturedSphere.peripheralBasis : FreeGroupBasis (Fin 2) (FundamentalGroup ThricePuncturedSphere basePt)

The peripheral elements periph0 and periph1, as a free basis of π₁(ℂ ∖ {0, 1}, 1/2). Its FreeGroupBasis.lift sends a pair of elements of any group to the unique homomorphism taking periph0 and periph1 to them.

Equations

• TauCeti.ThricePuncturedSphere.peripheralBasis = { repr := TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup }

@[simp]

theorem TauCeti.ThricePuncturedSphere.peripheralBasis_repr : peripheralBasis.repr = fundamentalGroupMulEquivFreeGroup

The isomorphism with FreeGroup (Fin 2) given by peripheralBasis is fundamentalGroupMulEquivFreeGroup.

@[simp]

theorem TauCeti.ThricePuncturedSphere.fundamentalGroupMulEquivFreeGroup_peripheralBasis (i : Fin 2) : fundamentalGroupMulEquivFreeGroup (peripheralBasis i) = FreeGroup.of i

The isomorphism fundamentalGroupMulEquivFreeGroup sends each element of peripheralBasis to the corresponding free-group generator.

@[simp]

theorem TauCeti.ThricePuncturedSphere.peripheralBasis_zero : peripheralBasis 0 = periph0

The first element of peripheralBasis is periph0.

@[simp]

theorem TauCeti.ThricePuncturedSphere.peripheralBasis_one : peripheralBasis 1 = periph1

The second element of peripheralBasis is periph1.

instance TauCeti.ThricePuncturedSphere.instIsFreeGroupFundamentalGroupBasePt : IsFreeGroup (FundamentalGroup ThricePuncturedSphere basePt)

π₁(ℂ ∖ {0, 1}, 1/2) is a free group.