chainMap_id
plain-language theorem explainer
The identity continuous map on a space induces the identity endomorphism of its singular chain groups in every degree. Algebraic topologists in the arc-complement acyclicity argument cite this when transporting boundaries along retractions or homeomorphisms. The proof is pure functoriality: the singular-chain functor sends id to id, then the degree-n component is the identity module map.
Claim. For any topological space $A$ and any $n \in \mathbb{N}$, if $C_n(A;\mathbb{Z})$ denotes the degree-$n$ singular chain group of $A$ with integer coefficients, then the chain map induced by $\mathrm{id}_A$ satisfies $C_n(\mathrm{id}_A)(x) = x$ for every $x \in C_n(A;\mathbb{Z})$.
background
The ambient module builds singular homology infrastructure for the arc-complement acyclicity argument in the Recognition foundation layer. Spaces are objects of TopCat (topological spaces as a category). The degree-$n$ singular chain group $C_n(A;\mathbb{Z})$ is the coproduct of one copy of $\mathbb{Z}$ per singular $n$-simplex of $A$.
The singular chain complex $SC(A)$ is the chain complex whose degree-$n$ term is that group. A continuous map $f:X\to Y$ induces a chain map $sChainMap(f):SC(X)\to SC(Y)$ via the singular-chain-complex functor; its degree-$n$ component is the module homomorphism chainMap f n between the coproduct presentations.
Upstream, sChainMap is exactly the image of $f$ under that functor, and chainMap is the degree-$n$ face of that morphism of complexes. The identity arrow $\mathbb{1}_A$ is the categorical identity in TopCat.
proof idea
Functoriality of the singular chain complex functor gives sChainMap(𝟙 A) = 𝟙(SC A) by CategoryTheory.Functor.map_id. Congruence on the degree-$n$ component of that equality of chain maps yields chainMap(𝟙 A) n = 𝟙(Cgrp A n). Rewriting with ModuleCat.id_apply evaluates the identity module map on $x$ and finishes.
why it matters
This is the identity case of naturality for singular chains, needed so that boundaries can be pulled back along retractions. Downstream, bounds_of_retract opens with the rewrite $z = chainMap(\mathbb{1}_A),1,z$ via the symmetric form of this lemma, then pushes a bounding chain forward along the section and back along the retraction. That lemma is the algebraic engine for showing that if a 1-cycle bounds after a continuous map that admits a left inverse, the original cycle already bounds.
In the Recognition foundation stack this sits under the arc-complement acyclicity development (imported from LinkingVanishingHighDim), which supports topological vanishing statements used in the forcing and linking arguments. It is pure algebraic topology scaffolding: no direct appeal to T5–T8, RCL, or the $\varphi$-ladder, but it underwrites the chain-level bookkeeping those geometric claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.