Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27
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.

Whitehead torsion is independent of all auxiliary choices

Statement

Let f:X→Y be a homotopy equivalence of finite CW complexes and let τ(f) be the class of Whitehead torsion of a finite CW homotopy equivalence attached to a choice of cellular representative, universal covers, lifts, basepoints, orientations, orders of the cells and chain contraction. Then the image of that class in Wh(π1(Y,y)) depends on none of these choices.

Moreover:

  1. Changing the basepoint y to y′ transports τ(f) under the canonical isomorphism Wh(π1(Y,y))→Wh(π1(Y,y′)) of basepoint change, and two different paths from y to y′ induce the same isomorphism, so the transport is canonical; the same holds at the source.
  2. If f′≃f is a second finite CW homotopy equivalence with the same target basepoint, then τ(f′)=τ(f) after the canonical identifications; in particular homotopic homotopy equivalences of finite CW complexes have equal torsion.
  3. For disconnected Y all statements hold componentwise in ⨁D∈π0(Y)Wh(π1D).

Facts & Assumptions

Given: A homotopy equivalence f:X→Y of finite CW complexes with the chosen data of Whitehead torsion of a finite CW homotopy equivalence, and a second choice of the same kind, written with primes.

[F1]

τ(f) is the image in Wh(π1(Y,y)) of the contraction torsion of the based contractible complex Cone⁡(C∗(f~))n=Cn(Y~)⊕Cn−1(X~) with the target summands first, computed from the odd-to-even part of d+s in the displayed bases (Whitehead torsion of a finite CW homotopy equivalence, Finite based free complexes and contraction torsion).

[F2]

The contraction torsion of a bounded contractible based free complex does not depend on the contraction (Contraction torsion does not depend on the contraction).

[F3]

If the degree-n basis is replaced by the basis whose coordinate columns are the columns of the invertible matrix Pn in the old basis, then τnew=τold+∑n(−1)n+1[Pn] in K~1(R); if u:F→G is a chain isomorphism with equal degreewise displayed basis sizes then τ(G)=τ(F)+∑n(−1)n[un]; and unipotent upper triangular matrices have class 0 (Basis-change, direct-sum and based exact-sequence formulas, Stable elementary matrices equal the commutator subgroup).

[F4]

Reordering a basis changes the class in K1 only by [−1], reversing an orientation or replacing a chosen cell lift changes it by a unit ±g of Z[π], and all of these classes vanish in Wh(π); a change of basepoint path conjugates the fundamental group, inner automorphisms induce the identity on Wh, and two basepoint paths induce the same map there (Cellular basis ambiguities vanish in the Whitehead group).

[F5]

Chain homotopic chain maps f0≃f1:C∗→D∗ have chain-isomorphic mapping cones, by the unitriangular isomorphism Ψ(y,x)=(y+hn−1x,x) on Dn⊕Cn−1 for a chain homotopy h; chain homotopy is compatible with composition, and a deck transformation is an additive chain isomorphism which is semilinear for the corresponding inner automorphism of the group ring (Homotopic maps have chain-isomorphic mapping cones, The mapping cone of a chain map, Chain homotopy is compatible with addition and composition, Universal-cover boundaries, maps and homotopies respect the right group-ring action).

[F6]

A continuous map of finite CW complexes is homotopic to a cellular map, and homotopic cellular maps of finite CW pairs admit a cellular homotopy; both statements are choice-free for finite complexes (Cellular approximation for maps of CW pairs).

[F7]

A lifted cellular homotopy induces a right-linear chain homotopy from the initial compatible lift to the deck-twisted endpoint composite, both interpreted with the initial map’s coefficient transport; the deck map alone need not be right-linear (Universal-cover boundaries, maps and homotopies respect the right group-ring action).

Proof

technique · direct
1.1

Replacing the contraction of the cone changes nothing, by [F2]; this proves independence of the contraction.

F1F2
1.2

Consider a change of the displayed cellular bases only. In degree n the cone basis is the concatenation of the basis of Cn(Y~) and of Cn−1(X~), so a change of the cell bases induces the block-diagonal basis change diag⁡(PnY~,Pn−1X~) in degree n; by [F3] the torsion changes by ∑n(−1)n+1[diag⁡(PnY~,Pn−1X~)]. Reordering, reorienting or relifting cells changes only the individual factors PnY~, Pn−1X~ by permutation matrices, by diagonal matrices with a single entry −1, or by diagonal matrices with a single entry a group element, all of which have class 0 in Wh(π1(Y,y)) by [F4]; hence the class in Wh is unchanged.

F1F3F4
1.3

For a fixed based map f and based cover identifications, a compatible lift is unique. Changing the chosen lift over the target basepoint by a deck map Tβ changes the compatible lift to Tβf~ and the coefficient identification from f∗ to αβf∗, where αβ(h)=βhβ−1. Indeed Tβ(c⋅h)=Tβ(c)⋅αβ(h), so Tβ is αβ-semilinear, generally not R-linear. With this simultaneous coefficient change, (y,u)↦(Tβy,u) is a semilinear chain isomorphism from the cone of C∗(f~) to the cone of C∗(Tβf~). In the transported target bases Tβe~ and unchanged source bases it preserves the displayed bases; using the original target lifts instead changes each target basis by a diagonal group unit. Inner automorphisms act trivially on Wh and these diagonal units vanish there by [F4]. Thus the torsion class is unchanged under a change of compatible cover identification or lifted map.

F1F3F4F5
1.4

A change of basepoint y→y′ transports the coefficient group ring along the basepoint isomorphism π1(Y,y)→π1(Y,y′) of [F4], and every path gives the same map on Wh because two such isomorphisms differ by an inner automorphism, which acts trivially; the same argument applies at the source, and the class of a componentwise definition on a disconnected target is transported componentwise.

F4
2.1

Let f′ be a second cellular representative of the given homotopy class, with compatible lift f~′. By [F6] there is a cellular homotopy H from f to f′. Its lift beginning at f~ ends at Tβf~′, and [F7] supplies a right-linear chain homotopy C∗(f~)≃C∗(Tβf~′) for the initial coefficient transport. Step 1.3 identifies the torsion of the latter map, after its corresponding inner coefficient transport, with the torsion of C∗(f~′). Thus it remains to compare cones of the two chain-homotopic maps over the same ring.

F6F7step 1.3
3.1

For chain-homotopic f0≃f1 the isomorphism Ψ of [F5] has matrix (Ihn−10I) in the target-first cone bases, so by the isomorphism formula of [F3] the two cone torsions differ by a sum of classes of unipotent matrices, namely 0; hence the two cones give the same class in K~1 and therefore the same class in Wh. This proves independence of the cellular representative and of homotopic replacements.

F3F5step 2.1
4.1

Combining steps 1.1, 1.2, 1.3 and 1.4 gives independence of contraction, cell bases, cover identifications, lifts and basepoint paths; combining with step 3.1 gives independence of the cellular approximation and equality for homotopic homotopy equivalences; the disconnected statement is the componentwise reading of steps 1.1 through 1.4 and step 2.1.

step 1.1step 1.2step 1.3step 1.4step 3.1∎

Depends on

Used by

Dependency tree · two levels

65 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