subApp
plain-language theorem explainer
Elementwise, the difference of two morphisms of abelian groups acts as the difference of their values: $(f-g)(z)=f(z)-g(z)$. Anyone computing singular boundaries or Mayer–Vietoris maps in this library cites it. The proof is a three-step rewrite through add-and-neg application lemmas.
Claim. Let $M,N$ be $\mathbb{Z}$-modules and $f,g:M\to N$ module morphisms. For every $z\in M$, $(f-g)(z)=f(z)-g(z)$.
background
The ambient setting is singular homology of topological spaces, formalized with chain groups as objects of ModuleCat over $\mathbb{Z}$. Morphisms are applied to elements via the underlying hom, so algebraic identities on morphisms must be re-proved at the pointwise level before they can be used in boundary calculations.
Two sibling lemmas already record the additive structure pointwise: $(f+g)(x)=f(x)+g(x)$ and $(-f)(x)=-(f(x))$. Subtraction is defined as $f-g=f+(-g)$, so the difference identity is the remaining piece of the abelian-group action on elements.
The module sits in the singular-sphere development, which builds generators, constant simplices, path simplices, and their boundaries toward homology of spheres and related Recognition foundations.
proof idea
Rewrite $f-g$ as $f+(-g)$ via sub_eq_add_neg. Apply the pointwise sum lemma addApp, then the pointwise negation lemma negApp. Rewrite the resulting $f(z)+(-(g(z)))$ back to $f(z)-g(z)$. No new category theory is needed; it is pure transport of the ring operations on homs to evaluation.
why it matters
The immediate consumer is the elementwise boundary of a path simplex: $\partial(\mathrm{genUnit}(\mathrm{pathSimplex},\gamma))$ equals the difference of the two endpoint constant 0-simplices. That identity needs $(f-g)(1)=f(1)-g(1)$ on the generator maps, which is exactly this lemma.
In the broader Foundation stack (singular pairs, prisms, subdivision, Mayer–Vietoris), such pointwise arithmetic is the glue between abstract chain maps and concrete geometric generators. It does not itself touch the forcing chain T0–T8 or the J-cost, but it keeps the singular-homology scaffolding that later geometric Recognition arguments rely on free of sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.