sChainMap_mono
plain-language theorem explainer
An injective continuous map $f:A\to X$ induces a monomorphism of singular chain complexes $C_*(A)\to C_*(X)$. Algebraic topologists cite it when assembling the short exact sequence of a pair. The proof is a one-line lift of the already-proved degreewise monomorphism via the standard HomologicalComplex criterion.
Claim. Let $f:A\to X$ be a continuous map of topological spaces whose underlying function is injective. Then the induced singular chain map $C_*(f):C_*(A)\to C_*(X)$ is a monomorphism in the category of chain complexes of $\mathbb{Z}$-modules.
background
The module builds relative singular homology for a continuous map $f:A\to X$ by treating $C_(X,A)$ as the cokernel of the induced chain map. The singular chain functor $C_$ (here sChainMap) sends a continuous map to a morphism of chain complexes of $\mathbb{Z}$-modules; degreewise it is free abelian on singular simplices, with the usual face differential.
Upstream, the degreewise statement is already available: an injective continuous map induces a monomorphism $C_n(A)\to C_n(X)$ in each degree (via a generating retract and a mono-of-factorization argument). The present lemma packages those degreewise monos into a single mono of chain complexes, which is exactly the input needed for short-exactness of $0\to C_(A)\to C_(X)\to C_*(X,A)\to 0$.
proof idea
One-line term proof. Apply HomologicalComplex.mono_of_mono_f: a chain-map morphism is mono iff each component is mono. Supply the family of components by the upstream lemma chainMap_mono f hf n, which already gives Mono (chainMap f n) from injectivity of the underlying continuous map. No new algebraic work is done here.
why it matters
This is the mono half of the pair short exact sequence. Downstream, pairSES_shortExact sets mono_f := sChainMap_mono f hf and concludes that $0\to C_(A)\to C_(X)\to C_*(X,A)\to 0$ is short exact for injective $f$. That SES is the algebraic engine for relative homology of pairs, including the sanity check that $H_n(X,X)=0$ (relative_homology_id_isZero).
In the Recognition foundation stack this sits in the singular-pair layer that interfaces topological input with chain-level exactness; it does not itself invoke the forcing chain (T5--T8) or the J-cost, but it is infrastructure those geometric layers can call when relative cycles appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.