isCoveringMap_carrierCovering
plain-language theorem explainer
The real-line map obtained by composing the complex exponential covering with the homeomorphism from Mathlib's unit circle onto the metric carrier of TopCat.sphere 1 is itself a covering map. Anyone building a winding or degree invariant for singular H₁(S¹) cites this intermediate transport step. The proof is a one-line homeomorph_comp application of Mathlib's Circle.isCoveringMap_exp.
Claim. The composite map $\mathbb{R} \to S^1_{\mathrm{carrier}}$ given by $t \mapsto$ (homeomorphism of Mathlib's unit circle onto the metric unit-circle carrier) $\circ\, e^{it}$ is a covering map.
background
This module builds the covering-space foundation needed 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 any winding invariant must lift singular simplices through a covering of the imported TopCat.sphere 1 object.
Mathlib already knows that $\mathrm{Circle.exp}:\mathbb{R}\to\mathrm{Circle}$, $t\mapsto e^{it}$, is a covering map. The local carrier SphereOneCarrier is the metric unit sphere in the Euclidean plane (the exact fibre type of TopCat.sphere 1). The homeomorphism circleHomeoCarrier identifies Mathlib's multiplicative circle with that carrier via the orthonormal-basis isometry $\mathbb{C}\simeq\mathbb{R}^2$.
The composite carrierCovering is defined as that homeomorphism after Circle.exp. The present theorem asserts that the composite remains a covering map, so later steps can transport the covering property all the way to the trigonometric map $t\mapsto(\cos t,\sin t)$.
proof idea
One-line term proof. Apply Mathlib's lemma that covering maps are stable under post-composition by a homeomorphism (IsCoveringMap.homeomorph_comp) to Circle.isCoveringMap_exp and the homeomorphism circleHomeoCarrier. No case splits or local trivializations are rebuilt by hand.
why it matters
This is the middle rung of the transport ladder that yields the module headline isCoveringMap_trigCirclePoint: the concrete map $t\mapsto(\cos t,\sin t)$ on the imported TopCat.sphere 1 is a covering map. Downstream that theorem rewrites the trigonometric parametrization as a ULift of carrierCovering and reapplies homeomorph stability, quoting this result.
In the Recognition Science foundation, the covering supplies the degree/winding invariant on singular 1-chains used for the by-hand circle-$H_1$ derivation tied to the T7 eight-tick octave (period $2^3$) and the realized circle defect. No project-local replacement for $S^1$ is introduced: everything is transported along real Lean equivalences from Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.