ulift_carrierCovering_eq_trig
plain-language theorem explainer
Pointwise equality: the ULift-transported carrier covering ℝ → TopCat.sphere 1 coincides with the trigonometric map t ↦ (cos t, sin t). Anyone identifying Mathlib's Circle.exp covering with the concrete trig parametrization used for winding/degree cites this. Proof is funext plus ULift and Subtype extensionality, reducing to the ambient vector identity carrierCovering_val.
Claim. As maps $\mathbb{R}\to\mathrm{TopCat.sphere}\,1$, the composition of the inverse ULift homeomorphism on the metric unit-circle carrier with the carrier covering (the transport of $\mathrm{Circle.exp}$ along the orthonormal-basis isometry) equals the trigonometric parametrization $t\mapsto(\cos t,\sin t)$ pointwise.
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 on singular 1-chains must lift simplices through a covering of the imported TopCat.sphere 1 object, with no project-local stand-in for $S^1$.
SphereOneCarrier is the metric unit sphere in the Euclidean plane $\mathbb{R}^2$ that sits under the ULift in TopCat.sphere 1. The carrier covering is $\mathbb{R}\to\mathrm{SphereOneCarrier}$ obtained by composing Mathlib's Circle.exp with the homeomorphism from the complex unit circle onto that metric carrier. Separately, trigCirclePoint packages the ambient vector $(\cos t,\sin t)$ as a point of the exact TopCat.sphere 1 object via ULift.up.
Upstream, carrierCovering_val already equates the carrier covering (as an ambient Euclidean vector) with the trigonometric vector $(\cos t,\sin t)$. The present statement lifts that ambient identity through ULift into the precise TopCat carrier.
proof idea
Tactic proof by pointwise extensionality. Apply funext on the real parameter $t$, then ULift.ext and Subtype.ext to peel the ULift and the metric-sphere subtype. The remaining ambient equality is exactly carrierCovering_val t, which identifies the transported Circle.exp value with $(\cos t,\sin t)$ via the complex exponential and the orthonormal basis OneI.
why it matters
Bridge lemma that lets every later argument work with the concrete trig map while inheriting covering and homeomorphism facts proved on the Mathlib Circle side.
The headline parent is isCoveringMap_trigCirclePoint: rewrite along this equality and transport isCoveringMap_carrierCovering across the inverse ULift homeomorphism, yielding that $t\mapsto(\cos t,\sin t)$ is an honest covering of the imported TopCat.sphere 1. That covering is the foundation for the winding/degree invariant on singular 1-chains.
Also used by trigCirclePoint_eq_iff_exp (two angles hit the same sphere point iff their Circle.exp values agree) and trigCirclePoint_surjective (every point of TopCat.sphere 1 is hit). Together these close the covering-space toolkit needed for the circle $H_1$ derivation without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.