A punctured star-convex set retracts onto a sphere about the puncture

Let V be a subset of a real normed space which is star-convex about a point p, and let the sphere sphere p r of some radius r > 0 lie in V. Then V \ {p} deformation retracts onto that sphere. The retraction is the radial projection z ↦ p + (r / ‖z - p‖) • (z - p), and the homotopy is the straight line from it to the identity. Every point of such a segment has the form p + c • (z - p) with c > 0 lying between 1 and r / ‖z - p‖, so it lies either on the segment from p to z or on the segment from p to the radial projection of z; star-convexity keeps both segments in V, and c > 0 keeps them off p.

In particular the inclusion of the sphere into V \ {p} is a homotopy equivalence. For an open convex subset of ℂ this is the reduction of the fundamental group of a punctured convex domain to that of a circle.

For subsets of ℂ, the file also records the direction map z ↦ (z - p) / ‖z - p‖ to the unit circle, the resulting path connectedness of V \ {p}, and the loop going once around the puncture of a punctured ball.

Connectedness and openness alone do not suffice: a punctured annulus is connected and open but is not homotopy equivalent to a circle.

Main declarations

• StarConvex.sphereHomotopyEquiv: the inclusion sphere p r → V \ {p} as a homotopy equivalence, with the radial projection as homotopy inverse (StarConvex.coe_sphereHomotopyEquiv_apply, StarConvex.coe_sphereHomotopyEquiv_symm_apply).
• StarConvex.radialHomotopy: the straight-line deformation from the radial projection to the identity, fixing the included sphere pointwise throughout.
• Complex.directionFrom: the direction map z ↦ (z - p) / ‖z - p‖ from V \ {p} to the unit circle, for V ⊆ ℂ.
• StarConvex.pathConnectedSpace_diff_singleton: for V ⊆ ℂ, V \ {p} is path connected; in particular so is a punctured ball (TauCeti.pathConnectedSpace_ball_diff_singleton).
• Complex.loopAround: the loop t ↦ p + (z - p) e^{2πit} going once around the puncture of ball p R \ {p}.

References

The radial deformation retraction is the standard one; compare Hatcher, Algebraic Topology, Chapter 0, where ℝⁿ \ {0} is deformation retracted onto the unit sphere by the same formula.

def TauCeti.sphereInclusionDiffSingleton {E : Type u_1} [NormedAddCommGroup E] {V : Set E} {p : E} {r : ℝ} (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) : C(↑(Metric.sphere p r), ↑(V \ {p}))

The inclusion of sphere p r into V \ {p}.

Equations

• TauCeti.sphereInclusionDiffSingleton hr hS = ContinuousMap.inclusion ⋯

@[simp]

theorem TauCeti.coe_sphereInclusionDiffSingleton_apply {E : Type u_1} [NormedAddCommGroup E] {V : Set E} {p : E} {r : ℝ} (hr : 0 < r) (hS : Metric.sphere p r ⊆ V) (x : ↑(Metric.sphere p r)) : ↑((sphereInclusionDiffSingleton hr hS) x) = ↑x

The inclusion of the sphere into V \ {p} does not move points.

noncomputable def TauCeti.radialProjectionToSphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} {p : E} {r : ℝ} (hr : 0 < r) : C(↑(V \ {p}), ↑(Metric.sphere p r))

Radial projection of V \ {p} onto the sphere sphere p r.

Equations

• TauCeti.radialProjectionToSphere hr = { toFun := fun (z : ↑(V \ {p})) => ⟨p + (r / ‖↑z - p‖) • (↑z - p), ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.coe_radialProjectionToSphere_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} {p : E} {r : ℝ} (hr : 0 < r) (z : ↑(V \ {p})) : ↑((radialProjectionToSphere hr) z) = p + (r / ‖↑z - p‖) • (↑z - p)

The radial projection onto sphere p r is z ↦ p + (r / ‖z - p‖) • (z - p).

noncomputable def StarConvex.radialHomotopy {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) : ((TauCeti.sphereInclusionDiffSingleton hr hS).comp (TauCeti.radialProjectionToSphere hr)).Homotopy (ContinuousMap.id ↑(V \ {p}))

The straight-line homotopy from the radial projection to the identity of V \ {p}.

Equations

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

@[simp]

theorem StarConvex.coe_radialHomotopy_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) (t : ↑unitInterval) (z : ↑(V \ {p})) : ↑((hV.radialHomotopy hr hS) (t, z)) = p + ((1 - ↑t) * (r / ‖↑z - p‖) + ↑t) • (↑z - p)

The radial deformation has the stated pointwise straight-line formula.

@[simp]

theorem StarConvex.radialHomotopy_apply_sphereInclusion {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) (t : ↑unitInterval) (x : ↑(Metric.sphere p r)) : (hV.radialHomotopy hr hS) (t, (TauCeti.sphereInclusionDiffSingleton hr hS) x) = (TauCeti.sphereInclusionDiffSingleton hr hS) x

The radial deformation fixes every included point of the sphere throughout the homotopy.

noncomputable def StarConvex.sphereHomotopyEquiv {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) : ContinuousMap.HomotopyEquiv ↑(Metric.sphere p r) ↑(V \ {p})

A punctured star-convex set is homotopy equivalent to a sphere about the puncture. If V is star-convex about p and contains the sphere sphere p r with r > 0, then the inclusion sphere p r → V \ {p} is a homotopy equivalence; its homotopy inverse is the radial projection z ↦ p + (r / ‖z - p‖) • (z - p).

Equations

• hV.sphereHomotopyEquiv hr hS = { toFun := TauCeti.sphereInclusionDiffSingleton hr hS, invFun := TauCeti.radialProjectionToSphere hr, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem StarConvex.coe_sphereHomotopyEquiv_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)) : ↑((hV.sphereHomotopyEquiv hr hS).toFun x) = ↑x

The homotopy equivalence StarConvex.sphereHomotopyEquiv is the inclusion of the sphere.

@[simp]

theorem StarConvex.coe_sphereHomotopyEquiv_symm_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) (z : ↑(V \ {p})) : ↑((hV.sphereHomotopyEquiv hr hS).symm.toFun z) = p + (r / ‖↑z - p‖) • (↑z - p)

The homotopy inverse of StarConvex.sphereHomotopyEquiv is the radial projection onto the sphere.

noncomputable def Complex.directionFrom (p : ℂ) (V : Set ℂ) : C(↑(V \ {p}), Circle)

The direction (z - p) / ‖z - p‖ of a point z of V \ {p} seen from p, as a point of the unit circle: the normalization TauCeti.normalizeToSphere of z - p, read in Circle.

Equations

• p.directionFrom V = (↑(TauCeti.sphereCircleHomeomorph 0 Complex.directionFrom._proof_2✝)).comp (TauCeti.normalizeToSphere (fun (z : ↑(V \ {p})) => ↑z - p) ⋯ ⋯)

@[simp]

theorem Complex.coe_directionFrom_apply (p : ℂ) (V : Set ℂ) (z : ↑(V \ {p})) : ↑((p.directionFrom V) z) = (↑z - p) / ↑‖↑z - p‖

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

A punctured star-convex subset of ℂ containing a circle about the puncture is path connected, being homotopy equivalent to the circle.

theorem TauCeti.pathConnectedSpace_ball_diff_singleton {R : ℝ} (p : ℂ) (hR : 0 < R) : PathConnectedSpace ↑(Metric.ball p R \ {p})

A punctured open ball in ℂ of positive radius is path connected.

noncomputable def Complex.loopAround {R : ℝ} (p : ℂ) (z : ↑(Metric.ball p R \ {p})) : Path z z

The loop t ↦ p + (z - p) e^{2πit} based at z, going once counterclockwise around p along the circle through z, in the punctured ball ball p R \ {p}.

Equations

• p.loopAround z = { toFun := fun (t : ↑unitInterval) => ⟨p + (↑z - p) * Complex.exp (↑(2 * Real.pi * ↑t) * Complex.I), ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Complex.coe_loopAround_apply {R : ℝ} (p : ℂ) (z : ↑(Metric.ball p R \ {p})) (t : ↑unitInterval) : ↑((p.loopAround z) t) = p + (↑z - p) * exp (↑(2 * Real.pi * ↑t) * I)