rel
plain-language theorem explainer
Canonical projection from the singular chain complex of X onto the relative singular chains of the pair induced by f : A → X. Algebraic topologists building relative homology via singular chains cite this map as the third arrow of the pair short complex. Defined in one line as the cokernel projection of the chain map induced by f.
Claim. For a morphism $f : A \to X$, the map $\mathrm{rel}\pi(f)$ is the projection $C_*(X) \twoheadrightarrow C_*(X,A)$ of singular chain complexes, given by the cokernel projection of the induced chain map $C_*(A) \to C_*(X)$.
background
In the singular-pair foundation, a morphism $f : A \to X$ induces a chain map on singular chain complexes $C_(A) \to C_(X)$. The relative singular chain complex $C_*(X,A)$ is the cokernel of that map, so relative chains measure the failure of $f$ to be a chain-level equivalence.
The ambient module assembles the short complex $0 \to C_(A) \to C_(X) \to C_*(X,A) \to 0$ and the associated short exact sequence of complexes (siblings pairSES, pairSES_shortExact). Homological-complex infrastructure from Mathlib supplies cokernels and homology sequences.
Notation: $C_*(-)$ is written SC in-module; the relative complex is relSC f. The projection defined here is the third arrow of that short complex.
proof idea
One-line definition: apply the cokernel projection cokernel.π to the singular chain map induced by $f$ (written sChainMap f). No further lemmas or tactics; the type is SC X ⟶ relSC f by the universal property of the cokernel.
why it matters
Supplies the third arrow of the singular-pair short complex $0 \to C_(A) \to C_(X) \to C_*(X,A) \to 0$, which the module doc attaches to $f : A \to X$. Downstream siblings (pairSES, pairSES_shortExact, pairSES_degreewise_shortExact, pair) package that complex and prove degreewise short exactness, the standard gateway to the long exact sequence of the pair.
In the Recognition Science foundation layer this is pure algebraic-topology scaffolding: relative singular chains underpin pair and prism constructions used later in the forcing and recognition pipeline. It does not itself touch T0–T8, the J-cost, or $\varphi$; it only equips the chain-level pair language those layers may import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.