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.

Basis-change, direct-sum and based exact-sequence formulas

Statement

Let $R$ be an associative unital ring and let $C, D, E$ be bounded finite based free right $R$ -chain complexes with displayed bases and defined torsion as in Finite based free complexes and contraction torsion, always in the reduced group ${\tilde{K}}_{1} (R)$ . Then:

(direct sums) If $C \oplus D$ carries, in each degree, the concatenation of the displayed bases of $C$ and $D$ , then $τ (C \oplus D) = τ (C) + τ (D)$ .
(basis change) If the displayed degree- $n$ basis of $C$ is replaced by the basis whose vectors have coordinate columns the columns of the invertible matrix $P_{n}$ in the old basis, then $τ_{n e w} (C) = τ_{o l d} (C) + \sum_{n} (- 1)^{n + 1} [P_{n}]$ .
(based exact sequences) If $0 \to C \overset{i}{\to} D \overset{q}{\to} E \to 0$ is a degreewise based exact sequence of chain maps between contractible such complexes, with the basis of each $D_{n}$ the concatenation of the image of the basis of $C_{n}$ and a set mapping bijectively onto the basis of $E_{n}$ , then $τ (D) = τ (C) + τ (E)$ . In diagram form, let the two rows be degreewise based exact sequences of bounded finite based free right $R$ -complexes, with vertical chain maps $a, b, c$ forming a strictly commutative diagram. Suppose two of these maps are chain homotopy equivalences and each of the three mapping cones has equally many odd and even displayed basis vectors. Then all three maps are chain homotopy equivalences and $τ (b) = τ (a) + τ (c)$ . Here, for a vertical map $v : F \to G$ , the notation is defined by $τ (v) : = τ (Cone (v))$ , with the basis of $G_{n}$ followed by that of $F_{n - 1}$ in cone degree $n$ ; the six row complexes themselves need not be contractible.
(chain isomorphisms and cones) If $u : F \to G$ is an isomorphism of bounded finite based free complexes with contractions and defined torsion (equal odd/even displayed basis sizes in each complex), and with equally many displayed basis vectors in $F_{n}$ and $G_{n}$ for every $n$ , and if $Cone (u)$ is the algebraic mapping cone with $Cone (u)_{n} = G_{n} \oplus F_{n - 1}$ carrying the basis of $G_{n}$ followed by that of $F_{n - 1}$ (The mapping cone of a chain map), then $τ (G) = τ (F) + \sum_{n} (- 1)^{n} [u_{n}]$ and $τ (Cone (u)) = \sum_{n} (- 1)^{n} [u_{n}]$ , where $u_{n}$ is written in the displayed bases. The degreewise equality makes each $u_{n}$ square; it is automatic over an invariant-basis-number ring, but not over an arbitrary unital ring.

Facts & Assumptions

Given: Bounded finite based free right $R$ -chain complexes with displayed bases and contractions, over an associative unital ring $R$ .

[F1]

Torsion is $τ (C) = [(d + s)_{o d d}] \in {\tilde{K}}_{1} (R)$ for any chain contraction $s$ , is independent of the contraction, and lies in the reduced group, where classes are additive over products, $[A B] = [A] + [B]$ , and $[A^{- 1}] = - [A]$ (Finite based free complexes and contraction torsion, Contraction torsion does not depend on the contraction, K₁ of a ring and the Whitehead group of a discrete group).

[F2]

For two contractions $s, t$ of one complex, $[(d + s)_{o d d}] = - [(d + t)_{e v e n}]$ in $K_{1} (R)$ , and both maps are isomorphisms of right $R$ -modules (A chain contraction makes the odd-to-even parity map invertible).

[F3]

A matrix that is unipotent upper triangular in a finite ordered basis lies in $E (R)$ and has class $0$ , and the class of a block sum satisfies $[diag (A, B)] = [A] + [B]$ because $diag (A, B) = diag (A, 1) diag (1, B)$ , where $diag (A, 1)$ and $diag (1, B)$ are stabilizations of $A$ and of a conjugate of $B$ (Stable general linear and elementary groups for right modules, Stable elementary matrices equal the commutator subgroup).

[F4]

The mapping cone of a chain map has $Cone (u)_{n} = G_{n} \oplus F_{n - 1}$ with differential $d (y, x) = (d^{G} y + u_{n - 1} x, - d^{F} x)$ , and a chain isomorphism $u$ is a chain map with an inverse (The mapping cone of a chain map, A chain homotopy equivalence).

[F5]

A chain map is a chain homotopy equivalence exactly when its mapping cone is contractible (A chain map is a homotopy equivalence exactly when its cone is contractible).

Proof

technique · direct

1.1

For the given complexes the parity lemma provides isomorphisms $(d + s)_{o d d}$ and $(d + s)_{e v e n}$ for every contraction $s$ ; all torsion classes below are computed from the odd-to-even components in the degree-ordered displayed bases, and equality in $K_{1} (R)$ implies equality in ${\tilde{K}}_{1} (R)$ .

givenF1F2

1.2

For the direct sum $C \oplus D$ use the contraction $s \oplus t$ and the concatenated degree-ordered bases: the parity decomposition of $C \oplus D$ is the direct sum of the parity decompositions, so the matrix of $(d^{C \oplus D} + (s \oplus t))_{o d d}$ is, after permuting the source and target bases to group the two summands, the block matrix $diag (A_{C}, A_{D})$ ; these permutations contribute only $[- 1]$ , which vanishes in the reduced group. The block matrix has class $[A_{C}] + [A_{D}] = τ (C) + τ (D)$ by [F3]; hence $τ (C \oplus D) = τ (C) + τ (D)$ .

givenF1F3

1.3

Let $u : F \to G$ be a chain isomorphism of based complexes with defined torsion and equal displayed basis sizes in each degree, as in assertion 4, and $ε$ a contraction of $F$ ; then $δ : = u ε u^{- 1}$ is a contraction of $G$ , and $(d^{G} + δ)_{o d d} = U_{e v e n} (d^{F} + ε)_{o d d} U_{o d d}^{- 1}$ where $U_{o d d}, U_{e v e n}$ are the block matrices of the components $u_{n}$ in the displayed bases. Taking classes and using additivity gives $τ (G) - τ (F) = [U_{e v e n}] - [U_{o d d}] = \sum_{n} (- 1)^{n} [u_{n}]$ , and since torsion does not depend on the contraction this holds for the displayed based complexes.

givenF1F2F4

1.4

Let $Σ F$ be the complex with $(Σ F)_{n} = F_{n - 1}$ and differential $- d^{F}$ , carrying the displayed basis of $F_{n - 1}$ in degree $n$ . Then $- ε$ is a contraction of $Σ F$ , and $(Σ F)_{o d d} = F_{e v e n}$ , $(Σ F)_{e v e n} = F_{o d d}$ , so the matrix of $(d^{Σ F} + (- ε))_{o d d}$ is $- B$ with $B$ the matrix of $(d^{F} + ε)_{e v e n}$ ; by [F2] $[B] = - [A]$ and in ${\tilde{K}}_{1} (R)$ also $[- B] = [B]$ , so $τ (Σ F) = - τ (F)$ .

givenF1F2

2.1

For a basis change as in assertion 2 let $u = i d : C \to C$ be the identity chain isomorphism from $C$ with the old basis to $C$ with the new basis; its component $u_{n}$ has matrix $P_{n}^{- 1}$ in the old and new bases, so step 1.3 gives $τ_{n e w} (C) - τ_{o l d} (C) = \sum_{n} (- 1)^{n} [P_{n}^{- 1}] = - \sum_{n} (- 1)^{n} [P_{n}] = \sum_{n} (- 1)^{n + 1} [P_{n}]$ .

F1step 1.3

2.2

For the based exact sequence $0 \to C \overset{i}{\to} D \overset{q}{\to} E \to 0$ choose a contraction $ε$ of $E$ and, using the basis splitting, the explicit right-linear section $σ_{p} : E_{p} \to D_{p}$ that sends each displayed basis vector of $E_{p}$ to the displayed basis vector of $D_{p}$ complementary to the image of the basis of $C_{p}$ ; then $s_{p} : = d_{p + 1}^{D} σ_{p + 1} ε_{p} + σ_{p} ε_{p - 1} d_{p}^{E}$ defines a chain map $s : E \to D$ with $q s = i d$ , and $i \oplus s : C \oplus E \to D$ is a chain isomorphism whose matrix in each degree is $(\begin{array}{cc} I & * \\ 0 & I \end{array})$ in the displayed concatenated bases. By steps 1.2 and 2.1, $τ (D) = τ (C \oplus E) + \sum_{p} (- 1)^{p} [i_{p} \oplus s_{p}] = τ (C) + τ (E)$ because each of the finitely many unipotent matrices $i_{p} \oplus s_{p}$ has class $0$ by [F3]; the diagram form follows after establishing the cone-sequence two-out-of-three argument below.

F3F4step 1.2step 1.3

3.1

In a degreewise based exact sequence $0 \to K \to M \to Q \to 0$ , if $Q$ is contractible then the formula for the chain section in step 2.2 splits the sequence as chain complexes, so $K$ is a chain retract of $M$ ; if $K$ is contractible, choose a graded section $σ : Q \to M$ and put $δ = d σ - σ d$ , valued in $K$ . For a contraction $h$ of $K$ , the identity $d δ + δ d = 0$ makes $σ^{'} = σ - h δ$ a chain section, so $Q$ is a chain retract of $M$ . These two splittings show directly that if any two of $K, M, Q$ are contractible then so is the third. In the diagram of assertion 3, strict commutativity and the cone differential give a degreewise exact sequence $0 \to Cone (a) \to Cone (b) \to Cone (c) \to 0$ . Reordering the middle cone basis groups the two subcomplex summands before the two quotient summands, making this sequence based exact; these permutations contribute only $[- 1] = 0$ in the reduced group. By [F5] two cones are contractible, hence all three are by the preceding splitting argument, and [F5] makes the third vertical map a chain homotopy equivalence. The assumed equality of parity basis counts licenses each cone torsion over arbitrary $R$ . Step 2.2 and the definition $τ (v) = τ (Cone (v))$ now give $τ (b) = τ (a) + τ (c)$ .

F1F4F5step 1.2step 2.2

4.1

For an isomorphism $u : F \to G$ the cone $Cone (u)$ carries the degreewise based exact sequence $0 \to G \to Cone (u) \to Σ F \to 0$ with the concatenated bases, so by step 2.2 $τ (Cone (u)) = τ (G) + τ (Σ F) = τ (G) - τ (F) = \sum_{n} (- 1)^{n} [u_{n}]$ by step 1.3, which together with steps 1.2, 2.1 and 2.2 proves all the stated formulas.

F4step 1.3step 1.4step 2.2∎

Depends on

Used by

Dependency tree · two levels

26 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, Lemma 2.9 and equation (2.11), pp.29–30 (standard reference, not scraped)
Cohen, §§19–20, pp.62–69 (standard reference, not scraped)