Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Ordinary acyclicity over Z does not detect group-ring torsion

Statement refuted

False claim: a bounded based free complex over a group ring whose underlying complex of abelian groups is acyclic must have vanishing torsion class in the Whitehead group of the group.

Facts & Assumptions

Given: The cyclic group π=C5=⟨t∣t5=1⟩, its group ring R=Z[π], and the element u=1−t2−t3∈R.

[F1]

The element u=1−t2−t3 is a unit of R=Z[C5] and its class [u] is a nonzero element of Wh(C5) (Cellular basis ambiguities vanish in the Whitehead group, K₁ of a ring and the Whitehead group of a discrete group).

[F2]

Contraction torsion of a two-term based free complex: for a unit u in a unital ring R and the complex 0→Cq=R→uCq−1=R→0 with the displayed single basis vector in each of the two degrees, the contraction is sq−1=u−1 and sq=0, and the contraction torsion is τ(C)=(−1)q+1[u]∈K~1(R) (Finite based free complexes and contraction torsion).

[F3]

The augmentation ε:R[G]→R is the ring homomorphism sending each basis element [g] to 1, and the group ring is the free module on the classes [g] with the uniquely determined product (The augmentation map ε:R[G]→R and the augmentation ideal IG=ker⁡ε, The group ring R[G] is a unital R-algebra with basis G, and each g∈G is a unit of R[G]).

[F4]

The handle chain complex is carried over the group ring with its chosen lifts and basis data, so that its torsion lives in Wh(π1) and not merely in a theory of abelian chain complexes (The based handle chain complex over the fundamental group ring).

Counterexample

1.1F1F2given

Let C be the based free right R-complex 0→C1=R→d1C0=R→0 with differential d1(x)=xu, generated in degree one and zero by one basis vector each. By [F1] u is a unit, and the map h0(y)=yu−1, h1=0 satisfies d1h0=idC0 and h0d1=idC1, so C is contractible with this contraction; by [F2] with q=1 its contraction torsion is τ(C)=(−1)2[u]=[u], which is nonzero in Wh(C5) by [F1].

2.1F3step 1.1

Forgetting the R-module structure, the contraction h of step 1.1 is a homomorphism of abelian groups, so it contracts the underlying complex of abelian groups of C; hence that underlying complex is contractible, and in particular acyclic, with differential the isomorphism x↦xu and inverse y↦yu−1. Separately, by [F3] the augmentation ε:Z[C5]→Z is a ring homomorphism with ε(1)=1 and ε(tk)=1 for every k, so ε(u)=1−1−1=−1, which is a unit of Z; the base change along ε gives the complex 0→Z→−1Z→0, contracted by n↦−n, whose homology also vanishes.

3.1F4step 1.1step 2.1∎

The complex C is bounded and based free over R=Z[C5], its contraction torsion class [u] is nonzero in Wh(C5) by step 1.1, and its underlying complex of abelian groups is contractible, in particular acyclic, by step 2.1; therefore the false claim fails. This is exactly why the handle chain complex of a cobordism is carried over Z[π1] with its chosen lifts and basis and not over Z, as recorded in [F4]: an abelian acyclicity check cannot see the class [u].

Depends on

Used by

Nothing in the library uses this result yet.

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