isCoveringMap_trigCirclePoint
plain-language theorem explainer
The trigonometric map $t\mapsto(\cos t,\sin t)$ from $\mathbb{R}$ into the imported unit sphere $S^1$ is a covering map. Anyone constructing a winding or degree invariant for singular $H_1(S^1;\mathbb{Z})$ cites this as the covering-space foundation. The proof rewrites the map through a ULift homeomorphism identity and transports Mathlib's exponential covering along the circle homeomorphism.
Claim. The map $t \mapsto (\cos t, \sin t)$ from $\mathbb{R}$ into the metric unit circle $S^1 \subset \mathbb{R}^2$ (the carrier of the imported topological $1$-sphere) is a covering map.
background
Mathlib's singular-homology development stops at the totally disconnected case, so any route to $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ must build its own degree or winding invariant by lifting singular simplices through a covering of the imported topological $1$-sphere. This module supplies that covering-space foundation without axioms, sorry, or a project-local replacement for $S^1$.
The trigonometric parametrization sends $t\in\mathbb{R}$ to the ULift of the unit vector $(\cos t,\sin t)$ in the metric sphere carrier. Upstream, the carrier covering is already known to be a covering map: it is Mathlib's exponential covering of the complex unit circle, transported along the orthonormal-basis isometry $\mathbb{C}\simeq\mathbb{R}^2$ and the resulting homeomorphism onto the metric circle. A separate pointwise identity equates the ULift of that carrier covering with the trigonometric parametrization used here.
proof idea
Term-mode proof in two steps. First rewrite the goal by the pointwise identity that the ULift of the carrier covering equals the trigonometric parametrization. The goal becomes: the composite of the carrier covering with the inverse ULift homeomorphism is a covering map. Apply the homeomorphism-composition lemma for covering maps to the already-proved carrier covering, using the inverse ULift homeomorphism on the metric sphere carrier. No further case analysis is required.
why it matters
This is the headline result of the CircleCovering module and the covering-space foundation for the by-hand circle-$H_1$ derivation. Downstream, CircleLifting repackages it as a bare IsCoveringMap term for direct use with the path-lifting API, so every subsequent lift of singular $1$-simplices and every winding-number computation rests on this fact.
In the broader Recognition foundation layer the result is infrastructure rather than a forcing-chain step: it lets the project compute $\deg$ and winding on the imported $S^1$ with real Lean equivalences only. No T0–T8 landmark is discharged here; the payoff is a clean, axiom-free covering of TopCat.sphere 1 that later homology and monodromy arguments can quote without rebuilding the exponential covering each time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.