chainMap_injective
plain-language theorem explainer
An injective continuous map of spaces induces an injective map on singular n-chains for every n. Algebraic topologists cite it when building Mayer–Vietoris inclusions and when proving arc-complement acyclicity. The proof is a short left-inverse argument: the general retract splits the chain map, so equality after the chain map implies equality of the original chains.
Claim. Let $f\colon A\to X$ be a continuous map of topological spaces that is injective on underlying points. Then for every $n\in\mathbb{N}$, the induced singular chain map $C_n(A)\to C_n(X)$ is injective as a map of abelian groups (equivalently, of $R$-modules in the module category).
background
The ambient module develops a singular Mayer–Vietoris toolkit for Recognition Science foundation work: singular chain complexes of spaces and subspaces, inclusions into small subcomplexes, and the factor maps needed for exact sequences. The chain map of a continuous map $f\colon A\to X$ is the usual free-abelian extension of post-composition of singular simplices by $f$.
Upstream, SingularPair supplies a general retract of that chain map whenever $f$ is injective on points: composing the chain map with the retract recovers the identity on $C_n(A)$. That splitting is the only nontrivial input. Nearby scaffolding tracks the forced spatial dimension $D=3$ and pre-temporal forcing stages, but this lemma itself is pure singular homology algebra.
Locally the result sits in the Subspaces section, immediately before the Stage-3 factor maps into the small subcomplex used by the Mayer–Vietoris diagrams.
proof idea
Assume two $n$-chains $a,b$ on $A$ become equal after the chain map of $f$. Apply the general retract of $f$ (from SingularPair) to both sides. Rewrite the resulting equality via composition in the module category, then invoke the splitting identity chainMap f n ≫ genRetract f n = id. Both sides reduce to $a$ and $b$ respectively, so $a=b$. The argument is a pure left-inverse injectivity check; no homology or subdivision is used.
why it matters
The lemma is the injectivity engine for the two subspace inclusions into the small MV subcomplex: both uInc_injective and vInc_injective reduce to it by composing with the small-complex inclusion and quoting injectivity of subspace inclusions. Downstream it supports arc-complement acyclicity (Hatcher 2B.1, arc case): every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$. That vanishing statement is the topological input to linking and higher-dimensional recognition constraints; in the RS forcing chain the spatial dimension is forced to $D=3$ (T8), so the arc case is the concrete geometric ingredient that later dimension-counting arguments rely on. The declaration is fully proved (no sorry), closing a routine but indispensable mono step in the singular MV pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.