Documentation

TauCeti.Topology.Homotopy.StarConvexComplement

The complement of a bounded star-convex set retracts onto a sphere #

Let K be a subset of a real normed space which contains a point p, is star-convex about p, and lies in the open ball ball p r. Then the complement Kᶜ deformation retracts onto the sphere sphere p r. 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) where c lies between 1 and r / ‖z - p‖. If c ≥ 1, the point z lies on the segment from p to p + c • (z - p), so star-convexity keeps the latter out of K; if c ≤ 1, then c ≥ r / ‖z - p‖ puts it outside ball p r.

In particular the complements of K and of {p} have the same homotopy type: this is the input for comparing the relative homology groups H(X, X ∖ K) and H(X, X ∖ {p}) in the local homology of manifolds.

Main declarations #

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.

The construction follows the companion construction for punctured star-convex sets in TauCeti.Topology.Homotopy.PuncturedStarConvex, whose StarConvex.sphereHomotopyEquiv retracts V ∖ {p} onto a sphere inside V; here the sphere lies outside K instead, and the radial projection is the restriction of TauCeti.radialProjectionToSphere.

source
theorem StarConvex.add_smul_sub_mem_compl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hKr : K ⊆ Metric.ball p r) {z : E} (hz : z ∉ K) {c : ℝ} (hc : 1 ≤ c ∨ r / ‖z - p‖ ≤ c ∧ z ≠ p) :
p + c • (z - p) ∉ K

A point p + c • (z - p) with z ∉ K stays outside K when c ≥ 1, by star-convexity of K about p, or when c ≥ r / ‖z - p‖, since it then lies outside ball p r ⊇ K provided z ≠ p.

source
noncomputable def StarConvex.complRadialHomotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) :
((ContinuousMap.inclusion ⋯).comp (TauCeti.complRadialProjection hp ⋯)).Homotopy (ContinuousMap.id ↑Kᶜ)

The straight-line homotopy from the radial projection onto sphere p r to the identity of Kᶜ, for K star-convex about p ∈ K and contained in ball p r.

Instances For
    source
    @[simp]
    theorem StarConvex.coe_complRadialHomotopy_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) (t : ↑unitInterval) (z : ↑Kᶜ) :
    ↑((hK.complRadialHomotopy hp hKr) (t, z)) = p + ((1 - ↑t) * (r / ‖↑z - p‖) + ↑t) • (↑z - p)

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

    source
    @[simp]
    theorem StarConvex.complRadialHomotopy_apply_inclusion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) (t : ↑unitInterval) (x : ↑(Metric.sphere p r)) :
    (hK.complRadialHomotopy hp hKr) (t, Set.inclusion ⋯ x) = Set.inclusion ⋯ x

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

    source
    noncomputable def StarConvex.complSphereHomotopyEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) :
    ContinuousMap.HomotopyEquiv ↑(Metric.sphere p r) ↑Kᶜ

    The complement of a bounded star-convex set is homotopy equivalent to a sphere. If K contains p, is star-convex about p and lies in ball p r, then the inclusion sphere p r → Kᶜ is a homotopy equivalence; its homotopy inverse is the radial projection z ↦ p + (r / ‖z - p‖) • (z - p).

    Instances For
      source
      @[simp]
      theorem StarConvex.coe_complSphereHomotopyEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) (x : ↑(Metric.sphere p r)) :
      ↑((hK.complSphereHomotopyEquiv hp hKr).toFun x) = ↑x

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

      source
      @[simp]
      theorem StarConvex.coe_complSphereHomotopyEquiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {p : E} {r : ℝ} (hK : StarConvex ℝ p K) (hp : p ∈ K) (hKr : K ⊆ Metric.ball p r) (z : ↑Kᶜ) :
      ↑((hK.complSphereHomotopyEquiv hp hKr).symm.toFun z) = p + (r / ‖↑z - p‖) • (↑z - p)

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