relSC
plain-language theorem explainer
Defines the relative singular chain complex C_*(X,A) as the cokernel of the singular chain map induced by a continuous map f : A → X. Algebraic topologists and anyone building relative homology in the RS foundation cite this as the working object. The body is a one-line cokernel construction on the induced chain map.
Claim. For a continuous map $f : A \to X$ of topological spaces, the relative singular chain complex $C_*(X,A)$ is the cokernel of the induced map of singular chain complexes $C_*(A) \to C_*(X)$. Degreewise this is the quotient $C_n(X)/C_n(A)$ with the induced differential.
background
In singular homology one associates to a space $X$ its singular chain complex $C_(X)$ with coefficients in $\mathbb{Z}$-modules. A continuous map $f : A \to X$ induces a chain map $C_(A) \to C_(X)$ (here written via the singular-chain functor). The relative complex is the standard cokernel of that map, so that degreewise one recovers the quotient modules $C_n(X)/C_n(A)$ with the differential descended from $C_(X)$.
The ambient module is SingularPair, which packages pairs of spaces and the short exact sequence of chain complexes that feeds relative homology. The upstream abbreviation for the induced chain map is the image of $f$ under the singular chain complex functor valued in chain complexes of $\mathbb{Z}$-modules. The two unrelated constants named $A$ in GapDerivation and Masses.Anchor (active edges per tick) are not used as data here; the parameter $A$ is simply the domain space of $f$.
proof idea
One-line definition: apply the cokernel of the chain complex category to the singular chain map induced by $f$. No further lemmas are invoked at the definition site; well-definedness of the induced differential is inherited from the cokernel of a chain map in an abelian category of complexes.
why it matters
This is the working relative complex for the pair formalism in the foundation layer. Downstream, the identity case is shown to be the zero complex, and relative homology of the identity pair vanishes in every degree, locking the cokernel semantics. The same object supplies the projection $C_(X) \to C_(X,A)$ and the connecting data used to build the pair short exact sequence and the relative boundary. In the broader RS stack this is scaffolding for topological invariants of recognition pairs rather than a forcing-chain step (T5–T8); it sits under the singular-prism and pair machinery that later interfaces with discrete octave and gap structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.