singularOneChainFree
plain-language theorem explainer
The free integer module on singular 1-simplices of the circle S¹, i.e. the ambient chain group in which finite edge-flows live. Anyone working the singular-homology half of H₁(S¹;ℤ) ≅ ℤ cites it as the carrier of winding and incidence sums. It is a one-line Mathlib free-module construction on the type of singular 1-simplices.
Claim. Let $S^1$ denote the topological circle. Write $\mathrm{Sing}_1(S^1)$ for the set of continuous maps $\Delta^1\to S^1$. Then $\mathbb{Z}[\mathrm{Sing}_1(S^1)]$ is the free $\mathbb{Z}$-module on that set (finite formal $\mathbb{Z}$-linear combinations of singular 1-simplices).
background
The module CircleWindingChain lifts the path-level displacement/winding invariant of CircleWinding to singular simplices of the Mathlib circle TopCat.sphere 1. A singular 1-simplex is a continuous map $\Delta^1\to S^1$; the sibling abbreviation packages exactly that type as an object of the singular simplicial set.
Free modules on those simplices are the standard singular chain groups $C_1(S^1;\mathbb{Z})$. Elements are finitely supported functions from singular edges to $\mathbb{Z}$, i.e. finite integer edge-flows. The module doc states the goal: show that simplex displacement vanishes on boundaries, so winding descends to a homology invariant and splits the fundamental class, giving injectivity of the comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
No project-local circle model is used; everything sits on Mathlib's singular simplicial set and free-module functor.
proof idea
One-line definitional wrapper: apply Mathlib's free $\mathbb{Z}$-module functor ModuleCat.free ℤ to the type of singular 1-simplices of TopCat.sphere 1. No further proof obligations.
why it matters
This is the ambient object for every finite free edge-chain argument in the winding-kills-boundaries development. Downstream, incidence sums, support sums, L¹ norms of chains, and the theorems that free-boundary-zero flows have vanishing incidence at each vertex are all typed over it.
Together with the 2-simplex telescoping identity (displacement of the alternating face sum is zero) and the fact that the fundamental loop has winding 1, it supplies the chain group on which the winding homomorphism acts as a left inverse to the fundamental class—the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc notes that the surjective/generation half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology.
In the broader Recognition foundation this is pure topological scaffolding for the circle's first homology, not a forcing-chain (T0–T8) step, but it underwrites any later use of integer winding as a discrete invariant on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.