cls_eq_zero_iff
plain-language theorem explainer
A 1-cycle on a space W represents the zero class in H₁ if and only if it is the boundary of some 2-chain. Algebraic topologists working the arc-complement vanishing lemmas cite this as the degree-1 specialization of the general homology vanishing criterion. The proof is a one-line wrapper applying that criterion to the singular chain complex of W at n = 0.
Claim. Let $W$ be a topological space and $z$ a singular $1$-chain with $\partial z = 0$. Then the homology class $[z] \in H_1(W;\mathbb{Z})$ vanishes if and only if there exists a singular $2$-chain $w$ with $z = \partial w$.
background
The module works in singular homology with integer coefficients on spaces in TopCat. Chain groups $C_n(W)$ are the free $\mathbb{Z}$-modules on singular $n$-simplices (coproduct presentation). The boundary $\partial : C_{n+1}(W) \to C_n(W)$ is the differential of the singular chain complex $SC(W)$.
Degree-1 homology classes of cycles are packaged by a thin wrapper: given $z \in C_1(W)$ with $\partial z = 0$, one forms $[z] \in H_1(W)$. The general vanishing criterion on an arbitrary chain complex states that the class of a cycle is zero exactly when the cycle is a boundary. That criterion is the upstream engine; the present lemma specializes it to singular homology in degree 1.
Local setting is the arc-complement acyclicity development: one needs an elementwise dictionary between "$[z]=0$ in $H_1$" and "exists a 2-chain bounding $z$" before pushing vanishing of $H_1$ through Mayer–Vietoris and open covers.
proof idea
One-line wrapper. Instantiate the general vanishing criterion classOf_eq_zero_iff on the singular chain complex $SC(W)$ at $n=0$, feeding the given 1-cycle $z$ and the hypothesis $\partial z=0$. The degree-1 class wrapper is definitionally that same classOf instance, so the biconditional transfers verbatim: $[z]=0$ iff $z$ is a boundary from degree 2.
why it matters
Feeds two parent results in the same module. First, bounds_of_isZero: if $H_1(W)=0$, every 1-cycle bounds; the proof applies the forward direction of this iff after forcing the class to zero by the zero-object property. Second, bounds_of_mv, the elementwise Mayer–Vietoris injectivity statement at $H_1(U\cap V)$: with $H_2(X)=0$, a 1-cycle of the intersection whose pushforwards bound in $U$ and in $V$ must itself bound; the criterion converts class-level vanishing back into an explicit bounding 2-chain.
In the Recognition foundation layer this is plumbing, not a forcing-chain landmark (T5–T8). It underwrites the topological half of the arc-complement story used when singular homology controls connectivity and linking data that later touch mass-topology and conditional-slot scaffolding. No open sorry sits on this lemma; it closes the degree-1 dictionary so the MV and zero-homology corollaries can stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.