coordAt_smul
plain-language theorem explainer
Scalar multiplication by an integer passes through the coordinate projection on the direct sum ∐_κ ℤ. Anyone tracking integer coefficients of free singular chains under linear maps cites this. The proof unfolds the coordinate definition, applies ModuleCat morphism ℤ-linearity, and finishes with the DFinsupp scalar action on components.
Claim. For every index $j \in \kappa$, every integer $c \in \mathbb{Z}$, and every element $x$ of the coproduct $\coprod_{\kappa} \mathbb{Z}$ (viewed in $\mathbf{Mod}_{\mathbb{Z}}$), the $j$-th coordinate satisfies $\mathrm{coord}_j(c \cdot x) = c \cdot \mathrm{coord}_j(x)$.
background
In the singular Mayer–Vietoris setup one works with free $\mathbb{Z}$-modules on index sets of singular simplices, presented as categorical coproducts $\coprod_{\kappa} \mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$. The coordinate map $\mathrm{coordAt}, i$ extracts the $i$-th integer coefficient by transporting along the isomorphism from the ModuleCat coproduct to the algebraic direct sum, then reading the DFinsupp component at $i$.
Because morphisms in ModuleCat are linear maps, scalar multiplication by $c \in \mathbb{Z}$ is natural. The auxiliary lemma mapSmul records that elementwise: for any ModuleCat arrow $\varphi$, one has $\varphi(c \cdot x) = c \cdot \varphi(x)$, stated through the underlying linear map to avoid carrier-instance noise.
The local module builds the singular Mayer–Vietoris exact sequence from small chains, inclusions, and subdivisions; coordinate bookkeeping on free generators is the algebraic engine behind those comparisons.
proof idea
Term-mode, three steps. Unfold coordAt to expose the composite of the coproduct-to-direct-sum isomorphism with DFinsupp evaluation at $j$. Rewrite the scalar through that morphism via mapSmul (ModuleCat $\mathbb{Z}$-linearity). Conclude by the standard identity DFinsupp.smul_apply, which says scalar multiplication on a direct sum acts componentwise.
why it matters
This is the scalar half of $\mathbb{Z}$-linearity for coordinate projections. Downstream, coordAt_map_eq and coordAt_map_notMem track coordinates through basis-index maps on free chains: the former says that at an image index of an injective reindexing the coordinate is preserved, the latter that coordinates outside the image vanish. Both proofs induct on free generators and need scalars to pass the induction step cleanly.
In the Recognition foundation stack those tracking lemmas underwrite the singular Mayer–Vietoris comparison for small chains and subdivisions, which is the algebraic backbone for the eight-tick / octave forcing material (T7) once singular homology enters the geometric side of the forcing chain. The lemma itself is pure homological algebra; its place is as a reusable coefficient identity rather than a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.