pair
plain-language theorem explainer
Defines the connecting homomorphism ∂ from relative singular homology H_{n+1}(X,A) to H_n(A) for an injective chain map A→X. Algebraic topologists and anyone building the long exact sequence of a pair cite it. The body is a one-line extraction of δ from the short exact sequence of singular chain complexes of the pair.
Claim. For an injective morphism $f:A\to X$ of singular chain complexes and any $n\in\mathbb{N}$, there is a connecting homomorphism $\partial:H_{n+1}(X,A)\to H_n(A)$ obtained from the short exact sequence of the pair.
background
In the singular-pair module one works with singular chain complexes $SC(-)$ and the relative complex $\mathrm{relSC}(f)$ of an injective chain map $f:A\to X$. The relative homology $H_{n+1}(X,A)$ is the homology of that relative complex.
A short exact sequence of chain complexes (the pair SES) yields, by the standard snake-lemma construction in homological algebra, a connecting map $\delta$ between consecutive homology groups. Mathlib supplies this $\delta$ once short-exactness is known degreewise.
Local setting: Foundation layer for singular homology of pairs, imported from SingularPrism and Mathlib homology sequences. The injectivity hypothesis on $f.hom$ ensures the relative complex is well-formed and the SES is short exact.
proof idea
One-line wrapper. Apply the connecting homomorphism field $\delta$ of the short-exactness certificate pairSES_shortExact f hf, at degrees $n+1$ and $n$, with the down-shape witness ComplexShape.down_mk _ _ rfl that records the degree drop by one.
why it matters
Supplies the boundary operator that appears in the long exact sequence of a pair, the standard tool relating absolute and relative singular homology. Downstream lemmas in the same module (e.g. the relation $\partial\circ H_n(A\to X)=0$) rest on this map. In the Recognition foundation it is scaffolding for any later identification of topological invariants with RS forcing data (eight-tick octave, $D=3$), though this declaration itself is pure homological algebra and does not yet touch T0–T8 or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.