singularTwoBoundaryFree_freeMk_coneCircleMap
plain-language theorem explainer
Free-boundary identity for the cone over an arbitrary singular edge of S¹: the free 2-boundary of that cone equals the terminal-return generator minus the constant-apex generator plus the original edge. Anyone assembling the chain-level cone shell before specializing to zero winding cites this. The proof is a short rewrite cascade through the free-boundary formula and the three explicit cone face maps.
Claim. For every continuous map $f:\Delta^1\to S^1$, write $C_f$ for the cone $2$-simplex obtained by coning the path of $f$ (once continuity of the cone map is given). Then the free singular boundary sends the free generator $[C_f]$ to $[\tau_f]-[c_{f(0)}]+[f]$, where $\tau_f$ is the terminal-return side of the cone and $c_{f(0)}$ is the constant edge at the apex value $f(0)$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$; a singular $2$-simplex is the analogous map from $\Delta^2$.
The cone construction packages a path $\gamma:I\to S^1$ into a pointwise cone map on $\Delta^2$, then (after continuity) into a concrete $2$-simplex. Its three faces are fixed by prior lemmas: $\delta_1$ is the constant edge at the apex $\gamma(0)$, $\delta_2$ recovers the original edge, and $\delta_0$ is the terminal-return side along the cone.
Free generators and the free boundary map live in the free module on singular simplices (Mathlib ModuleCat.freeMk / free singular chains). This theorem records the resulting free $1$-chain shell before any winding hypothesis is imposed.
proof idea
One short rewrite proof. First apply the free-boundary evaluation lemma that turns the free generator of a singular $2$-simplex into the alternating free sum of its three face $1$-simplices. Expand each face via the singular-face comparison for maps. Then replace the three faces by the cone face identities: face $0$ is the terminal-return side, face $1$ is the constant apex edge, and face $2$ is the original edge $f$. The resulting free combination is exactly terminal-return minus constant apex plus $f$.
why it matters
This is the unrestricted cone boundary shell used by the zero-winding specialization singularTwoBoundaryFree_freeMk_coneCircleMap_of_simplexWinding_zero. That parent cancels terminal-return against the constant apex once simplexWinding f = 0, leaving the free boundary equal to the original edge generator alone.
In the module narrative, that cancellation is the chain-level step that turns a null-homologous (zero-winding) edge into an explicit free boundary, feeding the "winding kills boundaries" / split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The doc-comment flags the zero-winding loop theorem as precisely this special case. It does not yet touch the generation/surjectivity half, which still needs a prism or subdivision operator absent from Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.