Isometric unit spheres force equal finite dimensions

MathlibAnnex.Sphere.finrank_eq

theorem

Compares Hausdorff dimensions in both directions using the surjective Lipschitz radial maps.

Statement

Let be finite-dimensional real normed spaces and let be a bijective isometry for the chord metrics inherited from their ambient norms. Here and are the unit spheres. Then

Assumptions

Both and are finite-dimensional in this exact theorem. Each carries a real normed-space structure and is a sphere isometry equivalence. If only one space is known to be finite-dimensional, the separate transfer theorem first supplies the other hypothesis. No positive-dimension assumption is needed.

Conclusion

The natural-number dimensions of the two real vector spaces agree. The intermediate invariant is the Hausdorff dimension of the entire ambient metric space, which is an extended nonnegative real number; its identification with linear dimension is a separate finite-dimensional theorem.

The proof compares the forward and inverse radial maps. It neither uses an unproved invariance of topological dimension nor identifies either radial map with a linear map.

Proof route

Write for the Hausdorff dimension of the whole metric space . The map is -Lipschitz, and the inverse identities show it is surjective. The Lipschitz range theorem therefore gives

For the inverse sphere isometry, is likewise surjective and -Lipschitz, giving

Thus the Hausdorff dimensions are equal. For each finite-dimensional real normed space the Hausdorff dimension of the whole space equals its real-linear dimension, viewed in . Applying that theorem to both spaces and using injectivity of the natural-number cast gives the asserted equality of linear dimensions.

theorem finrank_eq
    [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]
    (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :
    Module.finrank ℝ X = Module.finrank ℝ 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