Alphabeta Math
LemmaStatement: AI-adaptedProof: Literature-sourcedPipeline-generatedprecheck passjudge 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.

The handle complex of an h-cobordism is contractible over the group ring, with an explicit contraction

Statement

Assume ACω (The Axiom of Countable Choice (ACω)). Let (W;M0,M1) be a nonempty connected h-cobordism whose inclusions Mi↪W are homotopy equivalences, with a finite handle decomposition relative to M0, and let C∗h(W,M0) be its based handle complex over R=Z[π1(M0)]. Then C∗h(W,M0) is contractible: it admits a right R-linear chain contraction s with ds+sd=id. Choose a homotopy inverse r:W→M0 and homotopies ri≃idM0 and ir≃idW, cellularly approximate r, and lift the maps and homotopies equivariantly to universal covers. The lifted inclusion induces a chain homotopy equivalence, so its algebraic mapping cone is contractible by the lifted-cone lemma. The based pair sequence 0→C∗(M~0)→C∗(i~)C∗(W~)→C∗h(W,M0)→0 is degreewise split; its quotient complex is chain homotopy equivalent to that mapping cone, hence is contractible. The argument constructs a contraction from the lifted homotopy inverse and homotopies; it does not infer contractibility from acyclicity.

Facts & Assumptions

Given: An h-cobordism (W;M0,M1) with a finite handle decomposition relative to M0, and its based handle complex C∗h(W,M0) over R=Z[π1(M0)], all lifted data taken from the handle decomposition.

[F1]

Both inclusions of an h-cobordism are homotopy equivalences, so the inclusion ι:M0↪W induces an isomorphism on fundamental groups, and any homotopy inverse r:W→M0 with homotopies rι≃idM0 and ιr≃idW can be replaced by a cellular map and cellular homotopies in the CW structure induced by the handle decomposition (h-Cobordism, Cellular approximation for maps of CW pairs, Homotopy equivalences, homotopy inverses and spaces of the same homotopy type).

[F2]

A lifted cellular homotopy equivalence of connected finite CW complexes induces a right-linear chain homotopy equivalence of the based cellular chain complexes of their universal covers, with chain homotopies induced by the lifted geometric homotopies, and its algebraic mapping cone is contractible (A lifted finite CW equivalence has a contractible group-ring mapping cone, A chain homotopy equivalence, The mapping cone of a chain map, Lifting criterion for maps from path-connected locally path-connected spaces, Universal covering spaces).

[F3]

A chain map of bounded based free complexes is a chain homotopy equivalence if and only if its algebraic mapping cone is contractible, and the based-exact-sequence clause of the AT-22 sum theorem identifies the torsion of the quotient of a degreewise split based exact sequence with the relevant cone torsion (A chain map is a homotopy equivalence exactly when its cone is contractible, Composition and based-pair sum formulas for Whitehead torsion).

[F4]

The based handle complex is the based relative cellular chain complex of the relative CW pair induced by the handle decomposition, and the degreewise split based pair sequence of a based subcomplex and its relative quotient exists with the quotient complex the relative based complex of the pair (The based handle chain complex over the fundamental group ring).

Proof

1.1F1given

Choose a homotopy inverse r:W→M0 of the inclusion ι together with homotopies H:rι≃idM0 and K:ιr≃idW; by [F1] the inclusion is a homotopy equivalence and r may be assumed cellular with cellular homotopies, so all this data is compatible with the CW structure induced by the handle decomposition.

2.1F2step 1.1

Lift r and the homotopies to the universal covers; the lifted inclusion C∗(ι~):C∗(M~0)→C∗(W~) is a right R-linear chain homotopy equivalence, with the chain homotopies induced by the lifted geometric homotopies, and its algebraic mapping cone Cone⁡(C∗(ι~)) is contractible by the lifted-cone lemma of [F2].

3.1F4step 2.1

Consider the based pair sequence 0→C∗(M~0)→C∗(ι~)C∗(W~)→C∗h(W,M0)→0 of [F4]; it is degreewise based exact and split, because the relative cells of the handle decomposition and the cells over M0 together form a basis of C∗(W~) in each degree.

4.1F3F4step 2.1step 3.1

The quotient map γ:Cone⁡(C∗(ι~))→C∗h(W,M0), γ(b,a):=[b], is a chain map for the cone differential of The mapping cone of a chain map, since q∘C∗(ι~)=0 and q is a chain map; in the degreewise splitting C∗(W~)n=C∗(M~0)n⊕Cnh of [F4] its kernel consists of the pairs (C∗(ι~)a′,a) and is the complex K(a′,a)=(∂a′+a,−∂a) on C∗(M~0)n⊕C∗(M~0)n−1, which the explicit map s(a′,a)=(0,a′) contracts, so the kernel is contractible. The displayed sequence 0→ker⁡γ→Cone⁡(C∗(ι~))→C∗h(W,M0)→0 is degreewise split; choosing a graded splitting σ and correcting it by the kernel contraction as in the proof of the based-exact-sequence clause of the AT-22 sum theorem produces a chain section σ′ with dσ′=σ′d, and then γHσ′ contracts C∗h(W,M0) for any contraction H of the cone.

5.1F2F3step 2.1step 4.1∎

Therefore C∗h(W,M0) is contractible, with a right R-linear contraction s constructed from the lifted homotopy inverse and homotopies; in particular the contraction is produced by the geometric data and not inferred from the vanishing of homology.

Depends on

Used by

Dependency tree · two levels

69 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