isCoveringMap_trig
plain-language theorem explainer
The trigonometric parametrization $t \mapsto (\cos t, \sin t)$ of the imported $S^1$ is a covering map, packaged for Mathlib's path-lifting API. Anyone building the winding/degree invariant on singular 1-chains cites this. The proof is a one-line alias of the established covering theorem in CircleCovering.
Claim. The continuous map $\mathbb{R} \to S^1$ given by $t \mapsto (\cos t, \sin t)$ (as a point of the imported $\mathrm{TopCat.sphere}\,1$) is a covering map.
background
The module supplies lifting prerequisites for the circle winding invariant on singular 1-chains of the imported $S^1$. Two ingredients are needed: contractibility of standard simplices (so monodromy kills boundaries) and the fiber structure of the trigonometric covering.
The map in question is trigCirclePoint: $t \mapsto ULift.up,\langle(\cos t,\sin t),\ldots\rangle$, the once-around trigonometric parametrization into the exact TopCat.sphere 1 object. Upstream, CircleCovering already proves this map is a covering map by transporting the carrier covering across a homeomorphism with the ULift sphere carrier: "the trigonometric parametrization $t \mapsto (\cos t, \sin t)$ of the imported TopCat.sphere 1 object is a covering map. This is the covering-space foundation for the winding / degree invariant."
Mathlib's IsCoveringMap API then supplies path lifts, monodromy invariance under endpoint-relative homotopy, and the deck-group description of fibers.
proof idea
One-line wrapper: the statement is definitionally the already-proved theorem isCoveringMap_trigCirclePoint from CircleCovering. No extra argument is needed; the local name exists only so CircleWinding can call the covering map under a short identifier aligned with the lifting module.
why it matters
This is the covering-map handle that CircleWinding uses everywhere. Downstream, pathLift is defined as isCoveringMap_trig.liftPath of a path from its canonical start; pathLift_lifts and pathLift_zero are the corresponding lift axioms. Lift independence (pathDisplacement_eq), homotopy invariance (pathDisplacement_homotopic), and additivity under concatenation (pathDisplacement_trans) all invoke this covering map to move between continuous lifts in $\mathbb{R}$ and paths on $S^1$.
Together those three properties make path displacement a homology invariant: boundaries of singular 2-simplices are null-homotopic in the contractible standard simplex, so their displacement vanishes, and face sums telescope. That is the algebraic heart of the winding/degree invariant on singular 1-chains of $S^1$. No project-local $S^1$ replacement or axiom is involved; the covering is the exact imported sphere object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.