toSSet_map_app_injective
plain-language theorem explainer
An injective continuous map of spaces induces an injective map on singular n-simplices: postcomposition with an injective map stays injective. Algebraic topologists building relative singular chains or Mayer–Vietoris sequences cite this when they need monicity of the induced simplicial map. The proof reduces injectivity of the simplicial component to injectivity of the underlying continuous map via the objectwise equivalence to continuous maps out of the standard simplex.
Claim. Let $f\colon A\to X$ be a continuous map of topological spaces whose underlying function is injective, and let $n\in\mathbb{N}$. Then the induced map on singular $n$-simplices, $(|\Delta^n|\to A)\mapsto(f\circ -)$, is injective.
background
The module develops singular pairs $(A,X)$ with $A\hookrightarrow X$, aiming at relative singular chain complexes and a short exact sequence of chain complexes. Singular $n$-simplices of a space $Y$ are continuous maps $|\Delta^n|\to Y$; the singular simplicial set functor TopCat.toSSet packages them, and evaluation at the opposite of the simplex category object $\Delta[n]$ recovers the set of $n$-simplices.
An upstream equivalence toSSetObjEquiv identifies those simplices with continuous maps out of the geometric $n$-simplex. The induced map on simplicial sets acts by postcomposition: a simplex $\sigma$ of $A$ is sent to $f\circ\sigma$. The companion lemma toSSetObjEquiv_map records that this postcomposition intertwines with that equivalence. The chain map chainMap f n of SingularPrism is the free abelian group on the same data, so monicity at the simplex level is the first step toward monicity of chain maps.
proof idea
Tactic proof. Fix two singular $n$-simplices $a,b$ of $A$ with the same image under the induced simplicial map. Transport across toSSetObjEquiv_map to obtain equality of the continuous composites $f\circ\sigma_a=f\circ\sigma_b$. Pointwise evaluation plus injectivity of $f$ yields $\sigma_a=\sigma_b$ as continuous maps. Injectivity of the equivalence toSSetObjEquiv then forces $a=b$. No homology or freeness is used; the argument is pure set-level postcomposition.
why it matters
This is the monicity engine for the singular-pair apparatus. Downstream, gen_comp_genRetract uses it to build a retraction of the degree-$n$ chain map on generators when $f$ is injective, splitting chainMap f n on free generators. Independently, SingularMayerVietoris.pushIdx_injective instantiates it on subspace inclusions to get injectivity of the push of index sets, which feeds the Mayer–Vietoris comparison for singular chains.
In the Recognition Science foundation layer this sits under the singular-homology scaffolding that supports geometric and topological forcing arguments (octave structure, spatial dimension). It does not itself invoke the J-cost, $\varphi$, or the T0–T8 chain; it is pure topological infrastructure those later arguments rely on when they need relative or excised singular chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.