Radial extension of an isometry between unit spheres

MathlibAnnex.Sphere.radialExtension

def

Extends a bijective sphere isometry to all vectors by retaining each radius and transporting its unit direction.

Statement

Let be real normed spaces, let and carry their ambient chord distances, and let be a bijective isometry. The radial extension sends zero to zero and sends a nonzero vector to its radius times the image of its unit direction.

Definition

For , put . Since ,

Thus , so the formula

is well-defined. Normalization fixes unit vectors and is unchanged by positive rescaling, as the cited normalization lemmas state.

Assumptions

Both spaces are real normed spaces and is an isometry equivalence of their unit spheres. Neither space is assumed finite-dimensional, complete or nonzero. In the zero space there is no nonzero vector requiring normalization.

Conclusion

This defines on all of . The separately cited norm theorem gives ; for this follows from , and zero is immediate. The sphere-agreement theorem gives for .

This is a radial, positively homogeneous extension. Its defining operation uses positive radii; the declaration does not provide a linear extension theorem. In the classification argument is the map used for analytic and topological comparisons; a linear isometry supplied at a later stage is a separate object.

def radialExtension
    (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) (x : X) : Y := by
  classical
  exact if hx : x = 0 then 0 else
    ‖x‖ • (e (normalizeToSphere x hx) : Y)

namespace MathlibAnnex
namespace Sphere

universe u v

variable {X : Type u} {Y : Type v}
  [NormedAddCommGroup X] [NormedSpace ℝ X]
  [NormedAddCommGroup Y] [NormedSpace ℝ Y]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project