The fundamental group of a punctured star-convex set

Let V be star-convex about p in a real normed space, and let sphere p r ⊆ V with r > 0. Since the inclusion of the sphere into V \ {p} is a homotopy equivalence (StarConvex.sphereHomotopyEquiv), it induces an isomorphism of fundamental groups at every point of the sphere. The isomorphism is the map FundamentalGroup.map of the inclusion itself, so a loop on the sphere represents the same class in V \ {p} as on the sphere, and every loop of V \ {p} based on the sphere is homotopic to one on the sphere.

In ℂ the sphere is a circle, so the fundamental group of V \ {p} is infinite cyclic. This is the computation that identifies the fundamental group of a punctured convex domain in the plane, such as the half-plane {z | z.re < 1} punctured at 0, with that of a small circle about the puncture.

Main declarations

• StarConvex.sphereFundamentalGroupMulEquiv: the isomorphism π₁(sphere p r, x) ≃* π₁(V \ {p}, x) induced by the inclusion.
• StarConvex.fundamentalGroupMulEquivInt: for V ⊆ ℂ, π₁(V \ {p}, x) ≃* ℤ at a point x of the circle sphere p r.
• Complex.sphereLoop and StarConvex.fundamentalGroupMulEquivInt_sphereLoop: the loop going once counterclockwise around sphere p r from p + r is sent to the generator ofAdd 1, so its class generates π₁(V \ {p}, p + r).
• StarConvex.fundamentalGroup_map_directionFrom_bijective: the direction map Complex.directionFrom, z ↦ (z - p) / ‖z - p‖ to the unit circle, induces a bijection of fundamental groups at every point of V \ {p}, on the circle or off it. Composed with Circle.fundamentalGroupMulEquiv, it identifies π₁(V \ {p}, z) with ℤ by the degree of the direction of a loop.
• StarConvex.isCyclic_fundamentalGroup_diff_singleton: consequently π₁(V \ {p}, z) is cyclic at every point z.
• StarConvex.fundamentalGroup_map_directionFrom_comp_snd_bijective: for simply connected U, the direction of the second coordinate induces a bijection of fundamental groups at every point of U × (V \ {p}). For a punctured ball, composing with Circle.fundamentalGroupMulEquiv identifies the fundamental group with ℤ (TauCeti.fundamentalGroupMulEquiv_comp_map_directionFrom_comp_snd_bijective).
• TauCeti.zpowers_loopAround_eq_top: for simply connected U, the loop t ↦ (u, p + (z - p) e^{2πit}) around the puncture (Complex.loopAround) generates π₁(U × (ball p R \ {p}), (u, z)).

References

Hatcher, Algebraic Topology, Proposition 1.18 (homotopy equivalences induce isomorphisms on π₁) and Theorem 1.7 (π₁(S¹) ≅ ℤ).

noncomputable def StarConvex.sphereFundamentalGroupMulEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} {p : E} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (x : ↑(Metric.sphere p r)) : FundamentalGroup (↑(Metric.sphere p r)) x ≃* FundamentalGroup (↑(V \ {p})) ((hV.sphereHomotopyEquiv hr hS).toFun x)

The fundamental group of a punctured star-convex set is that of a sphere about the puncture. If V is star-convex about p and contains sphere p r with r > 0, the inclusion of the sphere into V \ {p} induces an isomorphism of fundamental groups at every point x of the sphere.

Equations

• hV.sphereFundamentalGroupMulEquiv hr hS x = MulEquiv.ofBijective (FundamentalGroup.map (hV.sphereHomotopyEquiv hr hS).toFun x) ⋯

@[simp]

theorem StarConvex.sphereFundamentalGroupMulEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} {p : E} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (x : ↑(Metric.sphere p r)) (γ : FundamentalGroup (↑(Metric.sphere p r)) x) : (hV.sphereFundamentalGroupMulEquiv hr hS x) γ = (FundamentalGroup.map (hV.sphereHomotopyEquiv hr hS).toFun x) γ

The isomorphism StarConvex.sphereFundamentalGroupMulEquiv is the map induced on fundamental groups by the inclusion of the sphere.

noncomputable def StarConvex.fundamentalGroupMulEquivInt {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (x : ↑(Metric.sphere p r)) : FundamentalGroup (↑(V \ {p})) ((hV.sphereHomotopyEquiv hr hS).toFun x) ≃* Multiplicative ℤ

The fundamental group of a punctured star-convex subset of ℂ is infinite cyclic. If V is star-convex about p and contains the circle sphere p r with r > 0, then π₁(V \ {p}, x) ≃* ℤ at every point x of that circle. It is the inverse of the isomorphism induced by the inclusion of the circle, followed by the parametrization w ↦ (w - p) / r of the circle by Circle and the computation Circle.fundamentalGroupMulEquiv.

Equations

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

theorem StarConvex.fundamentalGroupMulEquivInt_def {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (x : ↑(Metric.sphere p r)) : hV.fundamentalGroupMulEquivInt hr hS x = (hV.sphereFundamentalGroupMulEquiv hr hS x).symm.trans ((TauCeti.FundamentalGroup.homeomorphMulEquiv (TauCeti.sphereCircleHomeomorph p hr) x).trans ((TauCeti.sphereCircleHomeomorph p hr) x).fundamentalGroupMulEquiv)

StarConvex.fundamentalGroupMulEquivInt factors through the circle sphere p r.

noncomputable def Complex.sphereLoop {r : ℝ} (p : ℂ) (hr : 0 < r) : Path ((TauCeti.sphereCircleHomeomorph p hr).symm 1) ((TauCeti.sphereCircleHomeomorph p hr).symm 1)

The loop t ↦ p + r·exp(2πit) going once counterclockwise around the circle sphere p r, based at p + r. It is the image of Circle.expLoop under the parametrization of the circle by Circle.

Equations

• p.sphereLoop hr = Circle.expLoop.map ⋯

@[simp]

theorem Complex.coe_sphereLoop_apply {r : ℝ} (p : ℂ) (hr : 0 < r) (t : ↑unitInterval) : ↑((p.sphereLoop hr) t) = circleMap p r (2 * Real.pi * ↑t)

theorem StarConvex.fundamentalGroupMulEquivInt_sphereLoop {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) : (hV.fundamentalGroupMulEquivInt hr hS ((TauCeti.sphereCircleHomeomorph p hr).symm 1)) ((FundamentalGroup.map (hV.sphereHomotopyEquiv hr hS).toFun ((TauCeti.sphereCircleHomeomorph p hr).symm 1)) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk (p.sphereLoop hr)))) = Multiplicative.ofAdd 1

The counterclockwise circle generates the fundamental group of a punctured star-convex set. Under StarConvex.fundamentalGroupMulEquivInt, the class in V \ {p} of the loop going once counterclockwise around sphere p r is ofAdd 1.

theorem StarConvex.not_simplyConnectedSpace_diff_singleton {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) : ¬SimplyConnectedSpace ↑(V \ {p})

A punctured star-convex subset of ℂ containing a circle about the puncture is not simply connected.

theorem StarConvex.fundamentalGroup_map_directionFrom_bijective {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (z : ↑(V \ {p})) : Function.Bijective ⇑(FundamentalGroup.map (p.directionFrom V) z)

The direction map of a punctured star-convex set is bijective on fundamental groups. If V is star-convex about p and contains a circle about p, then z ↦ (z - p) / ‖z - p‖ induces a bijection π₁(V \ {p}, z) → π₁(Circle, (z - p) / ‖z - p‖) at every point z, not only on the circle. It is the forward map of the homotopy equivalence StarConvex.sphereHomotopyEquiv, inverted and followed by the parametrization of the circle by Circle.

theorem StarConvex.isCyclic_fundamentalGroup_diff_singleton {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (z : ↑(V \ {p})) : IsCyclic (FundamentalGroup (↑(V \ {p})) z)

The fundamental group of a punctured star-convex subset of ℂ is cyclic at every point, on the circle about the puncture or off it, since the direction map embeds it in π₁(Circle).

theorem StarConvex.fundamentalGroup_map_directionFrom_comp_snd_bijective {U : Type u_1} [TopologicalSpace U] [SimplyConnectedSpace U] {V : Set ℂ} {p : ℂ} {r : ℝ} (hV : StarConvex ℝ p V) (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (a : U × ↑(V \ {p})) : Function.Bijective ⇑(FundamentalGroup.map ((p.directionFrom V).comp ContinuousMap.snd) a)

Loops in a simply connected space times a punctured star-convex set are detected by the direction of their second coordinate. If U is simply connected and V is star-convex about p and contains a circle about p, then (u, z) ↦ (z - p) / ‖z - p‖ induces a bijection of fundamental groups at every point of U × (V \ {p}).

theorem TauCeti.fundamentalGroupMulEquiv_comp_map_directionFrom_comp_snd_bijective {U : Type u_1} [TopologicalSpace U] [SimplyConnectedSpace U] {p : ℂ} {R : ℝ} (a : U × ↑(Metric.ball p R \ {p})) : Function.Bijective ⇑((((p.directionFrom (Metric.ball p R)).comp ContinuousMap.snd) a).fundamentalGroupMulEquiv.toMonoidHom.comp (FundamentalGroup.map ((p.directionFrom (Metric.ball p R)).comp ContinuousMap.snd) a))

The degree of the direction identifies π₁(U × (ball p R \ {p})) with ℤ. For simply connected U, the direction of the second coordinate followed by Circle.fundamentalGroupMulEquiv is a bijective homomorphism from π₁(U × (ball p R \ {p}), a) to Multiplicative ℤ, at every base point a.

@[simp]

theorem TauCeti.zpowers_loopAround_eq_top {U : Type u_1} [TopologicalSpace U] [SimplyConnectedSpace U] {p : ℂ} {R : ℝ} (u : U) (z : ↑(Metric.ball p R \ {p})) : Subgroup.zpowers (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk ((Path.refl u).prod (p.loopAround z)))) = ⊤

The fundamental group of a simply connected space times a punctured disc is generated by the loop around the puncture. For simply connected U, the class of t ↦ (u, p + (z - p) e^{2πit}) generates π₁(U × (ball p R \ {p}), (u, z)). Its direction has degree one, and the degree of the direction identifies the group with ℤ (TauCeti.fundamentalGroupMulEquiv_comp_map_directionFrom_comp_snd_bijective).