negApp
plain-language theorem explainer
Negating a morphism of abelian groups and then evaluating at a point is the same as evaluating and then negating. Homological algebraists cite it when chasing signs elementwise in singular chain complexes. The proof is a three-line rewrite through the underlying additive structure of ModuleCat morphisms.
Claim. Let $M,N$ be $\mathbb{Z}$-modules and $f:M\to N$ a module morphism. For every $x\in M$, $(-f)(x)=-(f(x))$.
background
The ambient module is singular chain groups valued in ModuleCat ℤ: morphisms are additive maps of abelian groups, and the category carries a pointwise negation on arrows. Evaluation of a morphism at an element is the underlying function of that arrow.
This file builds the Mayer–Vietoris short exact sequence of singular chain complexes for an open cover $U\cup V=X$. Exactness and homology long exact sequences are proved by elementwise diagram chases, so one needs the elementary identities that addition, subtraction, and negation of morphisms act pointwise on chains.
The lemma sits next to the companion identities for addition and subtraction of morphisms; together they let later arguments treat biproduct inclusions and boundary maps as ordinary group homomorphisms on generators.
proof idea
Reduce the goal to the underlying additive maps: show that the hom of $-f$ at $x$ equals the negation of the hom of $f$ at $x$. Rewrite by the library fact that negation of a ModuleCat morphism is pointwise negation of its underlying map, then close by reflexivity.
why it matters
Elementwise sign control is required throughout the singular Mayer–Vietoris development. Downstream, subApp builds subtraction of morphisms from this lemma plus the addition identity; mvSESdeg_exact uses those identities when verifying exactness of the degree-$n$ Mayer–Vietoris short complex; and bounds_of_mv (arc-complement acyclicity) quotes the same toolkit to conclude that a 1-cycle of $U\cap V$ whose pushforwards bound in $U$ and in $V$ already bounds in the intersection, once $H_2(X)=0$.
In the Recognition foundation stack this is pure scaffolding for singular homology of spheres and arc complements, not a physics claim. It does not touch the forcing chain (T0–T8), the J-cost, or the eight-tick octave; it only keeps the algebraic topology layer free of ad-hoc sign lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.