toSphMap
plain-language theorem explainer
Converts a continuous sphere map written in the TopCat/ULift presentation into the matching continuous map between bare Sph models. Anyone moving embeddings, complements, or H1 statements between the two sphere presentations cites this bridge. The body is the pointwise ULift.up/down conjugation of the original map, with continuity by composition of the standard lift maps.
Claim. Given $D \in \mathbb{N}$ and a continuous map $f : S^1 \to S^D$ in the universe-lifted TopCat sphere model, return the underlying continuous map $\mathrm{Sph}(1) \to \mathrm{Sph}(D)$ obtained by conjugating $f$ with the canonical ULift identifications on domain and codomain.
background
The module studies when an embedded circle in $S^D$ can have homologically nontrivial complement. In Recognition Science, spatial dimension is forced to three partly because nontrivial circle linking is a three-dimensional phenomenon (the T9 linking step; cf. the constant $D := 3$ in the alpha derivation).
Two sphere presentations sit side by side. TopCat.sphere is Mathlib's sphere object lifted by ULift to universe 0; Sph is the bare Euclidean sphere model used by the singular-sphere geometry and low-dimensional linking lemmas. Continuous maps, embeddings, and complements must be transported between these presentations before homology comparisons make sense.
The conversion is purely notational: ULift.up embeds a bare sphere point into the TopCat model, and ULift.down projects back. Continuity of the conjugated map follows from continuity of the lifts and of $f$.
proof idea
Definitional construction, not a proof argument. The underlying function sends $x \in \mathrm{Sph}(1)$ to the down-projection of $f$ applied to the up-lift of $x$. Continuity is packaged as continuous_uliftDown composed with f.continuous composed with continuous_uliftUp. No nontrivial lemmas beyond the standard ULift continuity facts are used.
why it matters
This bridge is the entry point of the high-dimensional vanishing pipeline. Downstream, isEmbedding_toSphMap lifts embeddings across the conversion; complDownHomeo identifies complements in the two models; and not_detects_of_arcAcyclic concludes that, granting ArcComplementsAcyclic D, no embedded circle in $S^D$ for $D \ge 1$, $D \neq 3$ detects nontrivial linking. That vanishing is the topological half of the T9 argument that spatial dimension must be three: only in $D = 3$ can circle linking be homologically nontrivial. Without the conversion, TopCat-formulated embeddings cannot enter the Sph-model homology machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.