pairSES
plain-language theorem explainer
Packages the singular-chain short complex 0 → C_*(A) → C_*(X) → C_*(X,A) → 0 attached to a continuous map f : A → X as a Mathlib ShortComplex of ℤ-module chain complexes. Anyone proving relative homology exactness or the long exact sequence of a pair cites this object. Construction is a three-argument ShortComplex.mk from the induced chain map, the relative projection, and the cokernel zero-composition identity.
Claim. Given a continuous map $f : A \to X$ of topological spaces, form the short complex $0 \to C_*(A) \xrightarrow{f_\#} C_*(X) \xrightarrow{\pi} C_*(X,A) \to 0$ of singular chain complexes with coefficients in $\mathbb{Z}$, where $f_\#$ is the induced singular chain map and $\pi$ is the canonical projection onto the relative singular chains (realized as the cokernel of $f_\#$).
background
In singular homology, a continuous map $f : A \to X$ induces a chain map $f_# : C_(A) \to C_(X)$ on free $\mathbb{Z}$-modules generated by singular simplices. The relative complex $C_(X,A)$ is the cokernel of that map, so the composite $C_(A) \to C_(X) \to C_(X,A)$ is zero by construction.
The module sits in the Foundation singular-pair development: singular chain complexes are obtained from Mathlib's singular-chain-complex functor on TopCat, and sChainMap f is the induced map of those complexes. The relative projection relπ f is the cokernel projection of that chain map.
The short-complex packaging is the standard Mathlib carrier for later exactness and homology-sequence arguments; exactness itself is not claimed here and requires injectivity of $f$ on underlying points.
proof idea
Definitional construction only: ShortComplex.mk is applied to three data. The first arrow is sChainMap f (singular chain map induced by $f$). The second is relπ f (projection of $C_*(X)$ onto the relative complex). The zero-composition witness is the universal cokernel condition cokernel.condition _, which states that $\pi \circ f_# = 0$. No tactics or lemmas beyond that identity.
why it matters
This is the carrier object for the classical short exact sequence of a pair in singular homology inside the Recognition Science foundation layer. Downstream, pairSES_shortExact proves the complex is short exact whenever $f$ is injective on points; pairSES_degreewise_shortExact unpacks that degreewise; and subpair_shortExact specializes to subspace inclusions $S \hookrightarrow X$.
Those exactness lemmas feed the long exact sequence of a pair and the sanity identity $H_n(X,X)=0$. In the broader RS stack this is pure topological scaffolding (singular chains, relative homology), not a forcing-chain step (T5–T8) or a constants claim; it supplies the homological language used when geometric or ledger constructions are compared via continuous maps of spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.