chainMap_mono
plain-language theorem explainer
An injective continuous map of spaces induces an injective map on singular n-chains for every degree n. Algebraic topologists cite this when building relative pairs and Mayer–Vietoris sequences over ℤ. The proof is a one-line appeal to a left inverse: the chain map splits, so it is mono.
Claim. Let $f\colon A\to X$ be a continuous map of topological spaces whose underlying function is injective. Then for every $n\in\mathbb{N}$, the induced map $C_n(A;\mathbb{Z})\to C_n(X;\mathbb{Z})$ on singular $n$-chains is a monomorphism of abelian groups.
background
The ambient setting is the singular chain complex of a space in TopCat, valued in ModuleCat ℤ, written degreewise via the coproduct presentation Cgrp X n of free ℤ-modules on singular simplices. The degree-$n$ chain map induced by a continuous map $f$ is the component of the image under the singular-chain-complex functor.
Injectivity of continuous maps does not automatically give monomorphisms of chain groups without a concrete section on generators. Upstream, chainMap_comp_genRetract records that when $f$ is injective on points, the induced chain map admits a left inverse genRetract in each degree: the composite is the identity on $C_n(A)$. That splitting is the only nontrivial input here.
Locally the module develops relative pairs $(X,A)$ and the short exact sequence of chain complexes that feeds relative homology and Mayer–Vietoris.
proof idea
One-line term proof. Apply mono_of_mono_fac to the equality chainMap f n ≫ genRetract f n = 𝟙 from chainMap_comp_genRetract. Any morphism with a left inverse is a monomorphism, so the degree-$n$ chain map is mono.
why it matters
This is the degreewise engine behind sChainMap_mono, which lifts the statement to a monomorphism of singular chain complexes. That complex-level mono is what makes the relative complex well-behaved: downstream, relative_homology_id_isZero uses the pair machinery to prove $H_n(X,X)=0$, locking the cokernel semantics of relative chains.
It is also invoked directly in mvSESdeg_mono inside SingularMayerVietoris: inclusions of an intersection into the open sets are injective, so the corresponding chain maps are mono and the biproduct lift that starts the Mayer–Vietoris short exact sequence is mono in each degree.
In the Recognition foundation stack this is pure singular-homology scaffolding (not a T0–T8 forcing step), but it is required infrastructure for any later identification of topological invariants with RS discrete structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.