isoE
plain-language theorem explainer
Real-linear isometric equivalence identifying ℂ with the Euclidean plane ℝ² that carries Mathlib's unit circle onto the metric sphere ambient of TopCat.sphere 1. Anyone transporting covering maps or winding data from Circle to the project sphere carrier cites it. The body is a one-line alias of Mathlib's orthonormal-basis representation for {1,i}.
Claim. There is a real-linear isometric equivalence $\mathbb{C}\simeq_{\mathbb{R}}\mathbb{R}^{2}$ (Euclidean space on $\mathrm{Fin}\,2$), given by the orthonormal basis $\{1,i\}$, sending Mathlib's complex unit circle onto the metric unit circle in that plane.
background
This module builds the 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.
SphereOneAmbient is the exact ambient Euclidean space for that sphere: $\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$. Mathlib already has the exponential covering $\mathbb{R}\to\mathrm{Circle}$. The transport chain needs a real-linear isometry $\mathbb{C}\to\mathbb{R}^2$ that preserves the unit sphere metric, plus a later ULift homeomorphism into the precise sphere carrier.
The present definition is that isometry: the standard identification of $\mathbb{C}$ with $\mathbb{R}^2$ via the orthonormal frame ${1,i}$.
proof idea
One-line definition. The body is exactly Mathlib's Complex.orthonormalBasisOneI.repr, the linear isometric equivalence $\mathbb{C}\simeq_{\mathbb{R}}\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$ induced by the orthonormal basis ${1,i}$. No local proof work; the name packages that Mathlib object as the ambient map used throughout the covering transport.
why it matters
First leg of the transport that turns Mathlib's Circle.isCoveringMap_exp into the headline isCoveringMap_trigCirclePoint (the map $t\mapsto(\cos t,\sin t)$ on the exact TopCat.sphere 1 carrier). Downstream, circleHomeoCarrier builds the induced homeomorphism $\mathrm{Circle}\simeq_t$ metric unit-circle carrier by restricting this isometry to the unit spheres; carrierCovering_val then shows the transported covering agrees pointwise with the ambient trigonometric vector $(\cos t,\sin t)$.
That covering is the lift path for the singular-simplex winding invariant needed for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ without project-local replacements for $S^1$. In the broader RS forcing chain it supports the geometric realization of the T7 eight-tick / circle defect as an honest covering of the imported sphere, with no axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.