carrierCovering_val
plain-language theorem explainer
Pointwise, the covering map obtained by transporting Circle.exp through the orthonormal-basis isometry equals the ambient vector (cos t, sin t). Anyone building the winding/degree invariant for H₁(S¹; ℤ) via this covering cites it to identify the two parametrizations. The proof is a short term-mode coordinate check: rewrite through Circle.coe_exp and the repr isometry, then match real and imaginary parts.
Claim. For every real $t$, the image of $t$ under the transported covering $\mathbb{R}\to S^1_{\mathrm{carrier}}$ (viewed in the ambient Euclidean space $\mathbb{R}^2$) equals the trigonometric vector $(\cos t,\sin t)$.
background
This module builds the covering-space foundation needed 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 any winding invariant must lift simplices through a covering of the exact TopCat.sphere 1 object.
SphereOneAmbient is the Euclidean space $\mathbb{R}^2$ underlying that sphere. The isometry isoE is Mathlib's orthonormal-basis representation $\mathbb{C}\simeq_{\ell_i}\mathbb{R}^2$. The covering carrierCovering is the composite of Mathlib's Circle.exp with the homeomorphism from the complex unit circle onto the metric carrier. Independently, trigCircleVector t is the concrete ambient point $(\cos t,\sin t)$ already used by CircleParam.
The claim equates these two routes into ambient space, so later lifts can switch freely between the complex exponential covering and the trigonometric parametrization.
proof idea
Unfold the definition so the goal is isoE(Circle.exp t)=trigCircleVector t. Rewrite Circle.exp t via Circle.coe_exp to Complex.exp(t·I), and identify isoE with Complex.orthonormalBasisOneI.repr. Extend over the two coordinates of $\mathbb{R}^2$; on each coordinate apply orthonormalBasisOneI_repr_apply and fin_cases. The real part reduces by Complex.exp_ofReal_mul_I_re to $\cos t$; the imaginary part by Complex.exp_ofReal_mul_I_im to $\sin t, matching the definition of trigCircleVector`.
why it matters
This is the identification step that lets the headline covering theorem talk about the same map already used by CircleParam and the fundamental simplex. Downstream, ulift_carrierCovering_eq_trig lifts the equality into the exact TopCat.sphere 1 object: the ULift-symmetrized carrier covering equals trigCirclePoint pointwise. That equality is what feeds isCoveringMap_trigCirclePoint, the module's main result that $t\mapsto(\cos t,\sin t)$ is an honest covering map of Mathlib's sphere.
In the broader Recognition chain the circle covering underwrites the by-hand $H_1$ computation tied to the T7 eight-tick octave (period $2^3$) and the circle defect realization. No project-local $S^1$ substitute is introduced: everything is transported along real Lean equivalences from Mathlib's Circle.isCoveringMap_exp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.