carrierCovering
plain-language theorem explainer
Defines the real-line covering of the metric unit-circle carrier as Mathlib's complex exponential composed with the homeomorphism from the multiplicative circle onto that carrier. Anyone building winding numbers or lifting singular simplices for H₁(S¹;ℤ) cites this map. The body is a one-line function composition.
Claim. Define the map $c:\mathbb{R}\to S^1_{\mathrm{carrier}}$ by $c=h\circ\exp$, where $\exp:\mathbb{R}\to\mathbb{S}^1\subset\mathbb{C}$ is Mathlib's circle exponential and $h:\mathbb{S}^1\xrightarrow{\simeq}S^1_{\mathrm{carrier}}$ is the induced homeomorphism onto the metric unit-circle carrier of $\mathrm{TopCat.sphere}\,1$.
background
This module builds the 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 every route to the circle's first homology must lift simplices through a covering of the imported TopCat.sphere 1 object.
SphereOneCarrier is the exact metric sphere of radius one in the ambient Euclidean plane under the ULift used by TopCat.sphere 1. Upstream, circleHomeoCarrier is the homeomorphism from Mathlib's multiplicative Circle onto that carrier, induced by the orthonormal-basis isometry $\mathbb{C}\simeq\mathbb{R}^2$ that preserves the unit sphere.
Mathlib already knows Circle.exp : ℝ → Circle is a covering map. Transporting it along the homeomorphism yields a covering of the precise carrier used by the project's trigonometric parametrization (cos t, sin t).
proof idea
One-line definition: compose Mathlib's Circle.exp with the upstream homeomorphism circleHomeoCarrier. No tactics; the covering property is proved later by IsCoveringMap transport along that homeomorphism.
why it matters
This is the intermediate covering that the module's headline result transports further into TopCat.sphere 1. Downstream, isCoveringMap_carrierCovering shows it is a genuine covering map; carrierCovering_val identifies its ambient values with (cos t, sin t); and ulift_carrierCovering_eq_trig equates the ULifted map with trigCirclePoint.
Those identities feed CircleLifting.trigCirclePoint_eq_iff_exp (parameters hit the same point iff their exponentials agree) and CircleWinding.trigCirclePoint_surjective (every sphere point is hit). Together they supply the degree/winding invariant needed for the by-hand $H_1(S^1)$ argument that realizes the T7 eight-tick octave cycle as a circle defect, without axioms or project-local replacements for $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.