The inverse sphere isometry gives the inverse radial map

MathlibAnnex.Sphere.radialExtension_leftInverse

theorem

Shows that extending the inverse sphere isometry radially undoes the forward radial extension.

Statement

Let be real normed spaces and a bijective isometry for the ambient chord metrics. Here and are the unit spheres. Write and for , and define in the same way. Then

Assumptions

The only geometric assumptions are that are real normed spaces and is a bijective isometry between their unit spheres. The inverse used here is the inverse of that same . Completeness, finite-dimensionality and a positive dimension are not required.

Conclusion

The map is a left inverse of . Applying this result to gives for all , recorded separately as the right-inverse theorem. The two radial maps therefore give a bijection of the ambient spaces.

Bundling these two maps as radialExtensionEquiv uses precisely these inverse identities. The later homeomorphism uses the same maps with continuity proofs. Neither bundling chooses a new map.

Proof route

For both maps give zero. For , set , and . Since , norm preservation gives , so and . Substitution into the inverse radial formula gives

The cancellation uses the inverse of the given sphere equivalence, and positive normalization makes the argument of that inverse exactly .

theorem radialExtension_leftInverse
    (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :
    LeftInverse (radialExtension e.symm) (radialExtension e)

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