Pushing a convex body onto its frontier away from an interior point

Let s be a closed, von Neumann bounded convex set in a real topological vector space, let p be an interior point of s and let U be a neighbourhood of p. Moving every point y along the ray from p through y, scaled by the gauge of s centred at p, gives a homotopy of the identity, relative to the frontier of s, which keeps s inside itself and ends at a map sending every point outside U to the frontier of s (Convex.exists_homotopyRel_frontier). The points of s near p are spread over the whole of s at the end, so the homotopy is defined and continuous on the whole space.

This is the deformation which, read through the characteristic map of a cell of a CW complex, pushes a map missing a neighbourhood of a point of an open cell off the whole cell. It generalises TauCeti.radialPush, which pushes the closed unit ball away from its centre.

References

• A. Hatcher, Algebraic Topology, Section 4.1, proof of Theorem 4.8, the deformation retraction of Dᵏ ∖ {p} onto ∂Dᵏ.

theorem Convex.exists_homotopyRel_frontier {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {p : E} (hs : Convex ℝ s) (hsc : IsClosed s) (hsb : Bornology.IsVonNBounded ℝ s) (hp : p ∈ interior s) {U : Set E} (hU : U ∈ nhds p) : ∃ (g : C(E, E)) (H : (ContinuousMap.id E).HomotopyRel g (frontier s)), (∀ (t : ↑unitInterval), ∀ y ∈ s, H (t, y) ∈ s) ∧ ∀ y ∉ U, g y ∈ frontier s

Pushing a convex body onto its frontier away from an interior point. Let s be a closed von Neumann bounded convex set and p an interior point of s. For every neighbourhood U of p there is a homotopy H of the identity, relative to the frontier of s, which keeps s inside itself, and whose endpoint sends every point outside U to the frontier of s.