zeroApp
plain-language theorem explainer
The zero morphism of abelian groups (as objects of ModuleCat over ℤ) evaluates to the zero element at every point. Anyone writing elementwise identities for singular chain maps, homology maps in degree 0, or vanishing on zero objects cites this. The proof unwraps the ModuleCat arrow to its underlying linear map and applies the library fact that the zero arrow is the zero map.
Claim. For $\mathbb{Z}$-modules $M,N$ (viewed as objects of the category of modules) and any $x\in M$, the zero morphism $0:M\to N$ satisfies $0(x)=0$.
background
The ambient setting is singular chain complexes valued in ModuleCat ℤ: free abelian groups on singular simplices, with the usual face-boundary differentials. Morphisms of complexes are degreewise module maps, and many identities (homotopies, subdivision operators, augmentations) are checked by evaluating those maps on generators or on arbitrary chains.
In Mathlib, a morphism $f:M\to N$ in ModuleCat is a bundled linear map; applying it to an element is f.hom x (or the category application sugar). The zero morphism is the zero linear map. This lemma packages the elementary fact that evaluation of that zero arrow is literally the zero vector, so later proofs can rewrite (0 : M ⟶ N) x without unpacking the category structure each time.
The module sits inside the singular Mayer–Vietoris development: small-span subcomplexes for an open cover, prism/subdivision homotopies, and degree-0 homology criteria that repeatedly meet zero arrows and zero objects.
proof idea
Term/tactic hybrid, three steps. First rephrase the goal as evaluation of the underlying linear map of the zero arrow. Then rewrite by ModuleCat.hom_zero, which identifies that underlying map with the zero map of modules. The resulting 0 x = 0 is definitional (rfl). No Recognition-specific lemmas are used; it is pure ModuleCat plumbing.
why it matters
Tiny but heavily reused. Downstream, eq_zero_of_isZero reduces vanishing on a zero object to id = 0 plus this evaluation fact. Inside the same Mayer–Vietoris file it appears in the telescoped homotopy membership proof (tOpIter_mem_smallSpan at the zero iterate) and supports the degree-0 epi/iso criteria for homologyMap that drive the MV long exact sequence. On the sphere side it discharges the empty-support branch of the augmentation on a generator (augFun_genUnit) and feeds injectivity/non-vanishing lemmas for the fundamental class.
In the Recognition foundation stack this is infrastructure, not a forcing-chain step: it keeps singular homology computations honest so later continuum-bridge and ledger arguments can quote acyclicity and $H_0$ facts without category-theoretic friction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.