The closed unit ball with its boundary collapsed

In a real seminormed space E, the open unit ball is homeomorphic to E itself (OpenPartialHomeomorph.univUnitBall). This file sends the open unit ball onto E ⊆ OnePoint E along that homeomorphism and every other point, in particular the boundary sphere of the closed unit ball, to ∞, as a partial equivalence TauCeti.unitBallToOnePoint : PartialEquiv E (OnePoint E):

• on the open ball it is univUnitBall.symm followed by the inclusion E → OnePoint E, a bijection onto the complement of ∞;
• every point of norm at least one, in particular the whole boundary sphere, goes to ∞;
• it is continuous on all of E (TauCeti.continuous_unitBallToOnePoint), in particular on the closed unit ball, and its inverse is continuous on the complement of ∞ (TauCeti.continuousOn_unitBallToOnePoint_symm).

Composed with a homeomorphism from OnePoint E to a sphere, this is a characteristic map of the top cell of a sphere, in the shape Mathlib's classical CW complexes require.

References

• A. Hatcher, Algebraic Topology, Chapter 0, Example 0.3.

noncomputable def TauCeti.unitBallToOnePoint {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : PartialEquiv E (OnePoint E)

The closed unit ball of a real seminormed space E with its boundary collapsed to ∞, as a partial equivalence E → OnePoint E with source the open unit ball and target the complement of ∞. A point x of norm less than one goes to univUnitBall.symm x, and every other point goes to ∞.

@[simp]

theorem TauCeti.unitBallToOnePoint_source {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : unitBallToOnePoint.source = Metric.ball 0 1

@[simp]

theorem TauCeti.unitBallToOnePoint_target {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : unitBallToOnePoint.target = {OnePoint.infty}ᶜ

@[simp]

theorem TauCeti.unitBallToOnePoint_apply_of_norm_lt {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} (hx : ‖x‖ < 1) : ↑unitBallToOnePoint x = ↑(↑OpenPartialHomeomorph.univUnitBall.symm x)

@[simp]

theorem TauCeti.unitBallToOnePoint_apply_of_one_le_norm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} (hx : 1 ≤ ‖x‖) : ↑unitBallToOnePoint x = OnePoint.infty

@[simp]

theorem TauCeti.unitBallToOnePoint_apply_eq_infty_iff {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} : ↑unitBallToOnePoint x = OnePoint.infty ↔ 1 ≤ ‖x‖

@[simp]

theorem TauCeti.unitBallToOnePoint_symm_apply_coe {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (y : E) : ↑unitBallToOnePoint.symm ↑y = ↑OpenPartialHomeomorph.univUnitBall y

@[simp]

theorem TauCeti.unitBallToOnePoint_symm_apply_infty {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑unitBallToOnePoint.symm OnePoint.infty = 0

theorem TauCeti.mapsTo_unitBallToOnePoint_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : Set.MapsTo (↑unitBallToOnePoint) (Metric.sphere 0 1) {OnePoint.infty}

The boundary sphere of the unit ball is collapsed to ∞.

theorem TauCeti.image_unitBallToOnePoint_ball {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑unitBallToOnePoint '' Metric.ball 0 1 = {OnePoint.infty}ᶜ

The image of the open unit ball is the complement of ∞.

theorem TauCeti.image_unitBallToOnePoint_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] : ↑unitBallToOnePoint '' Metric.closedBall 0 1 = Set.univ

The image of the closed unit ball is all of OnePoint E when E has a point of nonzero norm: the open ball covers the complement of ∞ and the boundary sphere goes to ∞.

theorem TauCeti.continuous_unitBallToOnePoint {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : Continuous ↑unitBallToOnePoint

The collapse is continuous: approaching the boundary sphere from inside, univUnitBall.symm leaves every compact set, and outside the open ball the collapse is constantly ∞.

theorem TauCeti.continuousOn_unitBallToOnePoint_symm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ContinuousOn (↑unitBallToOnePoint.symm) unitBallToOnePoint.target

The inverse of the collapse is continuous away from ∞.