classOf_eq_zero_iff
plain-language theorem explainer
A cycle represents the zero homology class exactly when it is a boundary. Arc-complement and linking arguments cite this as the dictionary between abstract vanishing of H_{n+1} and existence of a filling chain one degree up. The proof unfolds the class construction through short-complex isomorphisms and reduces to the submodule-quotient range criterion.
Claim. Let $K$ be a chain complex of modules, $n\in\mathbb{N}$, and $z\in K_{n+1}$ a cycle ($d_{n+1}(z)=0$). Writing $[z]$ for its class in $H_{n+1}(K)$, one has $[z]=0$ if and only if there exists $w\in K_{n+2}$ with $z=d_{n+2}(w)$.
background
The ambient module builds singular and abstract chain complexes for arc-complement acyclicity (importing the high-dimensional linking-vanishing layer). Homology of $K$ is realized via Mathlib short complexes: at each degree one forms the three-term complex $K_{n+2}\to K_{n+1}\to K_n$, takes its left homology, and transports back along a canonical isomorphism scIso from the complex's native short complex to that honest-index triple.
The map sending a cycle $z$ (with $d(z)=0$) to its class is defined by quotienting $\langle z\rangle$ in the cycle submodule and pushing the class through the homology isomorphisms of that short complex. Upstream, any module isomorphism $e:M\cong N$ satisfies $e(x)=0\Leftrightarrow x=0$, so zero-detection is invariant under the transport used to define classes.
Locally this is pure homological algebra: no topology yet. Topology enters only when $K$ is specialized to singular chains of a space.
proof idea
Two preliminary facts: applying either the short-complex homology isomorphism or the module-category left-homology isomorphism sends an element to zero iff the element itself is zero (both instances of the iso zero-detection lemma). Unfold the class map, rewrite by those two equivalences, then by the standard facts that a quotient class is zero iff the representative lies in the submodule and that membership in the image of $d$ is exactly being a boundary. The two directions of the biconditional are then pure subtype extensionality between the abstract witness and the underlying chain $w$.
why it matters
This is the vanishing criterion named in the doc-comment: class zero iff boundary. It is the algebraic engine under the topological specializations in the same module. Downstream, the degree-1 singular form restates it for chain groups of a space $W$, and the nonbounding-cycle existence lemma uses it contrapositively: if $H_1(W)$ is not the zero object then some cycle is not a boundary.
In the Recognition foundation stack this supports arc-complement acyclicity and the linking-vanishing results that feed higher forcing and dimensional arguments. It does not itself invoke T5–T8 or the RCL; it is infrastructure those geometric claims rely on when they reduce topology to homology vanishing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.