singularOneChainToFree_freeToChain
plain-language theorem explainer
Transporting a free singular 1-chain on S¹ into the raw chain group C₁(S¹;ℤ) and back recovers the original free chain: the free-to-raw map is a right inverse of the raw-to-free map. Anyone working with free-module normal forms for singular chains on the circle cites this. The proof is a one-line extraction of the inverse-hom identity of the free-chain isomorphism, simplified in ModuleCat.
Claim. For every free singular $1$-chain $c$ on $S^1$ (an element of the free $\mathbb{Z}$-module on singular $1$-simplices), applying the free-to-raw map into $C_1(S^1;\mathbb{Z})$ and then the raw-to-free map returns $c$. Equivalently, $\mathrm{toFree}\circ\mathrm{freeToChain}=\mathrm{id}$ on free $1$-chains.
background
The module builds the winding invariant on singular $1$-simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Two presentations of degree-$1$ chains are in play. The raw group is the degree-$1$ object of the singular integer chain complex of $S^1$ (a coproduct of $\mathbb{Z}$ summands). The free module singularOneChainFree is the explicit free $\mathbb{Z}$-module on actual singular $1$-simplices, exposing finite-support normal form. The maps singularOneChainToFree (raw $\to$ free) and singularOneChainFreeToChain (free $\to$ raw) are the two legs of the isomorphism singularOneChainFreeIso, whose inverse-hom identity is the algebraic content used here.
Downstream structures such as DirectedCycleFreeTerm record a genuine cycle together with its free-chain coordinate, linked by the raw-to-free map; round-trip identities keep those coordinates honest.
proof idea
One-line wrapper around the inverse-hom identity of singularOneChainFreeIso. Apply congruence in the free-chain argument to singularOneChainFreeIso.inv_hom_id, which states that free-to-raw followed by raw-to-free is the identity morphism in ModuleCat. Simplify the composite of module morphisms (ModuleCat.hom_comp, ModuleCat.hom_id, and the corresponding LinearMap facts) to obtain the pointwise identity on an arbitrary free chain $c$.
why it matters
This is the free-side half of the free/raw isomorphism for singular $1$-chains on $S^1$. It lets every free edge-chain be treated as the free coordinate of a raw chain without loss of information.
Parents that consume it include DirectedCycleFreeTerm (whose chain_eq field equates the free coordinate to the image of a genuine cycle under raw-to-free), and the constructors directedCycleFreeTerm_of_cyclicFamily and directedCycleFreeTerm_of_orientedCyclicFamily, which package cyclic extraction as a free term with vanishing free boundary and integer winding. OrientedCyclicFamilyTerm sits in the same pipeline.
In the module narrative this supports the chain-level winding homomorphism that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The generation/surjectivity half still needs simplicial prism or subdivision, which Mathlib singular homology does not yet supply. No Recognition forcing-chain step (T0–T8) is discharged here; the lemma is pure singular-chain bookkeeping on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.