fundamentalSphereOneSingularOneChain
plain-language theorem explainer
The degree-1 singular chain on S¹ that selects the once-around fundamental 1-simplex as a free summand. Anyone building the generator of H₁(S¹;ℤ) from singular chains cites this map. It is the coproduct-inclusion of that simplex into C₁(S¹;ℤ), not a proved cycle or generator by itself.
Claim. The canonical map $\mathbb{Z}\to C_1(S^1;\mathbb{Z})$ that sends $1$ to the once-around fundamental singular $1$-simplex of $\mathrm{TopCat.sphere}\,1$ (the free summand inclusion of that simplex in the singular chain module).
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It works with Mathlib's singular chain complex of the topological circle and does not yet feed the strict T8 bridge until a real equivalence to the imported singular homology object is proved.
The target complex is the integer singular chain complex of $S^1$. Its degree-1 term is the free $\mathbb{Z}$-module on all continuous maps $\Delta^1\to S^1$. The once-around singular 1-simplex is the geometric generator candidate: the image of the standard fundamental circle path under the singular-set equivalence. The present definition packages that simplex as a chain by taking the corresponding coproduct summand inclusion $\mathbb{Z}\hookrightarrow C_1(S^1;\mathbb{Z})$.
proof idea
Pure definition, not a proof. The body is the coproduct inclusion Sigma.ι into the free $\mathbb{Z}$-module on the set of singular 1-simplices of $S^1$, indexed at the once-around fundamental singular 1-simplex. No lemmas are applied; the term is the canonical summand map for that simplex.
why it matters
This is the chain-level handle on the once-around loop used throughout the circle $H_1$ workbench. Downstream, the boundary-vanishing theorem shows this chain is a cycle (chain-level equal-faces for the once-around simplex). That cycle is lifted to fundamentalCycle in the cycles object, identified with integer multiples of the geodesic free chain $0\to 2\pi$, and sent to $1$ by the winding chain map, giving the injective half of $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ (infinite order of the fundamental class).
In the Recognition framework this sits in the Foundation layer supporting the circle homology computation that the module doc flags as a missing atom toward a strict T8 bridge. It does not itself close $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: surjectivity (generation) remains the open half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.