trigCirclePoint_surjective
plain-language theorem explainer
Every point of the exact unit-circle object arises from the trigonometric parametrization at some real angle. Path-lifting and winding constructions cite this to pick a real starting height for any continuous path on the circle. The proof chains surjectivity through the ULift homeomorphism, the Mathlib Circle homeomorphism onto the metric carrier, and Complex.arg on the exponential covering.
Claim. The once-around trigonometric parametrization $\mathbb{R}\to S^1$ into the exact metric unit circle (as a $\mathrm{TopCat}$ sphere) is surjective: for every point $y$ on that circle there exists a real angle $t$ such that the parametrization at $t$ equals $y$.
background
This module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. One lifts a path through the trigonometric covering and measures how far the lift travels in $\mathbb{R}$. The module doc stresses that displacement is independent of the choice of continuous lift, via a deck-transformation argument with period $2\pi\mathbb{Z}$.
The map in question is the once-around trigonometric parametrization into that exact sphere object: a real angle is sent to the ULift of the corresponding unit vector in the ambient Euclidean plane. Upstream, the carrier covering $\mathbb{R}\to\mathrm{SphereOneCarrier}$ is Mathlib's Circle.exp transported by the homeomorphism from Mathlib's Circle onto the metric unit-circle carrier. A prior identification states that the ULift of the carrier covering equals the trigonometric parametrization pointwise.
proof idea
Fix an arbitrary target point $y$ on the sphere. Rewrite via the pointwise identification of the trigonometric map with the ULifted carrier covering, so the goal becomes surjectivity of that composite. Pull $y$ back along the ULift homeomorphism to a carrier point $c$, then along the Circle-to-carrier homeomorphism to a Mathlib Circle point $z$. Take the preimage angle to be $\mathrm{Complex.arg}(z)$. Unfold the carrier covering as homeomorphism composed with Circle.exp, apply Circle.exp_arg, and discharge with the two surjectivity witnesses.
why it matters
This is the existence half of the covering used to start path lifts. The chosen real lift of a path's initial point is defined by applying this surjectivity and taking Classical.choose; its specification theorem is exactly the choose_spec of that application. Additivity of displacement under path concatenation also invokes it to align the starting angle of the first factor, which (together with homotopy invariance) makes winding a homology invariant: alternating face sums of singular $2$-simplices telescope to zero.
In the Recognition forcing chain this supports the continuous model behind T7 (the eight-tick octave): the circle covering and its deck group $2\pi\mathbb{Z}$ are the analytic counterpart of the discrete period-$2^3$ cycle. The module claims no axioms, sorry, or project-local $S^1$ replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.