Homeomorphisms onto the unit balls of normed spaces

A continuous linear equivalence L : E ≃L[ℝ] F of real normed spaces carries the closed unit ball of E onto a convex body of F, which is usually not the closed unit ball of F. Rescaling each ray through the origin by the ratio of the gauges of the two convex bodies, which is Mathlib's gaugeRescaleHomeomorph, corrects this: the result ContinuousLinearEquiv.unitBallHomeomorph L : E ≃ₜ F is a homeomorphism carrying the open unit ball, the closed unit ball and the unit sphere of E onto those of F.

The typical use compares the closed unit ball of the sup norm on Fin n → ℝ, which is the domain of the characteristic maps of a CW complex, with the Euclidean unit disk.

Mathlib's radial homeomorphism Homeomorph.unitBall : E ≃ₜ ball 0 1 of a real normed space onto its open unit ball, followed by the inclusion of the open unit ball in the closed unit ball, is an open embedding of E into the closed unit ball. It lets a chart valued in E be read as a chart valued in the closed unit ball.

Main declarations

• ContinuousLinearEquiv.unitBallHomeomorph: the rescaled homeomorphism.
• ContinuousLinearEquiv.image_unitBallHomeomorph_closedBall, ContinuousLinearEquiv.image_unitBallHomeomorph_ball and ContinuousLinearEquiv.image_unitBallHomeomorph_sphere: it matches the closed unit balls, the open unit balls and the unit spheres.
• TauCeti.isOpenEmbedding_inclusion_comp_unitBall: E embeds openly in its closed unit ball.
• Homeomorph.unitBall_symm_apply_coe: the inverse radial map in explicit coordinates.
• TauCeti.nonempty_homeomorph_cube_closedBall: the closed unit ball of a real normed space of finite dimension k is homeomorphic to the cube Iᵏ.
• TauCeti.sphereHomeomorphOfFinrankEq: the unit spheres of two finite-dimensional real normed spaces of the same dimension are homeomorphic.

theorem Homeomorph.unitBall_symm_apply_coe {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (y : ↑(Metric.ball 0 1)) : unitBall.symm y = (√(1 - ‖↑y‖ ^ 2))⁻¹ • ↑y

The inverse of unitBall in explicit radial coordinates.

noncomputable def ContinuousLinearEquiv.unitBallHomeomorph {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E ≃L[ℝ] F) : E ≃ₜ F

The homeomorphism E ≃ₜ F obtained from a continuous linear equivalence L : E ≃L[ℝ] F by rescaling each ray through the origin so that the image L '' closedBall 0 1 of the closed unit ball of E lands on the closed unit ball of F (gaugeRescaleHomeomorph).

Equations

• L.unitBallHomeomorph = L.toHomeomorph.trans (gaugeRescaleHomeomorph (⇑L '' Metric.closedBall 0 1) (Metric.closedBall 0 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

theorem ContinuousLinearEquiv.unitBallHomeomorph_apply {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E ≃L[ℝ] F) (x : E) : L.unitBallHomeomorph x = gaugeRescale (⇑L '' Metric.closedBall 0 1) (Metric.closedBall 0 1) (L x)

@[simp]

theorem ContinuousLinearEquiv.image_unitBallHomeomorph_closedBall {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E ≃L[ℝ] F) : ⇑L.unitBallHomeomorph '' Metric.closedBall 0 1 = Metric.closedBall 0 1

ContinuousLinearEquiv.unitBallHomeomorph L carries the closed unit ball onto the closed unit ball.

@[simp]

theorem ContinuousLinearEquiv.image_unitBallHomeomorph_ball {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E ≃L[ℝ] F) : ⇑L.unitBallHomeomorph '' Metric.ball 0 1 = Metric.ball 0 1

ContinuousLinearEquiv.unitBallHomeomorph L carries the open unit ball onto the open unit ball.

@[simp]

theorem ContinuousLinearEquiv.image_unitBallHomeomorph_sphere {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E ≃L[ℝ] F) : ⇑L.unitBallHomeomorph '' Metric.sphere 0 1 = Metric.sphere 0 1

ContinuousLinearEquiv.unitBallHomeomorph L carries the unit sphere onto the unit sphere.

theorem TauCeti.isOpenEmbedding_inclusion_comp_unitBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : Topology.IsOpenEmbedding (Set.inclusion ⋯ ∘ ⇑Homeomorph.unitBall)

The radial homeomorphism Homeomorph.unitBall of E onto its open unit ball, followed by the inclusion of the open unit ball in the closed unit ball, is an open embedding of E into the closed unit ball.

theorem TauCeti.nonempty_homeomorph_cube_closedBall (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] : Nonempty ((Fin (Module.finrank ℝ F) → ↑unitInterval) ≃ₜ ↑(Metric.closedBall 0 1))

The closed unit ball of a finite-dimensional real normed space is a cube. The closed unit ball of a real normed space of finite dimension k is homeomorphic to the cube Iᵏ.

noncomputable def TauCeti.sphereHomeomorphOfFinrankEq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hEF : Module.finrank ℝ E = Module.finrank ℝ F) : ↑(Metric.sphere 0 1) ≃ₜ ↑(Metric.sphere 0 1)

The unit spheres of two finite-dimensional real normed spaces of the same dimension are homeomorphic, through ContinuousLinearEquiv.unitBallHomeomorph applied to ContinuousLinearEquiv.ofFinrankEq.

Equations

• TauCeti.sphereHomeomorphOfFinrankEq hEF = ((ContinuousLinearEquiv.ofFinrankEq hEF).unitBallHomeomorph.image (Metric.sphere 0 1)).trans (Homeomorph.setCongr ⋯)

@[simp]

theorem TauCeti.coe_sphereHomeomorphOfFinrankEq_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hEF : Module.finrank ℝ E = Module.finrank ℝ F) (x : ↑(Metric.sphere 0 1)) : ↑((sphereHomeomorphOfFinrankEq hEF) x) = (ContinuousLinearEquiv.ofFinrankEq hEF).unitBallHomeomorph ↑x

TauCeti.sphereHomeomorphOfFinrankEq is the restriction of ContinuousLinearEquiv.unitBallHomeomorph to the unit sphere.