LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A product collar deformation retracts onto its face

Statement

Let $M$ be a smooth manifold (possibly with boundary) and let $C = M \times [0, 1]$ be a product collar with face $M_{0} = M \times {0}$ (the restriction of a smooth collar, Smooth collars of a manifold boundary). Then the projection $r : C \to M_{0}, r (x, t) : = (x, 0),$ is a strong deformation retraction (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise), and consequently for every abelian group $G$ and every $i$ the relative homology $H_{i} (C, M_{0}; G)$ vanishes: the map of pairs $r : (C, M_{0}) \to (M_{0}, M_{0})$ induces isomorphisms on relative homology (Relative singular homology).

Facts & Assumptions

Given: A smooth manifold $M$ , the product collar $C = M \times [0, 1]$ with face $M_{0} = M \times {0}$ , and an abelian group $G$ .

[F1]

A strong deformation retraction of $X$ onto $A \subseteq X$ is a retraction $r : X \to A$ together with a homotopy $H : {id}_{X} ≃_{A} i \circ r$ fixing $A$ pointwise (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

[F2]

A map $f : X \to Y$ is a homotopy equivalence when there is $g : Y \to X$ with $g \circ f ≃ {id}_{X}$ and $f \circ g ≃ {id}_{Y}$ (Homotopy equivalences, homotopy inverses and spaces of the same homotopy type).

[L1]

A homotopy equivalence induces an isomorphism on singular homology in every degree and every coefficient group (Homotopy equivalences induce isomorphisms on singular homology).

[F3]

For $A \subseteq X$ the sequence $\dots \to H_{n} (A; G) \to H_{n} (X; G) \to H_{n} (X, A; G) \overset{δ}{\to} H_{n - 1} (A; G) \to \dots$ is exact (Long exact sequence of a pair).

[F4]

A map of pairs induces a commuting morphism of the two pair long exact sequences, including the connecting maps (Naturality of the pair long exact sequence).

[F5]

If four comparison maps of a morphism of long exact sequences in an abelian category are isomorphisms, then so is the fifth (Five lemma for a morphism of long exact sequences).

[L2]

The relative chain group is $C_{n} (X, A; G) = C_{n} (X; G) / C_{n} (A; G)$ , so $C_{n} (X, X; G) = 0$ and $H_{n} (X, X; G) = 0$ for all $n$ (Relative singular chain complex, Relative singular homology).

Proof

technique · explicit formulas

1.1F1givenconstruct

Define $H ((x, t), s) : = (x, (1 - s) t)$ for $(x, t) \in C$ and $s \in [0, 1]$ . This is continuous, being the restriction of the smooth map $M \times [0, 1]^{2} \to C$ , and it satisfies $H ((x, t), 0) = (x, t)$ , $H ((x, t), 1) = (x, 0) = r (x, t)$ and $H ((x, 0), s) = (x, 0)$ for every $(x, t) \in C$ and every $s$ . Thus $r$ is a retraction of $C$ onto $M_{0}$ and $H$ is a homotopy from ${id}_{C}$ to $i \circ r$ fixing $M_{0}$ pointwise, so by [F1] the projection $r$ is a strong deformation retraction onto $M_{0}$ .

2.1F2L1step 1.1

Since $r \circ i = {id}_{M_{0}}$ and $H$ displays $i \circ r ≃ {id}_{C}$ , the maps $r$ and the inclusion $i : M_{0} \to C$ are homotopy inverses, so $r$ is a homotopy equivalence by [F2]. By [L1], for every $j$ the induced map $H_{j} (r; G) : H_{j} (C; G) \to H_{j} (M_{0}; G)$ is an isomorphism.

3.1F3F4step 2.1

The map $r$ is a map of pairs $r : (C, M_{0}) \to (M_{0}, M_{0})$ , so by [F4] it induces a morphism from the exact sequence of [F3] for $(C, M_{0})$ to that for $(M_{0}, M_{0})$ : $\dots \to H_{j} (M_{0}; G) \to H_{j} (C; G) \to H_{j} (C, M_{0}; G) \to H_{j - 1} (M_{0}; G) \to \dots$ compared with $\dots \to H_{j} (M_{0}; G) \to H_{j} (M_{0}; G) \to H_{j} (M_{0}, M_{0}; G) \to H_{j - 1} (M_{0}; G) \to \dots .$ In this morphism the comparison map on $H_{j} (C; G)$ is the isomorphism of step 2.1, and every comparison map on a copy of $H_{j} (M_{0}; G)$ is the identity, because on the subspace $M_{0}$ the map $r$ is the identity.

4.1F5step 3.1

Fix $i$ and apply [F5] to the five-term window of this morphism centred on the comparison map $H_{i} (C, M_{0}; G) \to H_{i} (M_{0}, M_{0}; G)$ : by step 3.1 the four surrounding comparison maps are isomorphisms (each is either an identity or $H_{j} (r; G)$ ), so the relative comparison map is an isomorphism.

5.1L2step 4.1∎

The relative complex of the pair $(M_{0}, M_{0})$ is the zero complex by [L2], so $H_{i} (M_{0}, M_{0}; G) = 0$ ; hence $H_{i} (C, M_{0}; G) = 0$ for every $i$ , and the map of pairs $r$ induces these isomorphisms on relative homology.

Remarks

The general collar case. A smooth collar neighbourhood of $\partial M$ is diffeomorphic to a product (Smooth collars of a manifold boundary), so the lemma applies to it verbatim; this is the form used to identify the relative homology of the top sublevel pair in the relative Morse inequalities.
Choice. The homotopy $H$ and the retraction $r$ are explicit formulas, so no choice principle is used to define the deformation; the cited homological suppliers are used as published.
Empty cases. If $M = \emptyset$ then $C = \emptyset = M_{0}$ and all groups vanish; the argument applies with $H$ the empty map.

Depends on

Used by

Relative Morse inequalities for a cobordism Proposition

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Allen Hatcher, Algebraic Topology, Sections 2.1-2.2 (relative homology and long exact sequences) (standard reference, not scraped)