MATHLIBANNEX / CANONICAL DECLARATION CARD

The unit-sphere chord metric determines the ambient normed space

MathlibAnnex.Sphere.nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_of_finiteDimensional

theorem

Classifies existence of ambient linear isometries from the unit-sphere chord metric.

Statement

Let be real normed vector spaces and assume Let and , with chord distances and . A sphere isometry equivalence is a bijection preserving these distances. A real linear isometry equivalence is a real linear bijection satisfying for every . Then

Assumptions

The real normed-space structures and the finite-dimensional disjunction are the inputs. Neither positive dimension, completeness nor initial finite-dimensionality of both spaces is an extra assumption.

Conclusion

The theorem equates existence statements. It does not assert that the recovered ambient map restricts to a specified . Zero-dimensional spaces and empty unit spheres are included.

Proof route

Transfer finite dimension in either direction, separate zero dimension, transport the positive-dimensional case to norm models, recover a linear isometry there, and compose back. Conversely restrict an ambient linear isometry.

Proof steps

  1. Transfer dimension in the applicable direction. Given , if is finite-dimensional, finite dimension transfer along a sphere isometry makes finite-dimensional. If is finite-dimensional, apply it to to make finite-dimensional. Then equality of dimensions gives . If , both spaces consist only of zero; the unique map is a real linear isometry equivalence. The sphere restriction is the empty bijection. the finite-dimensional construction including zero separates this case before using positive-dimensional coordinates. The dimension-transfer input is made explicit by the radial map

    Its inverse is . The radial estimates are and the analogous inverse inequality. Both maps are continuous, and these Lipschitz bounds in both directions give equality of Hausdorff dimensions. A finite-dimensional is locally compact; its radial homeomorphism makes locally compact, which forces finite-dimensionality for a real normed space. With both finite-dimensional, their Hausdorff dimensions equal their real dimensions. This use of the radial map proves dimension transfer; it does not identify the recovered linear with .

  2. Use one coordinate system on each space. For , choose continuous real linear equivalences and . Define

    The operator bounds for these equivalences and their inverses give positive comparisons with the reference sup norm. Transport the given sphere map by

    For ,

    These are the coordinate norm models and exact sphere transport. More explicitly, for or its model record has

    Both constants are positive. The inverse bound gives ; the direct bound gives ; continuity is the composition of with the norm. These specify the seminorm, two constants, positivity, lower and upper comparisons and continuity fields. The model carrier is the same vector space with norm ; the reference and model conversions are identity on values, zero and subtraction. On the sphere , so and give the two inverse subtype maps used in .

  3. Recover in the models and compose back. With standard Lebesgue measure on , put , , and

    where ranges over real linear maps and is the increasing-row maximal-minor vector. Define similarly. The sphere isometry gives equality of these bodies for every , by sphere-induced body invariance. Input these models and all body equalities to norm-preserving linear recovery, as in sphere-metric recovery in norm models, obtaining bijective real linear with . The same maps give

    The inverse is . This is coordinate model recovery and return. It proves existence, without claiming .

  4. Restrict an ambient linear isometry for the converse. Given , the equations and the corresponding inverse equation make its restriction a sphere bijection. For ,

    Thus the restriction is a sphere isometry equivalence, including the empty case, as in restriction of a linear isometry.

The conclusion is an equivalence of existence statements, not an extension assertion for the supplied . When both spaces are initially known to be finite-dimensional, the two-sided finite-dimensional version gives the same equivalence. The finite-dimensional-domain implication and finite-dimensional-codomain implication use the respective side of the present disjunction; the combined forward implication selects the applicable direction. These variants preserve the same existence conclusion and do not supply an agreement condition with .

Main citations

Lean source signature (exact)

/-- If one ambient space is finite-dimensional, the unit-sphere chord metric
is a complete invariant of real normed spaces up to linear isometry. -/
theorem nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_of_finiteDimensional
    {X : Type u} {Y : Type v}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y]
    (hfin : FiniteDimensional ℝ X ∨ FiniteDimensional ℝ Y) :
    Nonempty ((Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) ↔ Nonempty (X ≃ₗᵢ[ℝ] Y)
In the source Mathematical meaning
X; Y; [NormedAddCommGroup X] [NormedSpace ℝ X]; [NormedAddCommGroup Y] [NormedSpace ℝ Y] The two real normed spaces, their additive norms and real scalar actions.
hfin : FiniteDimensional ℝ X ∨ FiniteDimensional ℝ Y At least one space is finite-dimensional; ∨ means or. Both are not required initially.
Metric.sphere (0 : X) 1; Metric.sphere (0 : Y) 1 , subtypes with inherited chord distances. These spheres may be empty.
Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1 A bijection preserving and the corresponding target distance. ≃ᵢ is isometry equivalence.
In the source Mathematical meaning
X ≃ₗᵢ[ℝ] Y A real linear bijection preserving as .
Nonempty (…) ↔︎ Nonempty (…) The entire conclusion says existence of a sphere equivalence if and only if existence of an ambient linear isometry equivalence. No restriction-equals-input condition occurs.

hfin is a hypothesis, and ↔︎ is the final if-and-only-if. The two occurrences of Nonempty quantify independently over a sphere bijection and an ambient real linear isometry. There is no equation asserting that the latter restricts to the former.

Surrounding assumptions and aliases.

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

Exact content identity

Declaration: MathlibAnnex.Sphere.nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_of_finiteDimensional

Accepted content SHA-256: ab2edc84df9478a9f7988f6b95aa42ee5a995655cf46a24d6111a767b341ec1c

Accepted source guide SHA-256: ea58aee79f80e280d7b7720a69bb8b5f3bd83599e3197f1490f0288074bc581d

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑