The challenge bridge: ℙ¹ ≃ₜ the unit 2-sphere (CC5) #
Unit: projective-line (docs/design/projective-line.md §3.4). Mathlib already contains the
topological homeomorphism from a one-point compactification of a finite-dimensional real vector
space to the unit sphere in a Euclidean space of one higher dimension
(onePointEquivSphereOfFinrankEq); specializing it to V := ℂ (as a 2-dimensional real vector
space) and ι := Fin 3 gives exactly the sphere model used by the challenge's
genus_eq_zero_iff_homeo.
homeoSphere has no closed-form pointwise description (mathlib's construction selects a
ContinuousLinearEquiv via Nonempty.some); no consumer needs one (see design §3.4).
ℙ¹ is homeomorphic to the unit 2-sphere in EuclideanSpace ℝ (Fin 3) — the sphere model
used verbatim by the challenge's genus_eq_zero_iff_homeo.