trigCirclePoint_eq_iff_exp
plain-language theorem explainer
Two real parameters hit the same point of the topological unit sphere under the trigonometric covering exactly when their circle exponentials agree. Anyone building the winding number on singular 1-chains of S¹ cites this as the bridge from the project parametrization to Mathlib's Circle.exp. The proof rewrites through the carrier covering and uses injectivity of the homeomorphism Circle ≃ SphereOneCarrier.
Claim. For $a,b\in\mathbb{R}$, the trigonometric covering points on the topological unit sphere agree if and only if the standard circle exponentials agree: $e^{ia}=e^{ib}$ on the unit circle in $\mathbb{C}$.
background
The module supplies lifting prerequisites for the winding (degree) invariant on singular 1-chains of TopCat.sphere 1. That invariant is built by lifting simplices through the trigonometric covering; its well-definedness needs the fiber structure of the cover.
The trigonometric covering sends $t\in\mathbb{R}$ to the point of the exact topological unit sphere given by $(\cos t,\sin t)$ (packaged as trigCirclePoint). Upstream, the carrier covering is the composite of Mathlib's Circle.exp with the homeomorphism from Mathlib's Circle onto the metric unit-circle carrier of TopCat.sphere 1. The identity ulift_carrierCovering_eq_trig states that this carrier covering, after the ULift homeomorphism into the exact sphere object, equals the trigonometric parametrization pointwise.
Local setting (module doc): no axioms or project-local $S^1$ replacements; everything is transported from Mathlib's covering and homeomorphism API.
proof idea
Term-mode proof. Rewrite the left-hand equality via ulift_carrierCovering_eq_trig, so both sides become the ULift-symmetric composite of the carrier covering. Unfold the composite (Function.comp_apply and the definition of carrierCovering) to expose circleHomeoCarrier ∘ Circle.exp. Split the biconditional: forward direction applies injectivity of circleHomeoCarrier and of Homeomorph.ulift.symm; reverse direction is substitution of the assumed equality of exponentials.
why it matters
This is the algebraic half of the fiber description needed for the winding number. The immediate parent is trigCirclePoint_eq_iff, which rewrites through this lemma and Mathlib's Circle.exp_eq_exp to obtain the deck-transformation form: the two parameters agree on the sphere iff they differ by an integer multiple of $2\pi$. That statement is, in the module's words, "the algebraic heart of both the well-definedness of the winding number and the value $w(\mathrm{fundamental})=1$".
In the Recognition chain the circle covering and its winding support the eight-tick octave (T7) and the topological side of the forcing apparatus. Without a clean identification between the project parametrization and Mathlib's exponential, path-lifting monodromy cannot be applied to the exact TopCat.sphere 1 object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.