exists_bnd_of_pathConnected
plain-language theorem explainer
In a path-connected space, every singular 0-chain z is homologous to its total mass times a fixed base-point 0-simplex: there is a 1-chain whose boundary is z minus aug(z)·[x₀]. Algebraic topologists cite this when identifying H₀(X)≅ℤ. The proof is free induction on the chain group, reducing generators to a path from x₀ to the support point.
Claim. Let $X$ be a path-connected topological space and fix a base point $x_0\in X$. For every singular $0$-chain $z$, there exists a singular $1$-chain $v$ such that $\partial v=z-\mathrm{aug}(z)\,[x_0]$, where $[x_0]$ denotes the constant $0$-simplex at $x_0$ and $\mathrm{aug}$ is the augmentation (sum of coefficients).
background
Singular chain groups $C_n(X)$ are free abelian on continuous maps $\Delta^n\to X$. The boundary $\partial:C_1\to C_0$ and the augmentation $\mathrm{aug}:C_0\to\mathbb{Z}$ (total coefficient sum) form the start of the augmented singular complex. The constant simplex $[x_0]$ is the $0$-generator at a chosen base point.
The module SingularSphere builds the standard computation of low-degree singular homology of spheres and path-connected spaces, using the free-abelian induction principle and generating units from SingularMayerVietoris. Path-connectedness supplies a continuous path between any two points, which becomes a singular $1$-simplex whose boundary is the difference of the two $0$-simplices.
Upstream, freeInduction says a property of all chains closed under $0$, addition, and integer scaling need only be checked on generators. genUnit is the free generator attached to a singular simplex index.
proof idea
Apply freeInduction to the $0$-chain $z$.
On a generator $s$: path-connectedness joins $x_0$ to the support point of $s$, so exists_bnd_eq_sub yields a $1$-chain with boundary equal to that difference. Rewrite via constSimplex_pointOf, augFun_genUnit, and genUnit_eq to match the claimed formula.
On zero: take the zero $1$-chain; all maps vanish.
On sums: add the two witnessing $1$-chains and use additivity of $\partial$, $\mathrm{gen}$, and $\mathrm{aug}$, then cancel with abel.
On integer multiples: scale the witness and use mapSmul with smul_sub.
why it matters
This lemma is the chain-level engine behind isIso_homologyMap_augTo: the augmentation induces $H_0(X)\cong\mathbb{Z}$ on any path-connected space. Downstream that theorem quotes the existence of a bounding $1$-chain exactly in this form, then feeds a general criterion that a chain map inducing an iso on cycles modulo boundaries is a homology iso in degree zero.
In the Recognition foundation stack, low-degree singular homology of spheres and connected spaces underwrites the topological side of the forcing chain (contractibility, Mayer–Vietoris gluings, and the eight-tick discrete circle). Without a clean $H_0\cong\mathbb{Z}$ statement, later comparisons of discrete recognition complexes to continuous models lose their degree-zero anchor.
The result is fully proved (no sorry); it closes the path-connected case of the classical augmentation isomorphism inside the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.