Long exact sequence of a pair (Hatcher, Theorem 2.16)

Let $\iota\colon V\hookrightarrow M$ be an injective continuous map (the inclusion of a subspace). Then the integral singular homology groups of $V$, $M$ and of the pair $(M,V)$ fit into a long exact sequence

Precisely, for every $k\ge0$ the sequence is exact at $H_k(M)$ (the image of $\iota_*$ is the kernel of $j_*$), at $H_{k+1}(M,V)$ (the image of $j_*$ is the kernel of $\partial$), and at $H_k(V)$ (the image of $\partial\colon H_{k+1}(M,V)\to H_k(V)$ is the kernel of $\iota_*$). This is the long exact sequence of homology groups associated with the short exact sequence of chain complexes $0\to C_\bullet(V)\to C_\bullet(M)\to C_\bullet(M,V)\to 0$; it is the basic computational tool relating the homology of a space, a subspace and the pair, and in the mission it is used for the pair $(M, M\setminus\{p\})$ of a closed manifold and its punctured version.

Formalization Note Exactness is expressed by Mathlib's ShortComplex.Exact for the three short complexes built from SP4Homology.map k ι ($\iota_*$), SP4Homology.toRel k ι ($j_*$) and SP4Homology.relδ k ι hι ($\partial$); in ModuleCat ℤ this is the equality of the range of the first map with the kernel of the second. Mathlib's snake lemma for chain complexes (ShortComplex.ShortExact.homology_exact₁/₂/₃) applies to the short exact sequence SP4Homology.relShortComplex_shortExact ι hι.