gen_pathSimplex_bnd
plain-language theorem explainer
In singular chains, the boundary of a path 1-simplex is the constant 0-simplex at the target minus that at the source: ∂[γ] = [y] − [x]. Anyone building H₀ computations or path-induced chain homotopies cites this. The proof is a short reduction through the alternating-face formula, identifying the two faces with constant simplices.
Claim. Let $X$ be a topological space and $\gamma$ a path from $x$ to $y$ in $X$. Writing $[\sigma]$ for the generator of the singular chain group attached to a singular simplex $\sigma$, one has $\partial[\gamma] = [c_y] - [c_x]$, where $c_z$ denotes the constant $0$-simplex at $z$.
background
The module works in the singular chain complex of a space $X$, presented via the coproduct of free $\mathbb{Z}$-modules on singular simplices. The generator map sends a singular $n$-simplex $a$ to the corresponding basis arrow into the degree-$n$ chain group. The boundary out of degree $n+1$ is the differential of that complex.
Upstream, the boundary of any generator is the alternating sum of its faces: $\mathrm{gen}(a)\circ\partial = \sum_k (-1)^k,\mathrm{gen}(\delta_k a)$. A path $\gamma:x\to y$ is realized as a singular $1$-simplex (the path simplex). Constant maps give constant $0$-simplices at points of $X$. Face operators on the path simplex recover those constant simplices at the endpoints.
Locally this sits in the singular-sphere foundation layer: path simplices supply the elementary $1$-chains used to compare point inclusions and to build chain homotopies.
proof idea
Apply the general face formula for the boundary of a generator in degree $1$. The sum runs over $\mathrm{Fin},2$. Expand powers of $-1$ to get $+\mathrm{gen}(\delta_0\gamma)-\mathrm{gen}(\delta_1\gamma)$. Identify $\delta_0$ of the path simplex with the constant simplex at the target $y$, and $\delta_1$ with the constant simplex at the source $x$, via the point-of-face lemmas and the extension criterion that compares $0$-simplices by their image points. Rewrite the resulting sum as a difference.
why it matters
This is the elementary identity $\partial[\gamma]=[y]-[x]$ that makes paths into chain-level data. Downstream it is applied elementwise to unit generators (boundary of a path unit chain) and feeds the construction of a chain homotopy between the two point-inclusion chain maps associated to the endpoints of $\gamma$. That homotopy is the singular-chain avatar of "a path joins $x$ to $y$," and is the standard input for showing path-components control $H_0$ and for comparing point-supported cycles on spheres and related spaces in the foundation stack.
In the broader Recognition setting this is pure algebraic topology scaffolding (singular chains, not yet the forcing chain T0–T8), but it is the concrete mechanism by which continuous paths become homological equalities used later when point and sphere data are compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.