id_int_ne_zero
plain-language theorem explainer
The identity endomorphism of ℤ, as an object of ModuleCat over ℤ, is not the zero morphism. Homological algebraists working with singular chains or Mayer–Vietoris over ℤ cite it to turn a split monomorphism out of ℤ into a concrete non-vanishing statement. The proof is a three-line evaluation at 1, using id_apply, zeroApp, and 1 ≠ 0.
Claim. In the category of $\mathbb{Z}$-modules, the identity morphism $\mathrm{id}:\mathbb{Z}\to\mathbb{Z}$ is not equal to the zero morphism.
background
SingularSphere assembles singular-homology toolkit for the Recognition foundation: constant simplices, augmentation, path simplices on $\Delta^1\simeq I$, and the surrounding Mayer–Vietoris and subdivision infrastructure imported from SingularMayerVietoris, SingularSubdivision, SingularPair, and SingularPrism.
Morphisms are arrows in ModuleCat of $\mathbb{Z}$-modules. The zero arrow evaluates to the zero element at every point (zeroApp). Separately, the primitive calculus records that the generator $1\in\mathbb{Z}$ is not zero (one_ne_zero).
The present lemma is the elementary bridge between those two facts: it certifies that the identity on $\mathbb{Z}$ itself is a non-zero arrow, so any retract of that identity is likewise non-zero.
proof idea
Proof by contradiction. Assume $\mathrm{id}_{\mathbb{Z}}=0$ as morphisms in ModuleCat. Evaluate both sides at $1:\mathbb{Z}$. Rewrite the assumed equality, then apply ModuleCat.id_apply on the left and zeroApp on the right to obtain $1=0$. Discharge with one_ne_zero.
why it matters
Doc-comment states the intended use: convert split monomorphisms out of $\mathbb{Z}$ into non-vanishing statements. In the SingularSphere development this is the first non-vanishing seed before the Stage A path-simplex toolkit (homeomorphism $\Delta^1\simeq_t I$, constant simplices, augmentation). Non-vanishing of $\mathrm{id}_{\mathbb{Z}}$ is the algebraic starting point for showing that singular homology of spheres is free of rank one in top degree, which feeds dimensional and connectivity arguments in the foundation layer. No downstream consumers are wired yet in the graph; the lemma sits as a reusable primitive for any later split-mono or retract argument over $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.