circleHomeoCarrier
plain-language theorem explainer
Mathlib's complex unit circle is homeomorphic to the exact metric unit circle in EuclideanSpace R^2 that underlies TopCat.sphere 1. The map is the restriction of the orthonormal-basis linear isometry C ≃ R^2. Anyone building covering maps or winding numbers on the imported sphere carrier cites this bridge. The construction is a subtype homeomorphism whose membership equivalence is a one-line norm-preservation simp.
Claim. There is a homeomorphism $S^1_{\mathbb{C}} \simeq_{t} \{ x \in \mathbb{R}^2 : \|x\|=1 \}$, induced by restricting the orthonormal-basis linear isometry $\mathbb{C} \simeq_{\ell i} \mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,2)$ to the respective unit spheres. Explicitly, $z$ lies on the complex unit circle if and only if its image under that isometry lies on the Euclidean unit circle.
background
The module builds a covering-space foundation for a by-hand derivation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Mathlib's singular homology stops at the totally disconnected case, so winding/degree invariants must lift singular simplices through a covering of the imported TopCat.sphere 1 carrier. No project-local stand-in for $S^1$ is used.
SphereOneAmbient is the Euclidean plane $\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$. SphereOneCarrier is its metric unit sphere, the exact carrier under the ULift in TopCat.sphere 1. Mathlib's Circle is the unit circle subtype of $\mathbb{C}$. The upstream isometry isoE is Complex.orthonormalBasisOneI.repr: the real-linear isometry $\mathbb{C}\simeq_{\ell i}\mathbb{R}^2$ sending $1,i$ to the standard orthonormal frame.
The local goal is to transport Mathlib's covering map Circle.exp : R → Circle onto that metric carrier, then (via ULift) onto TopCat.sphere 1, yielding the trigonometric covering $t\mapsto(\cos t,\sin t)$.
proof idea
One-line subtype homeomorphism. Apply Homeomorph.subtype to isoE.toHomeomorph : C ≃ₜ SphereOneAmbient, with the membership predicate that a complex $z$ lies in the unit sphere iff its image does. The biconditional is discharged by simp on Metric.mem_sphere, dist_zero_right, the coercion of a linear isometry equiv to a homeomorphism, and LinearIsometryEquiv.norm_map (isometries preserve norms, hence unit spheres).
why it matters
This homeomorphism is the first transport leg from Mathlib's complex circle onto the exact metric carrier of TopCat.sphere 1. Downstream, carrierCovering is defined as the composite of this homeomorphism with Circle.exp, and isCoveringMap_carrierCovering obtains the covering property by Circle.isCoveringMap_exp.homeomorph_comp. That covering is then identified with the trigonometric map used by CircleParam and the fundamental simplex (ulift_carrierCovering_eq_trig, isCoveringMap_trigCirclePoint).
CircleLifting uses injectivity of the homeomorphism to equate trigonometric coincidence with equality of complex exponentials. CircleWinding uses its surjectivity to prove every point of TopCat.sphere 1 is hit by some real angle. In the Recognition forcing chain this supplies the honest covering geometry behind the T7 circle/octave realization: the eight-tick cycle is realized on a genuine $S^1$ with a Mathlib covering, not a stub carrier. It closes no open ledger-bridge question; it is pure topological scaffolding for the $H_1$ winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.