mapSmul
plain-language theorem explainer
Morphisms of ℤ-modules in ModuleCat preserve integer scalar multiplication pointwise: φ(c · x) = c · φ(x). Homological algebra in the singular Mayer–Vietoris development cites this constantly when pushing scalars through chain maps. The proof is a one-line appeal to the underlying AddCommGroup linear map’s map_smul.
Claim. For $\mathbb{Z}$-modules $M,N$ viewed in $\mathbf{Mod}_{\mathbb{Z}}$, any morphism $\varphi:M\to N$, any $c\in\mathbb{Z}$, and any $x\in M$, one has $\varphi(c\cdot x)=c\cdot\varphi(x)$.
background
The module SingularMayerVietoris builds the singular Mayer–Vietoris short exact sequence for an open cover $U\cup V=X$, working throughout in ModuleCat ℤ (the category of abelian groups as ℤ-modules). Singular chains, small spans, inclusions sInc, and free-module coordinate projections are all morphisms in that category.
A morphism $\varphi:M\to N$ in ModuleCat ℤ is a bundled linear map. Lean’s carrier coercion can make direct map_smul instance search fragile on those carriers, so the development states ℤ-linearity elementwise through the underlying map φ.hom.
This lemma is the scalar half of that elementwise linearity (additivity is handled separately). Downstream coordinate lemmas such as coordAt_smul and free-induction arguments on chain groups rely on being able to slide integers past every chain map.
proof idea
One-line term proof: apply φ.hom.map_smul c x, i.e. the map_smul field of the underlying ℤ-linear map of the ModuleCat morphism. No further rewriting or instance gymnastics.
why it matters
Inside the Recognition foundation stack this is plumbing, not a physical claim, but it is load-bearing for the singular Mayer–Vietoris exactness path. It is used by coordAt_smul, coordAt_map_eq, coordAt_map_notMem, exists_sInc_eq, exists_sdOpIter_mem_smallSpan, mv_middle_exact, and mvSESdeg_epi in the same module, and by compact-support lifting exists_chain_lift in ArcComplementAcyclic.
Those results assemble the middle exactness of the Mayer–Vietoris sequence for singular chains and the subdivision arguments that put every chain into the small span of an open cover. That homological toolkit underpins later acyclicity and covering arguments in the foundation layer; without clean scalar naturality the free-module inductions and coordinate tracking break.
No forcing-chain landmark (T5–T8, RCL, φ) is stated here; the lemma is categorical infrastructure those geometric arguments sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.