exists_nonbounding
plain-language theorem explainer
If the first singular homology of a space W is nonzero, some 1-cycle fails to bound. Algebraic topologists cite this when converting a homology obstruction into an explicit nonbounding chain. The proof extracts a nonzero class, represents it by a cycle, and applies the vanishing criterion so a boundary would force the class to zero.
Claim. Let $W$ be a topological space. If $H_1(W;\mathbb{Z})$ is not the zero module, then there exists a singular $1$-chain $z$ with $\partial z = 0$ that is not a boundary: no $2$-chain $w$ satisfies $z = \partial w$.
background
The module works in singular homology with integer coefficients on spaces in TopCat. Chain groups $C_n(W)$ are the coproduct presentation of singular $n$-chains; the boundary maps $\partial$ are those of the singular chain complex $SC(W)$. Homology $H_1(W)$ is written $Hgrp,W,1$.
Two local facts organize the argument. Representability says every homology class is the class of some cycle. The vanishing criterion says that class is zero if and only if the cycle is a boundary. Together they turn a nonzero $H_1$ element into a concrete nonbounding cycle.
The surrounding development supports arc-complement acyclicity in the sense of Hatcher 2B.1: complements of embedded arcs in spheres should have vanishing $H_1$. This lemma is the contrapositive engine used when a nonzero $H_1$ must be ruled out.
proof idea
From $\neg\mathrm{IsZero}(H_1(W))$, obtain a nonzero homology element $h$ by contradiction: if every element were zero the module would be a subsingleton, hence zero in ModuleCat. Apply representability (exists_classOf) to $h$ on $SC(W)$ to get a cycle $z$ with $\mathrm{classOf}(z)=h$. The cycle condition is $\partial z=0$. If $z$ bounded, the vanishing criterion (classOf_eq_zero_iff) would force $\mathrm{classOf}(z)=0$, contradicting $h\neq 0$. Package $z$ as the required witness.
why it matters
Feeds the main theorem arcComplementsAcyclic: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$ (Hatcher 2B.1, arc case). That proof proceeds by contradiction on a nonzero $H_1$ of the complement; this lemma supplies the nonbounding cycle that the geometric argument then excludes.
In the Recognition foundation layer, arc-complement acyclicity is part of the topological scaffolding around linking and high-dimensional vanishing used to lock spatial structure. It sits upstream of dimension and linking constraints rather than of the T5–T8 forcing identities themselves, but it is the formal bridge from singular homology language to the geometric non-linking statements the framework needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.