comp_pair
plain-language theorem explainer
The composite of the degree-(n+1) homology map induced by the relative projection X → (X,A) with the connecting homomorphism ∂ of the pair is zero. Anyone assembling the long exact sequence of a singular pair cites this annihilation. The proof is a one-line call to Mathlib's short-exact connecting-map identity on the pair SES.
Claim. Let $f:A\to X$ be a chain map that is injective on underlying modules, and let $n\in\mathbb{N}$. Write $\pi$ for the relative projection out of $X$ and $\partial_n$ for the connecting homomorphism of the pair. Then the composite $H_{n+1}(X)\xrightarrow{\pi_*}H_{n+1}(X,A)\xrightarrow{\partial_n}H_n(A)$ is the zero map.
background
The module develops singular-pair homology: given an injective chain map $f:A\to X$, one forms the relative complex $(X,A)$, the short exact sequence of complexes $0\to A\to X\to(X,A)\to 0$, and the associated connecting maps on homology.
The relative projection $\mathrm{rel}\pi(f)$ induces maps on homology $H_{\bullet}(X)\to H_{\bullet}(X,A)$. The connecting homomorphism $\partial$ (here pairδ) lands in $H_{\bullet}(A)$. Standard homological algebra asserts that consecutive maps in the long exact sequence of a pair compose to zero; this lemma records one of those two annihilations.
Upstream, pairSES_shortExact packages the degreewise short exactness of the pair sequence under the injectivity hypothesis on $f$, so Mathlib's generic comp_δ applies.
proof idea
One-line term proof. Apply the Mathlib lemma ShortExact.comp_δ to the short exact sequence of complexes furnished by pairSES_shortExact f hf, at degrees $n+1$ and $n$, with the downward complex-shape witness ComplexShape.down_mk _ _ rfl. No extra diagram chase is required.
why it matters
In the Recognition Science foundation layer this is bookkeeping for singular-pair homology: the vanishing $H_{n+1}(X)\to H_{n+1}(X,A)\xrightarrow{\partial}0$ is half of the exactness package that lets relative cycles control absolute ones. It sits beside the sibling SES constructors (pairSES, pairSES_shortExact, pairSES_degreewise_shortExact) and the dual annihilation for the inclusion-induced map. No downstream consumers are wired yet in the graph, so the lemma is presently a local exactness brick rather than a cited step in the T0–T8 forcing chain. It does not itself force dimension, $\phi$, or the eight-tick octave; it only keeps the homological scaffolding coherent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.