singularOneChainFreeIso
plain-language theorem explainer
Identifies the Mathlib singular 1-chains of the circle with the free ℤ-module on actual continuous maps Δ¹ → S¹. Anyone working the generation half of H₁(S¹;ℤ) ≅ ℤ cites this to move between coproduct-summand notation and finite-support free generators. The maps are the standard free-desc / sigma-desc pair; both composite identities are checked by evaluating on generators.
Claim. There is a canonical isomorphism of $\mathbb{Z}$-modules $C_1(S^1;\mathbb{Z}) \cong \mathbb{Z}\langle\{\text{singular }1\text{-simplices }\Delta^1\to S^1\}\rangle$, sending each coproduct summand generator to the matching free generator and conversely.
background
The module works at the chain level on $S^1=\mathrm{TopCat.sphere},1$. Mathlib's singular chain complex $C_\bullet(S^1;\mathbb{Z})$ presents $C_1$ as a coproduct of copies of $\mathbb{Z}$, one per continuous map $\Delta^1\to S^1$. That presentation is awkward for finite-support bookkeeping: cancellation and cycle-spanning arguments want the free module on the set of those maps, with ordinary finitely supported integer coefficients.
singularOneChainFree is exactly that free module. The two directions of the iso are already defined: one sends each coproduct summand to the free generator of the same simplex; the other free-descends by sending each free generator back to the unit of its coproduct summand. Upstream, sphereOneSingularIntChainComplex is the imported Mathlib complex whose $H_1$ is the strict T8 target.
Locally the module lifts path winding to singular 1-simplices and proves winding kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half still needs free-coordinate normal forms; this iso supplies them.
proof idea
Definitional iso: forward map is the already-built sigma-desc that sends each summand to the free generator; inverse is free-desc sending each free generator to the unit of its summand.
hom_inv_id is proved by sigma-extensionality then module-hom extensionality: on a summand $s$ and integer $n$, unfold the desc, apply toSpanSingleton, push the scalar through the free-desc, and recover $n\cdot\iota_s(1)=\iota_s(n)$.
inv_hom_id uses free-hom extensionality on generators: free-desc of $s$ is $\iota_s(1)$, and sigma-desc of that unit is the free generator of $s$. Both sides are pure generator bookkeeping; no topology enters.
why it matters
This is the representational bridge the generation program runs on. Downstream theorems that prove every closed singular 1-chain is homologous to an integer multiple of the fundamental cycle first transport the cycle into free coordinates via the forward map, run a free-boundary kernel decomposition (directed cycles, oriented cyclic families, free prisms), then transport back. Concrete consumers include closedSingularOneChainList_spansCycles_of_freeBoundaryKernel_decomposes, cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles, and the various fundamentalCycle_boundary_generates_of_* lemmas.
In the Recognition forcing chain this sits under the strict T8 target: identifying $H_1(S^1;\mathbb{Z})$ with $\mathbb{Z}$ so the once-around generator is unique up to sign. The module already has winding as a left inverse to the fundamental class; the missing half is surjectivity of the comparison map, which needs free-coordinate cancellation. The degree-2 analog is recorded immediately below for the same reason.
No axioms or sorry: pure identification of two presentations of the same free abelian group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.