ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck pass

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.

Relative Morse homology of a single-handle cobordism

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $0 \leq k \leq n$ and let $(W; M_{0}, M_{1})$ be a compact smooth cobordism obtained from a collar of $M_{0}$ by attaching one index- $k$ handle, with corners rounded. Fix adapted Morse--Smale data having exactly one interior critical point, of index $k$ (Smooth cobordism triad for Morse theory, Morse function adapted to a cobordism, Handle decomposition relative to the incoming boundary, Nondegenerate critical points, nullity, index, and coindex). The two boundary faces of this cobordism are disjoint closed manifolds. The handle attachment pair is $(D^{k} \times D^{n - k}, S^{k - 1} \times D^{n - k})$ ; its attaching and belt regions meet at a corner when $0 < k < n$ , so they are not themselves the two faces of a cobordism triad.

Then the relative Morse complex of The relative Morse complex of an adapted cobordism has exactly one generator, in degree $k$ , and no differential, so $H M_{i} (W, M_{0}; Λ) = {\begin{cases} Λ, & i = k, \\ 0, & i \neq k, \end{cases}$ recovering the single relative generator of the handle pair (One critical point handle attachment, Relative homology of a single handle pair) and matching $H_{*} (W, M_{0}; Λ) ≅ H_{*} (D^{k}, S^{k - 1}; Λ)$ as groups (Relative singular homology).

Facts & Assumptions

Given: The Axiom of Choice, $0 \leq k \leq n$ , and the smooth single-handle cobordism with the adapted Morse--Smale data just specified.

[F1]

By the hypothesis, the adapted Morse function has exactly one interior critical point of index $k$ . The single rounded handle is its handle model (One critical point handle attachment, Morse function adapted to a cobordism, Smooth cobordism triad for Morse theory).

[F2]

The relative Morse chain groups are free on the interior critical points, and the differential counts trajectories between points of adjacent index (The relative Morse complex of an adapted cobordism, part 2). With one critical point the formula defines a chain complex directly; no general cellular comparison is needed for its homology computation.

[F3]

Collar excision identifies the relative homology of the single-handle cobordism with the standard handle-pair homology, which is $Λ$ in degree $k$ and zero otherwise (Relative homology of a single handle pair, Relative homology of the standard handle pair, Relative singular homology).

Verification

technique · direct

1.1F1F2given

By [F1] the only critical point of the adapted function is the interior point of index $k$ ; hence the relative Morse chain groups of [F2] are $Λ$ in degree $k$ and zero in every other degree, since they are free on the interior critical points.

2.1F2step 1.1

The only differential that could be nonzero is $\partial_{k} : C M_{k} \to C M_{k - 1}$ , whose target is the group of the critical points of index $k - 1$ ; there are none, so $\partial_{k} = 0$ , and all other differentials have zero source or target. Therefore the relative Morse complex is $Λ$ concentrated in degree $k$ .

3.1step 2.1

The homology of that complex is $Λ$ in degree $k$ and zero otherwise, which is the displayed formula for $H M_{i} (W, M_{0}; Λ)$ .

4.1F2F3step 3.1∎

By [F3] the handle pair has the relative homology of $(D^{k}, S^{k - 1})$ , again $Λ$ in degree $k$ and zero otherwise; the two computations agree, and the single relative generator is the one recorded by the handle attachment.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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

Liviu I. Nicolaescu, An Invitation to Morse Theory, 2nd ed. (complete author PDF, 291 pp.) (standard reference, not scraped)
Alexander F. Ritter, Part III Morse Homology (Cambridge lecture notes, complete author PDF, 115 pp.) (standard reference, not scraped)