coordAt_map_notMem
plain-language theorem explainer
If a free ℤ-module map F sends basis vectors along an index map ψ, then at any target index outside the image of ψ the coordinate of every image chain is zero. Used when extracting intersection-supported chains in singular Mayer–Vietoris. Proof is free-module induction on generators, zero, sums, and scalar multiples.
Claim. Let $\psi:\kappa\to\kappa'$ and let $F$ be a morphism of free $\mathbb{Z}$-modules on those index sets with $F(e_i)=e_{\psi(i)}$ for every basis vector $e_i$. If $t\in\kappa'$ satisfies $\psi(i)\neq t$ for all $i$, then for every chain $z$ one has $\mathrm{coord}_t(F(z))=0$.
background
The module SingularMayerVietoris builds the singular Mayer–Vietoris sequence for a cover $X=U\cup V$ in the Recognition foundation stack. Chains live in free $\mathbb{Z}$-modules indexed by singular simplices; the coproduct $\coprod_{i}\mathbb{Z}$ is the algebraic carrier, and coordAt t reads the integer coefficient at a fixed index $t$.
A morphism $F$ of such free modules is determined by where it sends basis units unitOf i. The hypothesis here is that $F$ is induced by a pure index map $\psi$: each generator goes to a single generator, with no extra coefficients. The lemma tracks coordinates under that pushforward.
Sibling facts in the same Coordinates section give the elementary rules: coordinates of units, zero, sums, and scalar multiples. Those rules are the induction steps used below.
proof idea
Induct on the free-module structure of $z$ via freeInduction.
- On a generator
unitOf i': apply the structure hypothesis $F(e_{i'})=e_{\psi(i')}$, thencoordAt_unitOf; the resulting indicator is false byht, so the coordinate is $0$. - On zero:
map_zeroandcoordAt_zero. - On a sum:
map_add,coordAt_add, inductively both summands vanish, thenadd_zero. - On a scalar multiple:
mapSmul,coordAt_smul, inductively the vector part vanishes, thensmul_zero.
No further lemmas are needed beyond the coordinate arithmetic already proved in-section.
why it matters
Feeds directly into mv_middle_exact, the heart of Mayer–Vietoris exactness: a pair of chains on $U$ and $V$ whose images cancel in the ambient complex must come from a chain on $U\cap V$. Coordinate vanishing outside the image of the inclusion-induced index maps is what forces support into the intersection.
In the Recognition foundation, singular MV is scaffolding for the topological side of the forcing chain (local-to-global gluing of recognition data on covers). Exactness at the middle term is the algebraic content that lets one reconstruct intersection data from cancelling open-set data. This lemma is a pure free-module bookkeeping step; without it the support argument in mv_middle_exact does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.