intModuleCat_not_isZero
plain-language theorem explainer
The free rank-one module ℤ is not a zero object in the category of ℤ-modules. Anyone transferring nonvanishing of H₁(S¹; ℤ) along an isomorphism to ℤ cites this fact. The proof assumes a zero object, forces Hom(ℤ,ℤ) to be a singleton so id equals the zero map, and evaluates at 1 to obtain 1 = 0.
Claim. In the category of modules over $\mathbb{Z}$, the object $\mathbb{Z}$ is not a zero object: $\neg\,\mathrm{IsZero}(\mathrm{Mod}_{\mathbb{Z}}(\mathbb{Z}))$.
background
This module is the Mathlib cohomology bridge contract for Recognition Science. Mathlib already exposes the singular homology functor API, but the T8 replacement (forcing three spatial dimensions) needs a Mathlib-backed computation of the reduced cohomology of the circle S¹, together with an Alexander-duality bridge from circle-complement homology. The module records the exact backend objects required and deliberately does not fake them by reusing an internal nontriviality lemma.
A zero object in a pointed category is both initial and terminal: there is a unique morphism to and from every object. In ModuleCat ℤ the zero object is the zero module. The free module on one generator is ModuleCat.of ℤ ℤ. Nonvanishing of that object is the elementary algebraic fact needed once homology is identified with ℤ.
Downstream, nonvanishing of H₁(S¹; ℤ) is obtained by transporting along an isomorphism to ℤ; the present lemma discharges the algebraic half of that transport.
proof idea
Proof by contradiction. Assume IsZero (ModuleCat.of ℤ ℤ). Then the unique-morphism property supplies a Unique instance on endomorphisms of that object. Subsingleton elimination equates the identity morphism with the zero morphism. Congruence on the underlying ModuleCat.Hom.hom yields equality of ℤ-linear maps ℤ → ℤ, and evaluating both sides at 1 produces 1 = 0, which norm_num refutes.
why it matters
Parent use is circleH1ZNonzero_of_iso_int: if H₁(S¹; ℤ) is isomorphic to ℤ as a ℤ-module, then it is not a zero object. That nonvanishing is the required target for the Mathlib-backed circle computation that replaces the concrete S¹ cohomology encoding in the T8 dimension-forcing chain (eight-tick octave and D = 3). Without this elementary fact, an isomorphism to ℤ would not close the nonvanishing obligation. The lemma is pure category-of-modules algebra; the geometric content lives in the iso hypothesis and in the singular-homology API availability markers in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.