sphereHomeoOfLinearIsometryEquiv
plain-language theorem explainer
A real-linear isometric equivalence of normed spaces restricts to a topological homeomorphism of the unit spheres. Algebraic topologists and anyone building stereographic or two-chart covers of spheres cite it as the transport step that moves sphere geometry along an ambient isometry. The construction is a one-line subtype restriction of the underlying homeomorphism, using norm preservation.
Claim. Let $F$ and $G$ be real normed spaces and let $e : F \simeq_{\ell i} G$ be a linear isometry equivalence. Then $e$ restricts to a homeomorphism $S_F(0,1) \simeq_t S_G(0,1)$ between the unit spheres centered at the origin.
background
The ambient setting is the singular-sphere geometry module, which builds two-chart open covers of unit spheres in finite-dimensional real normed spaces and tracks homotopy types of punctured spheres and their intersections. Unit spheres are the usual sets ${x : |x| = 1}$ with the subspace topology.
A linear isometry equivalence is a linear equivalence that preserves the norm in both directions. It therefore maps the unit sphere of $F$ bijectively onto the unit sphere of $G$, and the underlying continuous inverse pair restricts to a homeomorphism of those subspaces. Mathlib already supplies the ambient homeomorphism (toHomeomorph) and the sphere membership criterion via the norm.
Downstream, this transport is applied to a hyperbolic-plane style isometry (hypIsometry) when identifying the intersection of the two punctured covers with a lower-dimensional sphere, and again in the two-point complement homotopy equivalence chain.
proof idea
One-line construction: take the homeomorphism underlying the linear isometry equivalence and restrict it to the subtype of unit-sphere points. Membership is rewritten with mem_sphere_zero_iff_norm on both sides; e.norm_map gives $|e x| = |x|$, so $|x| = 1$ if and only if $|e x| = 1$. The resulting subtype map is the desired homeomorphism of unit spheres.
why it matters
This is pure transport infrastructure inside the sphere-cover calculus of SingularSphereGeometry. It is consumed by interHomotopyEquiv (Step 2: the intersection of the two punctured covers of $S^{n+1}$ is homotopy equivalent to $S^n$), where it appears after polar coordinates as sphereHomeoOfLinearIsometryEquiv (hypIsometry n) paired with a product congruence. The same pattern feeds twoPointComplHEquiv in LinkingVanishingHighDim, which identifies $S^{n+1} \setminus {p,q}$ with $S^n$ by stereographic projection, translation, and ray collapse.
In the Recognition framework these sphere homotopy equivalences support high-dimensional linking-vanishing arguments that underwrite dimensional forcing (the T8 step $D = 3$ and the eight-tick octave geometry). The declaration itself is not a physics claim; it is the clean Mathlib-facing bridge that lets ambient linear isometries move sphere charts without rewriting every cover by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.