singularOneBoundaryFree
plain-language theorem explainer
Explicit free ℤ-module boundary ∂₁ from singular 1-chains on S¹ to singular 0-chains: each directed edge goes to terminal vertex minus initial vertex. Anyone working with free-boundary-zero flows, cyclic edge families, or the kernel decomposition of 1-cycles on the circle cites it. Defined by freeness: ModuleCat.freeDesc on generators via the two face maps of the singular simplicial set.
Claim. The free-module boundary $\partial_1^{\mathrm{free}} : C_1^{\mathrm{free}}(S^1;\mathbb{Z}) \to C_0^{\mathrm{free}}(S^1;\mathbb{Z})$ is the unique $\mathbb{Z}$-linear map determined on generators by sending each singular $1$-simplex $s$ to $\delta_0(s) - \delta_1(s)$ (terminal $0$-face minus initial $0$-face of $s$).
background
The module lifts path-level winding/displacement on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
SingularOneSimplex is a $1$-simplex in the singular simplicial set of TopCat.sphere 1. singularOneChainFree (resp. singularZeroChainFree) is the free $\mathbb{Z}$-module on those $1$-simplices (resp. $0$-simplices). The classical singular boundary on a $1$-simplex is terminal vertex minus initial vertex; this definition packages that rule as a morphism in ModuleCat ℤ on the free modules used throughout the chain-level arguments.
Face maps $\delta_0,\delta_1$ come from the singular simplicial set of the circle; on a directed edge they extract the two endpoint $0$-simplices.
proof idea
One-line definition by the universal property of free modules: ModuleCat.freeDesc extends the generator-wise assignment $s \mapsto \mathrm{freeMk}(\delta_0 s) - \mathrm{freeMk}(\delta_1 s)$ to a unique $\mathbb{Z}$-linear map $C_1^{\mathrm{free}}\to C_0^{\mathrm{free}}$. No further lemmas; the two face operators are those of TopCat.toSSet.obj (TopCat.sphere 1).
why it matters
This is the working boundary map for all free-module cycle arguments in CircleWindingChain. Downstream, cyclicEdgeFamily_freeBoundary_zero shows cyclic edge walks lie in its kernel (C₀ telescoping); boundaryIncidenceSum_eq_zero_of_boundary_zero and its primed form convert kernel membership into vanishing incidence sums at vertices; cyclicEdgeListExtractionStep and the free-boundary-kernel decomposition theorems use $\ker\partial_1^{\mathrm{free}}$ as the ambient space of balanced flows that split into directed cycles.
Those decompositions feed cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles and the spanning statement for closed singular $1$-chains, which close the generation half of the winding isomorphism on $H_1(S^1)$. The module goal is the homology-invariant winding left-inverse to the fundamental class; this boundary is the algebraic substrate that makes "cycle" precise at the free-module level without Mathlib's full singular chain complex API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.