pair_les_exact
plain-language theorem explainer
For an injective continuous map of spaces A → X, the connecting map and induced map make H_{n+1}(X,A) → H_n(A) → H_n(X) exact in every degree. Algebraic topologists cite this as one third of the long exact sequence of a pair. The proof is a one-line appeal to homology exactness of the short exact sequence of singular chain complexes of the pair.
Claim. Let $f\colon A\to X$ be a morphism of topological spaces whose underlying map of points is injective, and let $n\in\mathbb{N}$. Then the short complex $H_{n+1}(X,A)\xrightarrow{\partial} H_n(A)\xrightarrow{f_*} H_n(X)$ is exact (kernel of $f_*$ equals image of the connecting homomorphism $\partial$).
background
The module builds the singular homology of a pair $(X,A)$ from an injective continuous inclusion $f\colon A\hookrightarrow X$. Singular chains on $A$ and $X$ form chain complexes; the relative complex is the quotient by the image of the induced chain map. The connecting homomorphism $\partial\colon H_{n+1}(X,A)\to H_n(A)$ is the usual boundary of the snake lemma (or of the homology long exact sequence of a short exact sequence of complexes).
A short exact sequence of chain complexes $0\to C_\bullet(A)\to C_\bullet(X)\to C_\bullet(X,A)\to 0$ is assembled earlier in the file (the pair SES). Mathlib supplies the general fact that any short exact sequence of complexes yields a long exact sequence in homology; the three consecutive exactness statements at $H_n(A)$, $H_n(X)$, and $H_{n+1}(X,A)$ are the local pieces of that LES.
The complex shape is the standard downward shape on $\mathbb{N}$ (degree drops by one under the differential), so the connecting map lands in degree $n$ from degree $n+1$.
proof idea
One-line term proof. Apply homology_exact₁ to the already-established short exactness of the pair SES (pairSES_shortExact f hf), at consecutive degrees $n+1$ and $n$, with the trivial witness that the downward complex shape relates those degrees. No extra diagram chase is written by hand; Mathlib's homology LES machinery does the work.
why it matters
This lemma is the first of the three exactness legs that assemble the long exact sequence of a pair in singular homology inside the Foundation layer. Downstream siblings in the same file record exactness at $H_n(X)$ and at $H_{n+1}(X,A)$; together they give the full LES used whenever relative homology must be related to absolute homology of subspace and ambient space.
In the broader Recognition Science stack this sits in pure topological scaffolding (singular chains, relative complexes, LES), not in the T0–T8 forcing chain or the J-cost calculus. It supplies standard homological infrastructure that later geometric or recognition constructions can quote without re-proving algebraic topology. No open RS physics claim is discharged here; the value is reusable exactness for pair inclusions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.