bnd_genUnit_pathSimplex
plain-language theorem explainer
The degree-0 boundary of the unit 1-chain of a path simplex equals the difference of the unit 0-chains at the path endpoints. Singular-homology workers in the foundation layer cite this when turning path-connectedness into a homology relation on point chains. The proof rewrites through the unit-generator identity and applies the already-proved boundary formula for path simplices.
Claim. Let $X$ be a topological space and $\gamma$ a continuous path from $x$ to $y$ in $X$. Then the degree-$0$ boundary of the generating unit $1$-chain of the path simplex of $\gamma$ equals the difference of the generating unit $0$-chains of the constant simplices at the endpoints: $\partial_0(\iota_1(\sigma_\gamma)) = \iota_0(c_y) - \iota_0(c_x)$.
background
The module builds singular chain groups on a topological space $X$ in the coproduct presentation used throughout the Singular* foundation stack. In that presentation, each singular $n$-simplex $s$ contributes a generating unit chain $\iota_n(s)$ in the degree-$n$ chain group; the lemma genUnit_eq records that this unit is exactly the free generator evaluated at $1\in\mathbb{Z}$.
The boundary operator $\partial_n$ is the differential of the singular chain complex, typed on those coproduct groups. Constant $0$-simplices $c_x$ and $c_y$ are the degenerate maps sending the standard $0$-simplex to a point. A continuous path $\gamma:x\to y$ determines a singular $1$-simplex $\sigma_\gamma$ (the path simplex).
Upstream, the prism and Mayer–Vietoris layers already supply the chain-level boundary identity for path simplices on free generators. The present lemma lifts that identity from free generators to the unit-chain presentation used by the rest of the sphere package.
proof idea
Rewrite the left-hand side via genUnit_eq and the module-category composition identity, so the claim becomes an equality of free generators evaluated at $1\in\mathbb{Z}$. A short calc then applies the upstream path-simplex boundary formula gen_pathSimplex_bnd, which gives $\partial(\mathrm{gen}(\sigma_\gamma))=\mathrm{gen}(c_y)-\mathrm{gen}(c_x)$ on free generators. The final step restores unit chains by subApp and two more uses of genUnit_eq. No new geometric content is introduced; the work is presentation bookkeeping.
why it matters
Immediate parent is exists_bnd_eq_sub: joined points have homologous point chains. That lemma packages the present identity as an existence statement (there is a $1$-chain whose boundary is $\iota_0(c_y)-\iota_0(c_x)$), taking the unit path simplex of any witnessing path. Without the unit-level boundary formula, path-connectedness would not pass cleanly into the singular chain complex used by the sphere and Mayer–Vietoris layers.
In the Recognition foundation stack this is pure singular-homology scaffolding: it lets later arguments treat path components as homology classes of $0$-chains, which is the standard bridge from topology of $X$ to $H_0(X)$. It does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder; those enter only if downstream sphere or dimension arguments quote the resulting $H_0$ facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.