singularOneBoundaryFree_freeMk
plain-language theorem explainer
On free singular 1-chains of the circle, the explicit free boundary applied to a generator equals the free generator of the terminal 0-face minus that of the initial 0-face. Anyone computing cycles or incidence coefficients for singular edges on S¹ cites this evaluation. The proof is a two-step rewrite: unfold the freeDesc definition and apply freeDesc on generators.
Claim. For every singular $1$-simplex $s$ on $S^1$, the explicit free-module boundary map sends the free generator of $s$ to $\mathrm{free}(\delta_0 s) - \mathrm{free}(\delta_1 s)$, i.e. terminal $0$-face minus initial $0$-face.
background
The module builds the winding invariant on singular $1$-simplices of the topological circle $S^1=\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}$.
A singular $1$-simplex is an element of the singular simplicial set $(\mathrm{TopCat.toSSet}\cdot S^1)$ in degree $1$. Free singular $1$-chains and $0$-chains are the free $\mathbb{Z}$-modules on those simplices. The explicit free boundary is the unique module map out of free $C_1$ specified on generators by terminal face minus initial face (face maps $\delta_0,\delta_1$ of the singular simplicial set).
Upstream, singularOneBoundaryFree is exactly that freeDesc of the alternating face formula. This lemma records how that map evaluates on free generators, which is the computational interface every later boundary-vanishing or incidence argument needs.
proof idea
One-line computational unwrap. Rewrite by the definition of the free boundary (the freeDesc of the face formula), then apply the universal property of free modules on generators (ModuleCat.freeDesc_apply). The right-hand side is literally the defining clause of that freeDesc, so equality is immediate. No geometric content is used.
why it matters
This is the generator-level evaluation that turns the free boundary from a black-box Hom into a concrete terminal-minus-initial formula. Downstream it is the rewrite step in vertexBoundaryCoeff_freeMk (incidence coefficients), in cyclicEdgeFamily_freeBoundary_zero (closed edge-walks are free cycles via $C_0$ telescoping), in parallelTwoEdgeFlow_boundary_zero and singleEdgeFlow_zero_boundary_faces_eq (balanced two-edge and single-edge flows), and in the comparison singularOneChainFreeToChain_boundary_free that identifies the free boundary with Mathlib's singular boundary after transport.
In the module's program, free-boundary vanishing is the chain-level companion of the winding kills-boundaries identity (simplexDisplacement_boundary). Together with the fundamental-loop winding equal to $1$, that supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a prism or subdivision operator Mathlib does not yet provide; this lemma does not close that gap, but it is the algebraic primitive every free-cycle argument in the chain rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.