LemmaStatement: 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.

Contraction torsion does not depend on the contraction

Statement

Let $C$ be a bounded finite based free right $R$ -chain complex over an associative unital ring $R$ , with displayed bases $B_{o d d}, B_{e v e n}$ of equal finite size, and let $s$ and $t$ be two chain contractions of $C$ with $d s + s d = i d = d t + t d$ . Then $τ_{s} (C) = τ_{t} (C) \in {\tilde{K}}_{1} (R),$ where $τ_{s}, τ_{t}$ are the contraction torsions of Finite based free complexes and contraction torsion. Their common value is written $τ (C)$ and called the torsion of the based complex $C$ . The equality uses no choice and no further hypothesis on the contraction.

Facts & Assumptions

Given: A bounded finite based free right $R$ -chain complex $C$ with two chain contractions $s, t$ and displayed bases of $C_{o d d}, C_{e v e n}$ of equal size.

[F1]

The contraction torsion is $τ_{s} (C) = [A_{s}]$ with $A_{s}$ the matrix of $(d + s)_{o d d} : C_{o d d} \to C_{e v e n}$ in the degree-ordered bases, viewed in ${\tilde{K}}_{1} (R) = K_{1} (R) / ⟨ [- 1] ⟩$ (Finite based free complexes and contraction torsion).

[F2]

For two contractions $s, t$ the parity lemma gives $[(d + s)_{o d d}] = - [(d + t)_{e v e n}]$ in $K_{1} (R)$ , where $(d + t)_{e v e n} : C_{e v e n} \to C_{o d d}$ is the even-to-odd component (A chain contraction makes the odd-to-even parity map invertible).

[F3]

${\tilde{K}}_{1} (R)$ is the quotient of $K_{1} (R)$ by the subgroup generated by $[- 1]$ , so classes equal in $K_{1} (R)$ remain equal in ${\tilde{K}}_{1} (R)$ (K₁ of a ring and the Whitehead group of a discrete group).

Proof

technique · direct

1.1

By the parity lemma both $(d + s)_{o d d}$ and $(d + t)_{o d d}$ are isomorphisms of right $R$ -modules, so in the displayed bases of equal size they have invertible square matrices $A_{s}$ and $A_{t}$ , and $B_{t}$ , the matrix of $(d + t)_{e v e n}$ , is invertible as well.

givenF1F2

2.1

Applying [F2] to the pair $(s, t)$ gives $[A_{s}] = - [(d + t)_{e v e n}] = - [B_{t}]$ , and applying it to the pair $(t, t)$ gives $[A_{t}] = - [B_{t}]$ ; hence $[A_{s}] = [A_{t}]$ in $K_{1} (R)$ .

F2step 1.1

3.1

Reducing this equality along the quotient map $K_{1} (R) \to {\tilde{K}}_{1} (R)$ of [F3] gives $τ_{s} (C) = [A_{s}] = [A_{t}] = τ_{t} (C)$ in ${\tilde{K}}_{1} (R)$ , so the two contractions define the same torsion class; no contraction-dependent data remains, and the argument used only the displayed bases and the two contraction identities.

F1F3step 2.1∎

Depends on

Used by

Dependency tree · two levels

15 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

Lück, §2.2, equation (2.7), pp.27–28 (standard reference, not scraped)