coordAt_map_eq
plain-language theorem explainer
Under an injective reindexing of free ℤ-summands and a module map sending basis units to basis units, the coordinate of an image chain at the image index equals the source coordinate. Algebraic topologists cite it when tracking singular chains through inclusions in a Mayer–Vietoris cover. The proof is free-module induction on units, zero, sums, and scalar multiples, using the coordinate calculus lemmas.
Claim. Let $\psi:\kappa\to\kappa'$ be injective, and let $F:\bigoplus_{\kappa}\mathbb{Z}\to\bigoplus_{\kappa'}\mathbb{Z}$ be a morphism of $\mathbb{Z}$-modules with $F(e_i)=e_{\psi(i)}$ for each basis unit $e_i$. Then for every $z\in\bigoplus_{\kappa}\mathbb{Z}$ and every index $i\in\kappa$, the coordinate of $F(z)$ at $\psi(i)$ equals the coordinate of $z$ at $i$.
background
The ambient module is the categorical coproduct $\coprod_{\kappa}\mathbb{Z}$ in ModuleCat, identified with the direct sum of copies of $\mathbb{Z}$. The coordinate functional at an index $i$ extracts the $i$-th component of a chain via the coproduct–direct-sum isomorphism: it is additive, $\mathbb{Z}$-homogeneous, vanishes at zero, and on the basis unit at $j$ returns $1$ if $i=j$ and $0$ otherwise.
This lives in the singular Mayer–Vietoris foundation layer: free $\mathbb{Z}$-modules on singular simplices (and on small/subdivided generators) are presented as such coproducts, so chain maps induced by continuous maps or inclusions act by reindexing basis units. The free-induction principle lets one prove identities on all chains by checking units, zero, addition, and scalar multiplication.
Upstream coordinate lemmas already record additivity, scalar compatibility, the unit evaluation formula, and vanishing at zero; the present statement lifts those to a basis-index map that is injective on indices.
proof idea
Proceed by free induction on the chain $z$.
On a basis unit at $i'$, apply the hypothesis that $F$ sends units to units, then the unit-coordinate formula on both sides; injectivity of $\psi$ turns the two indicator equalities into a single if_congr.
On zero, use that $F$ and the coordinate both kill zero. On a sum, push $F$ through addition and apply coordinate additivity, then the inductive hypotheses. On a scalar multiple, push $F$ through the scalar action and apply coordinate homogeneity, then the inductive hypothesis.
No further global structure is used: the argument is pure free-module bookkeeping.
why it matters
Middle exactness of the singular Mayer–Vietoris sequence needs to recover a chain on $U\cap V$ from a cancelling pair of chains on $U$ and $V$. That reconstruction compares coordinates of image chains under the inclusion-induced maps on free modules of singular simplices; this lemma guarantees that coordinates along the image of an injective index map are faithfully preserved, so support and coefficients can be read off on the intersection.
It is a local algebraic step inside the Foundation singular package (prism, pair, subdivision, then Mayer–Vietoris), not a physics forcing step. It does not itself invoke T0–T8, the Recognition Composition Law, or the $\varphi$-ladder; it supplies the chain-level exactness infrastructure those later geometric claims rely on when singular homology enters the recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.