LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Integral group rings have invariant basis number

Statement

For every discrete group $π$ , the integral group ring $Z [π]$ has invariant basis number: an isomorphism of finite free right $Z [π]$ -modules $Z [π]^{m} ≅ Z [π]^{n}$ forces $m = n$ . More generally, if $R$ is an associative unital ring admitting a unital ring homomorphism $R \to S$ into a nonzero commutative unital ring $S$ , then an isomorphism of finite free right $R$ -modules $R^{m} ≅ R^{n}$ forces $m = n$ .

Facts & Assumptions

Given: An associative unital ring $R$ with a unital ring homomorphism $φ : R \to S$ into a nonzero commutative unital ring $S$ .

[F1]

For $n \geq 0$ the module $R^{n}$ consists of column vectors with entrywise addition and the right action $(v \cdot r)_{i} = v_{i} r$ , every right-linear $f : R^{m} \to R^{n}$ has a unique matrix $A \in M_{n \times m} (R)$ with $(A v)_{i} = \sum_{j} A_{i j} v_{j}$ , and the matrix of a composite is the product in the displayed order (Stable general linear and elementary groups for right modules).

[F2]

A unital ring homomorphism preserves sums, products and the identity, so entrywise application of $φ$ commutes with matrix multiplication and with the identity matrices (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[F3]

Every nonzero commutative unital ring has invariant basis number for finite bases: $S^{m} ≅ S^{n}$ as $S$ -modules implies $m = n$ (Every nonzero commutative ring has invariant basis number for finite bases).

[F4]

For a group $π$ the integral group ring $Z [π]$ is a unital ring with basis the elements $[g]$ , and the augmentation $ε : Z [π] \to Z$ is a ring homomorphism with $ε ([g]) = 1$ (The group ring $R [G]$ of finitely supported formal $R$ -linear combinations of group elements, The group ring $R [G]$ is a unital $R$ -algebra with basis $G$ , and each $g \in G$ is a unit of $R [G]$ , The augmentation map $ε : R [G] \to R$ and the augmentation ideal $I_{G} = \ker ε$ ).

[F5]

The integer operations make $Z$ a commutative unital ring (The integers form a commutative ring). Its zero and unit are represented by $[(0, 0)]$ and $[(1, 0)]$ (The integers as equivalence classes of pairs of naturals, Arithmetic on the integers); these classes differ, since their equality would require $0 = 1$ in $N$ , whereas $0 = \emptyset$ and $1 = {0}$ (The natural numbers $N$ (von Neumann)). Thus $Z$ is nonzero.

Proof

technique · direct

1.1

Suppose $f : R^{m} \to R^{n}$ and $g : R^{n} \to R^{m}$ are mutually inverse right-linear maps. By [F1] the images of the standard basis vectors have unique coordinate expressions, so $f$ and $g$ have matrices $A \in M_{n \times m} (R)$ and $B \in M_{m \times n} (R)$ with $f (v) = A v$ and $g (w) = B w$ for columns $v, w$ ; composing the coordinate formulas and using uniqueness of coordinates gives $B A = I_{m}$ from $g \circ f = i d$ and $A B = I_{n}$ from $f \circ g = i d$ .

givenF1

2.1

Applying $φ$ entrywise to the two matrix identities yields matrices $φ (A) \in M_{n \times m} (S)$ and $φ (B) \in M_{m \times n} (S)$ with $φ (A) φ (B) = φ (A B) = I_{n}$ and $φ (B) φ (A) = φ (B A) = I_{m}$ .

F2step 1.1

3.1

Since $S$ is commutative, the matrix $φ (A)$ defines an $S$ -linear map $S^{m} \to S^{n}$ , $x \mapsto φ (A) x$ , whose composite with $x \mapsto φ (B) x$ is the identity in both orders by step 2.1; hence $S^{m} ≅ S^{n}$ as $S$ -modules.

step 2.1

4.1

As $S$ is a nonzero commutative unital ring, [F3] applies to this isomorphism and gives $m = n$ .

F3step 3.1

5.1

For $R = Z [π]$ take $φ = ε$ : by [F4] the group ring is a unital ring and the augmentation is a unital ring homomorphism onto $Z$ , which is a nonzero commutative unital ring by [F5]; step 4.1 therefore shows that an isomorphism $Z [π]^{m} ≅ Z [π]^{n}$ of finite free right modules forces $m = n$ , and the general clause is step 4.1 itself.

F3F4F5step 4.1∎

Depends on

Used by

Dependency tree · two levels

43 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, contraction-torsion setup pp.27–28 (standard reference, not scraped)