singularTwoBoundaryFree_freeMk_of_cone_faces
plain-language theorem explainer
If a singular 2-simplex on S¹ has base face equal to a singular 1-simplex s and equal side faces, its free-module boundary is exactly the free generator of s. Algebraic topologists working the H₁(S¹) ≅ ℤ split cite this as the cone-filling identity. The proof rewrites by the free-boundary evaluation and cancels the equal sides by abelian-group arithmetic.
Claim. Let $\sigma$ be a singular $2$-simplex on $S^1$ and $s$ a singular $1$-simplex. If the base face satisfies $\delta_2\sigma=s$ and the two side faces agree ($\delta_0\sigma=\delta_1\sigma$), then the free-module boundary map sends the free generator of $\sigma$ to the free generator of $s$: $\partial^{\mathrm{free}}([\sigma])=[s]$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1=\mathrm{TopCat.sphere},1$, and proves that winding kills boundaries. Singular $1$- and $2$-simplices are the actual singular simplicial-set objects $(\mathrm{toSSet},S^1)(\Delta^n)$ for $n=1,2$.
The free boundary $\partial^{\mathrm{free}}$ on singular $2$-chains is the alternating face sum $\delta_0-\delta_1+\delta_2$ into free singular $1$-chains. Its evaluation on a free generator is recorded by singularTwoBoundaryFree_freeMk: $\partial^{\mathrm{free}}([\sigma])=[\delta_0\sigma]-[\delta_1\sigma]+[\delta_2\sigma]$.
A cone simplex over a closed edge is the geometric model of filling a loop by coning to a point: base face is the edge, and the two lateral faces coincide (both run from the cone tip to the same endpoint).
proof idea
One-line algebraic reduction. Rewrite the left-hand side by singularTwoBoundaryFree_freeMk, which expands $\partial^{\mathrm{free}}([\sigma])$ to $[\delta_0\sigma]-[\delta_1\sigma]+[\delta_2\sigma]$. Substitute the base-face hypothesis $\delta_2\sigma=s$ and the side-face equality $\delta_0\sigma=\delta_1\sigma$. The remaining identity $[t]-[t]+[s]=[s]$ is discharged by abel in the free abelian group on singular $1$-simplices.
why it matters
This is the algebraic shell of cone-filling: once a geometric cone $2$-simplex over a closed singular edge exists, the free boundary collapses exactly to that edge generator. Downstream, closedSingularOneCycle_bounds_of_cone_simplex uses it to conclude that the corresponding closed singular $1$-cycle bounds: "a cone singular $2$-simplex over a closed singular edge proves that the corresponding closed singular $1$-cycle bounds."
In the module's larger program, winding on $1$-cycles is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Cone-bounding of null-winding loops is the geometric handoff after the rel-endpoint nullhomotopy of zero-winding edges. The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.