eq_zero_of_isZero
plain-language theorem explainer
In the category of abelian groups (as R-modules), every concrete element of a zero object is the zero vector. Homological algebraists cite it to turn a vanishing homology group into an elementwise statement that cycles bound. The proof equates the identity endomorphism with the zero morphism and evaluates both on the element.
Claim. Let $M$ be a zero object in $\mathbf{Mod}_{\mathbb{Z}}$. Then for every element $x$ of the underlying abelian group of $M$, one has $x = 0$.
background
The ambient setting is chain complexes of $\mathbb{Z}$-modules in Mathlib's ModuleCat, used to compute singular homology of topological spaces. A zero object $M$ is both initial and terminal: the unique endomorphism $M \to M$ is simultaneously the identity and the zero morphism.
The module builds an elementwise homology-class toolkit: cycles live in short complexes $K.X(n+2)\to K.X(n+1)\to K.X(n)$, and homology is the honest quotient $\ker/\mathrm{range}$. Vanishing of a homology object is therefore a categorical IsZero hypothesis on that quotient module.
This lemma converts that categorical hypothesis into a statement about underlying elements, which is what later bounds and Mayer–Vietoris arguments need.
proof idea
From IsZero M, the source-uniqueness clause gives $\mathrm{id}_M = 0$ as morphisms $M\to M$. A short calculation then runs: $x = \mathrm{id}_M(x)$ by the module-category identity law, rewrite the identity to the zero morphism, and apply the zero-morphism evaluation rule to conclude $x=0$. Three rewrites, no induction.
why it matters
Parent lemmas are bounds_of_isZero ("a vanishing $H_1$ makes every cycle bound") and bounds_of_mv (elementwise Mayer–Vietoris injectivity at $H_1(U\cap V)$ under $H_2(X)=0$). Both reduce a homology class being zero to an existence of a bounding chain; this lemma discharges the class-equals-zero step once the homology object is known to be a zero object.
In the Recognition Science foundation stack, arc-complement acyclicity is the topological input that forces low-dimensional vanishing used downstream in the forcing chain (spatial dimension and octave structure). The lemma itself is pure homological algebra, but it is the elementwise hinge those topological vanishing theorems turn on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.