Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

The torsion of the handle complex is the torsion of the inclusion

Statement

Assume ACω (The Axiom of Countable Choice (ACω)). Let (W;M0,M1) be a nonempty connected compact smooth cobordism whose inclusion ι:M0↪W is a homotopy equivalence, and equip (W,M0) with the relative CW structure induced by a finite handle decomposition. Put π=π1(M0) and identify π1(W) with π along ι∗. Then the contraction torsion of the based handle complex C∗h(W,M0) is defined and satisfies τ(C∗h(W,M0))=τ(ι)∈Wh⁡(π), where τ(ι) is AT-22's Whitehead torsion of the inclusion computed with the induced CW structures. In particular, for a presentation with handles only in two adjacent degrees q,q+1, with differential dq+1:Cq+1→Cq given by the intersection matrix A over Z[π], the contraction torsion is (−1)q[A] in AT-22's parity convention for a two-term complex with differential in degree q+1, so (−1)q[A], rather than an unsigned matrix class, is the topological torsion of the inclusion.

Facts & Assumptions

Given: A compact smooth cobordism (W;M0,M1) whose inclusion ι:M0↪W is a homotopy equivalence, with a finite handle decomposition and the induced relative CW structure on (W,M0).

[F1]

The pairs clause of AT-22's composition and sum theorem: for a cellular map of finite CW pairs f:(X,A)→(Y,B) whose restrictions fX and fA are homotopy equivalences and whose basepoints are compatible, one has τ(fX)=j∗τ(fA)+τ(frel) in Wh(π1(Y)), where frel is the induced map of relative based cellular complexes and τ(frel) is the contraction torsion of its algebraic mapping cone; the formula also supplies the contractibility of that cone (Composition and based-pair sum formulas for Whitehead torsion, Whitehead torsion of a finite CW homotopy equivalence, Finite based free complexes and contraction torsion).

[F2]

The based handle complex of (W,M0) is the based relative cellular complex of the relative CW pair induced by the handle decomposition, with one basis vector per handle; for a presentation with handles only in two adjacent degrees q,q+1 it is the two-term complex 0→Cq+1→ACq→0 with matrix A the intersection matrix, and the contraction torsion of a two-term complex with differential in degree q+1 is (−1)q[A] (The based handle chain complex over the fundamental group ring, Finite based free complexes and contraction torsion, Contraction torsion does not depend on the contraction).

Proof

1.1F1given

Apply the pairs clause of [F1] to the cellular map of pairs f=(ι,idM0):(M0,M0)→(W,M0): both restrictions are homotopy equivalences, the first by hypothesis and the second as an identity, so τ(ι)=j∗τ(idM0)+τ(frel) where frel is the induced map of relative based cellular complexes.

2.1F1F2step 1.1

The source relative complex of the pair (M0,M0) is the zero complex, so frel is the zero map from the zero complex into the based handle complex C∗h(W,M0); its algebraic mapping cone is therefore C∗h(W,M0) itself. By [F1] the cone is contractible and τ(frel) is its contraction torsion, so the contraction torsion of C∗h(W,M0) is defined and, by [F2], independent of the chosen contraction.

2.2F1step 1.1

The first summand vanishes: the identity of M0 is simple, exhibited by the empty sequence of elementary operations (Simple homotopy equivalence), so its Whitehead torsion vanishes by Simple homotopy equivalences have zero torsion; since j∗ is a homomorphism this gives τ(ι)=τ(frel)=τ(C∗h(W,M0)).

3.1F2step 2.1step 2.2∎

For a presentation with handles only in degrees q,q+1, [F2] identifies the complex with 0→Cq+1→ACq→0. The contraction supplied by step 2.1 satisfies Asq=idCq and sqA=idCq+1, so A is invertible and sq=A−1. Thus the odd-to-even map d+s has matrix A when q is even and A−1 when q is odd, giving τ(C∗h(W,M0))=(−1)q[A]. Step 2.2 identifies this class with τ(ι).

Depends on

Used by

Dependency tree · two levels

42 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